A concrete finite AC0 lower bound for parity

This module instantiates the complete structural argument with the explicit probability and integer-survivor schedules. For a depth-d circuit and target tree depth t, the two source-facing numerical conditions are

S * (1/2)^(t+1) < 1/(20t)

and

t < n / (20 * (20t)^(d-2)).

Here S is the number of AND/OR gates. These inequalities rule out exact computation of parity even with arbitrary internal NOT gates, without changing S. The checked input-negation statements remain compatibility wrappers. The result is uniform in every parameter and follows from symbolic inequalities; it is not a fixed-size experiment or a finite circuit search.

theorem Algebraic.AC0.ParityParameters.treeBound_le_target (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) : treeBound t level ≤ t

Every scheduled tree allowance is at most the common target depth.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_concrete_parameters_raw {n : ℕ} (circuit : Circuit signature n 1) (rounds : ℕ) (circuitDepth : logicalDepth circuit ≤ rounds + 1) (t : ℕ) (oneLe : 1 ≤ t) (small : ParityParameters.switchingFailure circuit.program t < ↑(ParityParameters.minimumRatio t)) (tooMany : t < ParityParameters.retained n t rounds) : ¬circuit.ComputesWith interpretation (Parity.target n)

Concrete rounds-step parity contradiction using the canonical probabilities, tree bounds, and floor-divided survivor targets, with arbitrary internal NOT gates.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_concrete_parameters {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (rounds : ℕ) (circuitDepth : logicalDepth circuit ≤ rounds + 1) (t : ℕ) (oneLe : 1 ≤ t) (small : ParityParameters.switchingFailure circuit.program t < ↑(ParityParameters.minimumRatio t)) (tooMany : t < ParityParameters.retained n t rounds) : ¬circuit.ComputesWith interpretation (Parity.target n)

Compatibility wrapper for the checked input-negation presentation.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_concrete_depth_reduction_raw {n : ℕ} (circuit : Circuit signature n 1) (depth t : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (oneLe : 1 ≤ t) (small : ParityParameters.switchingFailure circuit.program t < ↑(ParityParameters.minimumRatio t)) (survivors : t < n / (20 * (20 * t) ^ (depth - 2))) : ¬circuit.ComputesWith interpretation (Parity.target n)

Depth-facing concrete parity lower bound. A depth-d circuit uses exactly d-1 restriction rounds, leaving the top gate for the normal-form obstruction. Arbitrary internal NOT gates are permitted.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_concrete_depth_reduction {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (depth t : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (oneLe : 1 ≤ t) (small : ParityParameters.switchingFailure circuit.program t < ↑(ParityParameters.minimumRatio t)) (survivors : t < n / (20 * (20 * t) ^ (depth - 2))) : ¬circuit.ComputesWith interpretation (Parity.target n)

Compatibility wrapper for the checked input-negation presentation.