Extracting bottom AC0 gates as bounded normal forms

Source logical depth counts AND/OR gates and gives every negation zero delay. This module proves the structural fact needed for circuit depth reduction: every wire of logical depth zero, including an arbitrary internal NOT chain, computes a signed original input. The older bottom-gate extraction API retains its checked input-negation premise for compatibility; semantic layer reduction uses the unrestricted literal theorem directly.

Those literal inputs are converted to the exact DNF or CNF from LiteralGate. The resulting formula computes the internal shared-DAG gate function pointwise and has width at most the gate's fan-in. No circuit is unfolded into a formula, so sharing is preserved outside the one gate being extracted.

def Algebraic.AC0.Program.logicalGateDepths {n g : ℕ} (program : Program signature n g) : Fin g → ℕ

Source logical depth of each internal program gate.

Equations

• Algebraic.AC0.Program.logicalGateDepths program = program.eval Algebraic.AC0.logicalDepthInterpretation fun (x : Fin n) => 0

def Algebraic.AC0.Program.logicalWireDepths {n g : ℕ} (program : Program signature n g) : Wire n g → ℕ

Source logical depth of each input or internal-gate wire.

Equations

• Algebraic.AC0.Program.logicalWireDepths program = program.trace Algebraic.AC0.logicalDepthInterpretation fun (x : Fin n) => 0

@[simp]

theorem Algebraic.AC0.Program.logicalWireDepths_input {n g : ℕ} (program : Program signature n g) (input : Fin n) : logicalWireDepths program (Wire.input input) = 0

Original inputs have source logical depth zero.

@[simp]

theorem Algebraic.AC0.Program.logicalWireDepths_gate {n g : ℕ} (program : Program signature n g) (gate : Fin g) : logicalWireDepths program (Wire.gate gate) = logicalGateDepths program gate

A gate wire has the source logical depth of that gate.

theorem Algebraic.AC0.Program.lines_logicalDepth {n g : ℕ} (program : Program signature n g) (gate : Fin g) : (program.lines gate).eval logicalDepthInterpretation (fun (x : Fin n) => 0) (logicalGateDepths program) = logicalGateDepths program gate

Evaluating a widened program line in the logical-depth interpretation recovers the stored depth of its gate.

theorem Algebraic.AC0.Program.line_op_eq_not_of_logicalDepth_zero {n g : ℕ} (program : Program signature n g) (gate : Fin g) (depthZero : logicalGateDepths program gate = 0) : (program.lines gate).op = Op.not

An internal gate of source logical depth zero must be a NOT gate.

theorem Algebraic.AC0.Line.NegationAtInput.castSucc {n g : ℕ} {line : Line signature n g} (atInput : NegationAtInput line) : NegationAtInput (line.mapWires Wire.Renaming.castSucc.apply)

Widening a line's gate-wire namespace preserves the property that a NOT reads an original input.

theorem Algebraic.AC0.Program.NegationsAtInputs.line {n g : ℕ} {program : Program signature n g} (normal : NegationsAtInputs program) (gate : Fin g) : Line.NegationAtInput (program.lines gate)

Every widened line of an input-negation-normal program satisfies the same input-negation condition.

theorem Algebraic.AC0.Program.exists_literal_of_logicalWireDepth_zero_raw {n g : ℕ} (program : Program signature n g) (wire : Wire n g) (depthZero : logicalWireDepths program wire = 0) : ∃ (literal : Literal n), program.wireFunction interpretation wire = literal.eval

Every source-depth-zero wire computes an explicit signed original-input literal, even when NOT gates form arbitrary internal chains.

theorem Algebraic.AC0.Program.exists_literal_of_logicalWireDepth_zero {n g : ℕ} (program : Program signature n g) (_normal : NegationsAtInputs program) (wire : Wire n g) (depthZero : logicalWireDepths program wire = 0) : ∃ (literal : Literal n), program.wireFunction interpretation wire = literal.eval

Every source-depth-zero wire of an input-negation-normal program computes an explicit signed original-input literal.

def Algebraic.AC0.Line.LiteralInputs {n g : ℕ} (program : Program signature n g) (line : Line signature n g) : Prop

Every argument wire of a line computes the corresponding signed input literal.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.AC0.Line.LiteralInputs.literals {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) : Fin (arity line.op) → Literal n

Chosen literal family witnessing LiteralInputs.

Equations

• literalInputs.literals = Classical.choose literalInputs

theorem Algebraic.AC0.Line.LiteralInputs.literals_spec {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) (argument : Fin (arity line.op)) : program.wireFunction interpretation (line.wires argument) = (literalInputs.literals argument).eval

Each chosen literal computes its source argument wire.

noncomputable def Algebraic.AC0.Line.LiteralInputs.andLiterals {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.and fanIn) : Fin fanIn → Literal n

Transport the chosen literal family to the declared fan-in of an AND line.

