The iterated switching contradiction for parity circuits

This module connects iterated semantic depth reduction to exact parity resilience at a designated circuit output. If a one-output circuit computes parity, any ShallowUpTo witness covering that output forces the restriction to leave at most the common decision-tree allowance many variables live.

Combining that fact with exists_shallowUpTo_with_liveCount gives the central parameterized contradiction: a survivor schedule satisfying the explicit switching inequalities rules out the circuit whenever its final value exceeds the tree-depth allowance. Closed-form parameter selection is intentionally a separate arithmetic layer.

theorem Algebraic.AC0.Program.ShallowUpTo.parity_liveCount_le {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (wire : Wire n g) (wireDepth : logicalWireDepths program wire ≤ level) (computes : program.wireFunction interpretation wire = Parity.function n) : rho.liveCount ≤ bound

A shallow invariant covering a parity-computing wire forces the live count below the common tree-depth allowance.

theorem Algebraic.AC0.Circuit.logicalOutputDepth_le_logicalDepth {n m : ℕ} (circuit : Circuit signature n m) (output : Fin m) : logicalOutputDepths circuit output ≤ logicalDepth circuit

Every designated output depth is at most the circuit's maximum logical output depth.

theorem Algebraic.AC0.Circuit.logicalWireDepth_output_le {n m : ℕ} (circuit : Circuit signature n m) (output : Fin m) (level : ℕ) (depthBound : logicalDepth circuit ≤ level) : Program.logicalWireDepths circuit.program (circuit.outputs output) ≤ level

A circuit logical-depth bound covers each designated output wire in the underlying program.

theorem Algebraic.AC0.Circuit.wireFunction_output_eq_parity_of_computes {n : ℕ} {circuit : Circuit signature n 1} (computes : circuit.ComputesWith interpretation (Parity.target n)) : circuit.program.wireFunction interpretation (circuit.outputs 0) = Parity.function n

Exact circuit computation of parity identifies the scalar function on its unique designated output wire.

theorem Algebraic.AC0.Circuit.liveCount_le_of_shallowUpTo_computes_parity {n : ℕ} {circuit : Circuit signature n 1} {rho : PartialAssignment n} {level bound : ℕ} (computes : circuit.ComputesWith interpretation (Parity.target n)) (depthBound : logicalDepth circuit ≤ level) (shallow : Program.ShallowUpTo circuit.program rho level bound) : rho.liveCount ≤ bound

A shallow invariant covering a parity circuit's output leaves at most the tree-depth allowance many variables live.

theorem Algebraic.AC0.Circuit.retained_le_bound_of_iterated_parity_raw {n : ℕ} (circuit : Circuit signature n 1) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth bound : ℕ) (circuitDepth : logicalDepth circuit ≤ depth) (oneLeBound : 1 ≤ bound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : Program.layerFailureBound circuit.program p bound ≤ ↑p) (room : ∀ level < depth, Program.layerFailureBound circuit.program p bound * ↑(retained level) + ↑(retained (level + 1)) < ↑p * ↑(retained level)) : retained depth ≤ bound

Any parity circuit satisfying the iterated switching premises forces the final survivor schedule below the common tree-depth allowance, with arbitrary internal NOT gates.

theorem Algebraic.AC0.Circuit.retained_le_bound_of_iterated_parity {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth bound : ℕ) (circuitDepth : logicalDepth circuit ≤ depth) (oneLeBound : 1 ≤ bound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : Program.layerFailureBound circuit.program p bound ≤ ↑p) (room : ∀ level < depth, Program.layerFailureBound circuit.program p bound * ↑(retained level) + ↑(retained (level + 1)) < ↑p * ↑(retained level)) : retained depth ≤ bound

Compatibility wrapper for the checked input-negation presentation.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_iterated_switching_raw {n : ℕ} (circuit : Circuit signature n 1) (depth bound : ℕ) (circuitDepth : logicalDepth circuit ≤ depth) (oneLeBound : 1 ≤ bound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : Program.layerFailureBound circuit.program p bound ≤ ↑p) (room : ∀ level < depth, Program.layerFailureBound circuit.program p bound * ↑(retained level) + ↑(retained (level + 1)) < ↑p * ↑(retained level)) (tooMany : bound < retained depth) : ¬circuit.ComputesWith interpretation (Parity.target n)

Parameterized iterated-switching lower bound: if the survivor schedule ends above the tree allowance, the circuit cannot compute parity, even with arbitrary internal NOT gates.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_iterated_switching {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (depth bound : ℕ) (circuitDepth : logicalDepth circuit ≤ depth) (oneLeBound : 1 ≤ bound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : Program.layerFailureBound circuit.program p bound ≤ ↑p) (room : ∀ level < depth, Program.layerFailureBound circuit.program p bound * ↑(retained level) + ↑(retained (level + 1)) < ↑p * ↑(retained level)) (tooMany : bound < retained depth) : ¬circuit.ComputesWith interpretation (Parity.target n)

Compatibility wrapper for the checked input-negation presentation.