Integral size arithmetic for the AC0 parity lower bound

The concrete depth-reduction theorem states its switching smallness condition in exact finite probabilities. This module proves that, for t >= 1, it is equivalent to the natural-number inequality

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

Thus the finite parity lower bound can be consumed without any NNReal or ENNReal arithmetic: the size inequality above and the survivor inequality t < n / (20 * (20t)^(d-2)) suffice. Denominator cancellation is proved symbolically in the nonnegative reals and transported through the exact order embedding into extended nonnegative reals.

theorem Algebraic.AC0.ParityParameters.switchingFailure_eq_coe {n g : ℕ} (program : Program signature n g) (t : ℕ) : switchingFailure program t = ↑(↑(Program.cost andOrCost program) * (1 / 2) ^ (t + 1))

The extended-real switching failure is the coercion of the corresponding finite nonnegative-real expression.

theorem Algebraic.AC0.ParityParameters.switchingFailure_lt_minimum_nnreal {n g : ℕ} (program : Program signature n g) (t : ℕ) (oneLe : 1 ≤ t) (small : 20 * t * Program.cost andOrCost program < 2 ^ (t + 1)) : ↑(Program.cost andOrCost program) * (1 / 2) ^ (t + 1) < minimumRatio t

Integral size smallness implies the finite nonnegative-real probability inequality.

theorem Algebraic.AC0.ParityParameters.switchingFailure_lt_minimum_nnreal_iff {n g : ℕ} (program : Program signature n g) (t : ℕ) (oneLe : 1 ≤ t) : ↑(Program.cost andOrCost program) * (1 / 2) ^ (t + 1) < minimumRatio t ↔ 20 * t * Program.cost andOrCost program < 2 ^ (t + 1)

Exact finite-real equivalence between switching smallness and the integral size inequality.

theorem Algebraic.AC0.ParityParameters.switchingFailure_lt_minimum_of_nat {n g : ℕ} (program : Program signature n g) (t : ℕ) (oneLe : 1 ≤ t) (small : 20 * t * Program.cost andOrCost program < 2 ^ (t + 1)) : switchingFailure program t < ↑(minimumRatio t)

Natural-number size smallness supplies the exact extended-real condition used by depth reduction.

theorem Algebraic.AC0.ParityParameters.switchingFailure_lt_minimum_iff {n g : ℕ} (program : Program signature n g) (t : ℕ) (oneLe : 1 ≤ t) : switchingFailure program t < ↑(minimumRatio t) ↔ 20 * t * Program.cost andOrCost program < 2 ^ (t + 1)

Exact extended-real equivalence with the integral size inequality.

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

Fully integral finite AC0 parity lower bound, allowing arbitrary internal NOT gates without changing the AND/OR cost.

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

Compatibility wrapper for the checked input-negation presentation.