The quantitative AC0 parity lower bound at an explicit scale

The integral lower bound becomes especially transparent when parameterized by an arbitrary scale t. If

(20 * (t + 1))^(d - 1) <= n,

then every depth-d circuit computing parity, even with arbitrary internal NOT gates, satisfies

2^(t + 1) <= 20 * t * S,

where S is its AND/OR-gate count. The input hypothesis implies the exact floor-divided survivor inequality, and contradiction with the fully integral finite theorem yields the size tradeoff.

This is the standard quantitative lower bound before choosing a particular integer root of n: it displays the exponent 1/(d-1) directly while keeping root rounding out of the structural theorem.

theorem Algebraic.AC0.ParityParameters.survivorDenominator_mul_succ_le_scalePow (depth t : ℕ) (twoLeDepth : 2 ≤ depth) : 20 * (20 * t) ^ (depth - 2) * (t + 1) ≤ (20 * (t + 1)) ^ (depth - 1)

The exact survivor denominator times t+1 is bounded by the cleaner scale power.

theorem Algebraic.AC0.ParityParameters.survivors_of_scalePow (n depth t : ℕ) (twoLeDepth : 2 ≤ depth) (oneLe : 1 ≤ t) (inputLarge : (20 * (t + 1)) ^ (depth - 1) ≤ n) : t < n / (20 * (20 * t) ^ (depth - 2))

The clean scale hypothesis implies the exact floor-divided survivor condition used by depth reduction.

theorem Algebraic.AC0.Circuit.parity_size_tradeoff_at_scale_raw {n : ℕ} (circuit : Circuit signature n 1) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth t : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (oneLe : 1 ≤ t) (inputLarge : (20 * (t + 1)) ^ (depth - 1) ≤ n) : 2 ^ (t + 1) ≤ 20 * t * Program.cost andOrCost circuit.program

Quantitative parity size tradeoff at an arbitrary integral scale, with arbitrary internal NOT gates charged at zero.

theorem Algebraic.AC0.Circuit.parity_size_tradeoff_at_scale {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depth t : ℕ) (twoLeDepth : 2 ≤ depth) (circuitDepth : logicalDepth circuit ≤ depth) (oneLe : 1 ≤ t) (inputLarge : (20 * (t + 1)) ^ (depth - 1) ≤ n) : 2 ^ (t + 1) ≤ 20 * t * Program.cost andOrCost circuit.program

Compatibility wrapper for the checked input-negation presentation.