Bounded normal forms for the next AC0 layer

Suppose every wire through logical depth i has a decision tree of depth at most t after a restriction. The tree-to-normal-form theorem gives every argument of a connective gate in layer i + 1 an exact width-t DNF and CNF. Flattening the argument DNFs through an OR, or the argument CNFs through an AND, preserves that common width bound regardless of the gate's fan-in.

This is the deterministic composition step in the standard layer-by-layer switching-lemma application. It traverses supplied formulas and stored gate arguments structurally; it neither expands a truth table nor searches for an optimal representation.

def Algebraic.AC0.DNF.disjoinFamily {count n : ℕ} (formulas : Fin count → DNF n) : DNF n

Disjoin a finite indexed family of DNFs by flattening their ordered term lists.

Equations

• Algebraic.AC0.DNF.disjoinFamily formulas = { terms := List.flatMap Algebraic.AC0.DNF.terms (List.ofFn formulas) }

theorem Algebraic.AC0.DNF.eval_disjoinFamily {count n : ℕ} (formulas : Fin count → DNF n) (input : Fin n → Bool) : (disjoinFamily formulas).eval input = interpretation (Op.or count) fun (index : Fin (signature.Arity (Op.or count))) => (formulas index).eval input

Finite DNF disjunction agrees with the unbounded OR interpretation.

theorem Algebraic.AC0.DNF.WidthAtMost.disjoinFamily {count n : ℕ} {formulas : Fin count → DNF n} {bound : ℕ} (bounded : ∀ (index : Fin count), (formulas index).WidthAtMost bound) : (DNF.disjoinFamily formulas).WidthAtMost bound

Flattening a finite family preserves a common DNF width bound.

def Algebraic.AC0.CNF.conjoinFamily {count n : ℕ} (formulas : Fin count → CNF n) : CNF n

Conjoin a finite indexed family of CNFs by flattening their ordered clause lists.

Equations

• Algebraic.AC0.CNF.conjoinFamily formulas = { clauses := List.flatMap Algebraic.AC0.CNF.clauses (List.ofFn formulas) }

theorem Algebraic.AC0.CNF.eval_conjoinFamily {count n : ℕ} (formulas : Fin count → CNF n) (input : Fin n → Bool) : (conjoinFamily formulas).eval input = interpretation (Op.and count) fun (index : Fin (signature.Arity (Op.and count))) => (formulas index).eval input

Finite CNF conjunction agrees with the unbounded AND interpretation.

theorem Algebraic.AC0.CNF.WidthAtMost.conjoinFamily {count n : ℕ} {formulas : Fin count → CNF n} {bound : ℕ} (bounded : ∀ (index : Fin count), (formulas index).WidthAtMost bound) : (CNF.conjoinFamily formulas).WidthAtMost bound

Flattening a finite family preserves a common CNF width bound.

theorem Algebraic.AC0.Line.eval_eq_or {n g : ℕ} (line : Line signature n g) (inputs : Fin n → Bool) (gates : Fin g → Bool) {fanIn : ℕ} (operation : line.op = Op.or fanIn) : line.eval interpretation inputs gates = interpretation (Op.or fanIn) fun (argument : Fin (signature.Arity (Op.or fanIn))) => Wire.elim inputs gates (line.wires (Fin.cast ⋯ argument))

Evaluation of a line known to be an OR, with its dependent argument type transported to the declared fan-in.

theorem Algebraic.AC0.Line.eval_eq_and {n g : ℕ} (line : Line signature n g) (inputs : Fin n → Bool) (gates : Fin g → Bool) {fanIn : ℕ} (operation : line.op = Op.and fanIn) : line.eval interpretation inputs gates = interpretation (Op.and fanIn) fun (argument : Fin (signature.Arity (Op.and fanIn))) => Wire.elim inputs gates (line.wires (Fin.cast ⋯ argument))

Evaluation of a line known to be an AND, with its dependent argument type transported to the declared fan-in.

theorem Algebraic.AC0.Program.ShallowUpTo.exists_argumentDNFs {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) (connective : Op.connective (program.lines gate).op ≠ none) (gateDepth : logicalGateDepths program gate ≤ level + 1) : ∃ (formulas : Fin (arity (program.lines gate).op) → DNF n), (∀ (argument : Fin (arity (program.lines gate).op)), (formulas argument).WidthAtMost bound) ∧ ∀ (argument : Fin (arity (program.lines gate).op)) (input : Fin n → Bool), (formulas argument).eval input = ScalarFunction.restrict (program.wireFunction interpretation ((program.lines gate).wires argument)) rho input

Choose exact bounded DNFs for all arguments of a connective gate in the next logical layer.

theorem Algebraic.AC0.Program.ShallowUpTo.exists_argumentCNFs {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) (connective : Op.connective (program.lines gate).op ≠ none) (gateDepth : logicalGateDepths program gate ≤ level + 1) : ∃ (formulas : Fin (arity (program.lines gate).op) → CNF n), (∀ (argument : Fin (arity (program.lines gate).op)), (formulas argument).WidthAtMost bound) ∧ ∀ (argument : Fin (arity (program.lines gate).op)) (input : Fin n → Bool), (formulas argument).eval input = ScalarFunction.restrict (program.wireFunction interpretation ((program.lines gate).wires argument)) rho input

Choose exact bounded CNFs for all arguments of a connective gate in the next logical layer.

theorem Algebraic.AC0.Program.ShallowUpTo.exists_dnf_for_or_gate {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (gateDepth : logicalGateDepths program gate ≤ level + 1) : ∃ (formula : DNF n), formula.WidthAtMost bound ∧ ∀ (input : Fin n → Bool), formula.eval input = ScalarFunction.restrict (program.gateFunction interpretation gate) rho input

An OR gate in the next layer has an exact DNF of the current common decision-tree width.

theorem Algebraic.AC0.Program.ShallowUpTo.exists_cnf_for_and_gate {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (gateDepth : logicalGateDepths program gate ≤ level + 1) : ∃ (formula : CNF n), formula.WidthAtMost bound ∧ ∀ (input : Fin n → Bool), formula.eval input = ScalarFunction.restrict (program.gateFunction interpretation gate) rho input

An AND gate in the next layer has an exact CNF of the current common decision-tree width.