Equations

• literalInputs.andLiterals operation argument = literalInputs.literals (Fin.cast ⋯ argument)

noncomputable def Algebraic.AC0.Line.LiteralInputs.orLiterals {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.or fanIn) : Fin fanIn → Literal n

Transport the chosen literal family to the declared fan-in of an OR line.

Equations

• literalInputs.orLiterals operation argument = literalInputs.literals (Fin.cast ⋯ argument)

noncomputable def Algebraic.AC0.Line.LiteralInputs.andFormula {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.and fanIn) : DNF n

Exact DNF representation of an AND line whose arguments are literals.

Equations

• literalInputs.andFormula operation = Algebraic.AC0.LiteralFamily.conjunction (literalInputs.andLiterals operation)

noncomputable def Algebraic.AC0.Line.LiteralInputs.orFormula {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.or fanIn) : CNF n

Exact CNF representation of an OR line whose arguments are literals.

Equations

• literalInputs.orFormula operation = Algebraic.AC0.LiteralFamily.disjunction (literalInputs.orLiterals operation)

theorem Algebraic.AC0.Line.LiteralInputs.andFormula_widthAtMost {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.and fanIn) : (literalInputs.andFormula operation).WidthAtMost fanIn

The extracted AND formula has width at most the line fan-in.

theorem Algebraic.AC0.Line.LiteralInputs.orFormula_widthAtMost {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.or fanIn) : (literalInputs.orFormula operation).WidthAtMost fanIn

The extracted OR formula has width at most the line fan-in.

theorem Algebraic.AC0.Line.LiteralInputs.andFormula_eval {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.and fanIn) (input : Fin n → Bool) : (literalInputs.andFormula operation).eval input = line.eval interpretation input (program.eval interpretation input)

The extracted DNF computes the original AND line.

theorem Algebraic.AC0.Line.LiteralInputs.orFormula_eval {n g : ℕ} {program : Program signature n g} {line : Line signature n g} (literalInputs : LiteralInputs program line) {fanIn : ℕ} (operation : line.op = Op.or fanIn) (input : Fin n → Bool) : (literalInputs.orFormula operation).eval input = line.eval interpretation input (program.eval interpretation input)

The extracted CNF computes the original OR line.

theorem Algebraic.AC0.Program.argument_logicalWireDepth_zero_of_gateDepth_one {n g : ℕ} (program : Program signature n g) (gate : Fin g) (depthOne : logicalGateDepths program gate = 1) (connective : Op.connective (program.lines gate).op ≠ none) (argument : Fin (arity (program.lines gate).op)) : logicalWireDepths program ((program.lines gate).wires argument) = 0

Every argument of a connective gate at source logical depth one has source logical depth zero.

theorem Algebraic.AC0.Program.literalInputs_of_gateDepth_one {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) (depthOne : logicalGateDepths program gate = 1) (connective : Op.connective (program.lines gate).op ≠ none) : Line.LiteralInputs program (program.lines gate)

A connective gate at source logical depth one has a semantic signed literal for every argument wire.

noncomputable def Algebraic.AC0.Program.andGateFormula {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (depthOne : logicalGateDepths program gate = 1) : DNF n

Extract a source-depth-one AND gate as an exact DNF.

Equations

• Algebraic.AC0.Program.andGateFormula program normal gate operation depthOne = ⋯.andFormula operation

noncomputable def Algebraic.AC0.Program.orGateFormula {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (depthOne : logicalGateDepths program gate = 1) : CNF n

Extract a source-depth-one OR gate as an exact CNF.

Equations

• Algebraic.AC0.Program.orGateFormula program normal gate operation depthOne = ⋯.orFormula operation

theorem Algebraic.AC0.Program.andGateFormula_widthAtMost {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (depthOne : logicalGateDepths program gate = 1) : (andGateFormula program normal gate operation depthOne).WidthAtMost fanIn

The extracted depth-one AND-gate DNF has width at most its fan-in.

theorem Algebraic.AC0.Program.orGateFormula_widthAtMost {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (depthOne : logicalGateDepths program gate = 1) : (orGateFormula program normal gate operation depthOne).WidthAtMost fanIn

The extracted depth-one OR-gate CNF has width at most its fan-in.

theorem Algebraic.AC0.Program.andGateFormula_eval {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (depthOne : logicalGateDepths program gate = 1) (input : Fin n → Bool) : (andGateFormula program normal gate operation depthOne).eval input = program.gateFunction interpretation gate input

The extracted DNF computes the internal AND gate's scalar function.

theorem Algebraic.AC0.Program.orGateFormula_eval {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (depthOne : logicalGateDepths program gate = 1) (input : Fin n → Bool) : (orGateFormula program normal gate operation depthOne).eval input = program.gateFunction interpretation gate input

The extracted CNF computes the internal OR gate's scalar function.