One-step probabilistic AC0 layer advancement

This module packages the standard circuit-level application of the switching lemma. If every wire through logical layer i has decision-tree depth at most t after a base restriction rho, then a fresh independent p-restriction advances the same invariant through layer i + 1, except with probability at most

andOrCost(program) * (5 * p * t)^(t + 1).

The proof composes exact bounded DNFs through OR gates and exact bounded CNFs through AND gates, applies the single-formula switching lemma at each charged gate, and takes an ordinary finite union bound over exactly the AND/OR gates. Input negations contribute neither probability loss nor source size. All events are semantic decision-tree predicates. Their decidability is classical and noncomputable solely so the exact finite probability can be formed; no tree optimizer, circuit search, or finite lower-bound experiment is defined.

theorem Algebraic.AC0.Op.eq_not_of_connective_eq_none {operation : Op} (notConnective : operation.connective = none) : operation = not

The only AC0 operation that is not a connective is NOT.

@[instance_reducible]

noncomputable instance Algebraic.AC0.Program.shallowUpToDecidable {n g : ℕ} (program : Program signature n g) (rho : PartialAssignment n) (level bound : ℕ) : Decidable (ShallowUpTo program rho level bound)

Proof-level decidability of the semantic layer invariant. This instance is used only to form exact finite restriction events; it does not search for decision trees.

Equations

• Algebraic.AC0.Program.shallowUpToDecidable program rho level bound = Classical.propDecidable (Algebraic.AC0.Program.ShallowUpTo program rho level bound)

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

Under checked input-negation normal form, a NOT gate has logical depth zero.

theorem Algebraic.AC0.Program.logicalGateDepth_eq_zero_of_not_connective {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (gate : Fin g) (notConnective : Op.connective (program.lines gate).op = none) : logicalGateDepths program gate = 0

Under checked input-negation normal form, every non-connective gate has logical depth zero.

theorem Algebraic.AC0.Program.ShallowUpTo.succ_of_connective_raw {n g : ℕ} {program : Program signature n g} {rho extension : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (next : ∀ gate ∈ connectiveGates program, logicalGateDepths program gate ≤ level + 1 → DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) bound) : ShallowUpTo program (rho.refine extension) (level + 1) bound

If every charged gate in the next layer is shallow after an extension, then the semantic shallow-layer invariant advances by one. Arbitrary internal NOT chains are handled directly by topological induction and negating the tree for their source wire.

theorem Algebraic.AC0.Program.ShallowUpTo.succ_of_connective {n g : ℕ} {program : Program signature n g} {rho extension : PartialAssignment n} {level bound : ℕ} (_normal : NegationsAtInputs program) (shallow : ShallowUpTo program rho level bound) (next : ∀ gate ∈ connectiveGates program, logicalGateDepths program gate ≤ level + 1 → DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) bound) : ShallowUpTo program (rho.refine extension) (level + 1) bound

Compatibility wrapper for the checked input-negation presentation.

theorem Algebraic.AC0.DNF.restrict_eval_eq_refine_of_eval_eq {n : ℕ} (formula : DNF n) (function : ScalarFunction Bool n) (rho extension : PartialAssignment n) (computes : ∀ (input : Fin n → Bool), formula.eval input = function.restrict rho input) : (formula.restrict extension).eval = function.restrict (rho.refine extension)

Restricting a represented DNF composes exactly with the base restriction.

theorem Algebraic.AC0.CNF.restrict_eval_eq_refine_of_eval_eq {n : ℕ} (formula : CNF n) (function : ScalarFunction Bool n) (rho extension : PartialAssignment n) (computes : ∀ (input : Fin n → Bool), formula.eval input = function.restrict rho input) : (formula.restrict extension).eval = function.restrict (rho.refine extension)

Restricting a represented CNF composes exactly with the base restriction.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_gate_not_depthAtMost_refine_le_five {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) (connective : gate ∈ connectiveGates program) (gateDepth : logicalGateDepths program gate ≤ level + 1) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) bound) ≤ (5 * ↑p * ↑bound) ^ (bound + 1)

One charged gate in the next logical layer fails the common shallow-tree bound with probability at most the switching-lemma estimate.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_gate_in_nextLayer_not_depthAtMost_refine_le_five {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) (connective : gate ∈ connectiveGates program) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => logicalGateDepths program gate ≤ level + 1 ∧ ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) bound) ≤ (5 * ↑p * ↑bound) ^ (bound + 1)

The next-layer failure event for one charged gate obeys the same bound; gates outside the layer contribute the empty event.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_exists_connective_in_nextLayer_not_depthAtMost_refine_le_five {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ∃ gate ∈ connectiveGates program, logicalGateDepths program gate ≤ level + 1 ∧ ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) bound) ≤ ↑(Program.cost andOrCost program) * (5 * ↑p * ↑bound) ^ (bound + 1)

Union bound over exactly the charged gates in the next logical layer.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_not_succ_refine_le_five_raw {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ¬ShallowUpTo program (rho.refine extension) (level + 1) bound) ≤ ↑(Program.cost andOrCost program) * (5 * ↑p * ↑bound) ^ (bound + 1)

One random switching step advances the semantic shallow-tree invariant by one logical layer, except on an event of charged-size times the standard switching-lemma failure probability. This raw form permits arbitrary internal NOT gates.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_not_succ_refine_le_five {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (_normal : NegationsAtInputs program) (shallow : ShallowUpTo program rho level bound) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ¬ShallowUpTo program (rho.refine extension) (level + 1) bound) ≤ ↑(Program.cost andOrCost program) * (5 * ↑p * ↑bound) ^ (bound + 1)

Compatibility wrapper for the checked input-negation presentation.