Variable-parameter depth reduction for parity circuits

This module composes the variable-parameter layer iterator with the parity top-gate obstruction. A circuit of logical depth at most rounds + 1 needs only rounds restriction steps: the final unreduced AND or OR is handled as a bounded-width normal form.

Under the explicit per-round switching and survivor inequalities, any parity circuit forces retained rounds <= treeBound rounds. If the chosen schedule ends above that tree bound, the circuit cannot compute parity. This is the complete structural contradiction with the source-faithful d - 1 round count; selecting closed-form parameters remains a separate arithmetic task.

theorem Algebraic.AC0.Circuit.retained_le_treeBound_of_iterated_parity_raw {n : ℕ} (circuit : Circuit signature n 1) (computes : circuit.ComputesWith interpretation (Parity.target n)) (rounds : ℕ) (circuitDepth : logicalDepth circuit ≤ rounds + 1) (treeBound : ℕ → ℕ) (oneLeInitialBound : 1 ≤ treeBound 0) (p : ℕ → NNReal) (atMostOne : ∀ level < rounds, p level ≤ 1) (boundMonotone : ∀ level < rounds, treeBound level ≤ treeBound (level + 1)) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : ∀ level < rounds, Program.layerFailureBoundOfBounds circuit.program (p level) (treeBound level) (treeBound (level + 1)) ≤ ↑(p level)) (room : ∀ level < rounds, Program.layerFailureBoundOfBounds circuit.program (p level) (treeBound level) (treeBound (level + 1)) * ↑(retained level) + ↑(retained (level + 1)) < ↑(p level) * ↑(retained level)) : retained rounds ≤ treeBound rounds

A depth-rounds + 1 parity circuit satisfying an explicit reduction schedule forces the final survivor count below the final tree bound, with no restriction on the placement of NOT gates.

theorem Algebraic.AC0.Circuit.retained_le_treeBound_of_iterated_parity {n : ℕ} (circuit : Circuit signature n 1) (_normal : Program.NegationsAtInputs circuit.program) (computes : circuit.ComputesWith interpretation (Parity.target n)) (rounds : ℕ) (circuitDepth : logicalDepth circuit ≤ rounds + 1) (treeBound : ℕ → ℕ) (oneLeInitialBound : 1 ≤ treeBound 0) (p : ℕ → NNReal) (atMostOne : ∀ level < rounds, p level ≤ 1) (boundMonotone : ∀ level < rounds, treeBound level ≤ treeBound (level + 1)) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : ∀ level < rounds, Program.layerFailureBoundOfBounds circuit.program (p level) (treeBound level) (treeBound (level + 1)) ≤ ↑(p level)) (room : ∀ level < rounds, Program.layerFailureBoundOfBounds circuit.program (p level) (treeBound level) (treeBound (level + 1)) * ↑(retained level) + ↑(retained (level + 1)) < ↑(p level) * ↑(retained level)) : retained rounds ≤ treeBound rounds

Compatibility wrapper for the checked input-negation presentation.

theorem Algebraic.AC0.Circuit.not_computes_parity_of_iterated_switching_below_top_raw {n : ℕ} (circuit : Circuit signature n 1) (rounds : ℕ) (circuitDepth : logicalDepth circuit ≤ rounds + 1) (treeBound : ℕ → ℕ) (oneLeInitialBound : 1 ≤ treeBound 0) (p : ℕ → NNReal) (atMostOne : ∀ level < rounds, p level ≤ 1) (boundMonotone : ∀ level < rounds, treeBound level ≤ treeBound (level + 1)) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : ∀ level < rounds, Program.layerFailureBoundOfBounds circuit.program (p level) (treeBound level) (treeBound (level + 1)) ≤ ↑(p level)) (room : ∀ level < rounds, Program.layerFailureBoundOfBounds circuit.program (p level) (treeBound level) (treeBound (level + 1)) * ↑(retained level) + ↑(retained (level + 1)) < ↑(p level) * ↑(retained level)) (tooMany : treeBound rounds < retained rounds) : ¬circuit.ComputesWith interpretation (Parity.target n)

Parameterized rounds-step parity lower bound with one unreduced top layer: a schedule ending above its final tree allowance rules out the circuit, with arbitrary internal NOT gates.

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

Compatibility wrapper for the checked input-negation presentation.