Iterated AC0 depth reduction with variable parameters

The source-faithful parity argument uses a different first restriction from its later restrictions: the first round starts from literal width one, while subsequent rounds start from the chosen tree bound. This module iterates the existential layer theorem with explicit schedules

• treeBound i for the invariant after i rounds,
• p i for the next random restriction, and
• retained i for the guaranteed live-variable count.

At each round the caller supplies the exact switching failure and first-moment inequalities. The resulting theorem constructs one cumulative restriction by finite induction. It is purely structural and does not choose asymptotic parameters, enumerate circuits, or search for witnesses.

theorem Algebraic.AC0.Program.layerFailureBoundOfBounds_ne_top {n g : ℕ} (program : Program signature n g) (p : NNReal) (sourceBound targetBound : ℕ) : layerFailureBoundOfBounds program p sourceBound targetBound ≠ ⊤

The charged two-parameter switching failure bound is finite.

theorem Algebraic.AC0.Program.exists_shallowUpTo_with_liveCount_bounds_raw {n g : ℕ} (program : Program signature n g) (rounds : ℕ) (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, layerFailureBoundOfBounds program (p level) (treeBound level) (treeBound (level + 1)) ≤ ↑(p level)) (room : ∀ level < rounds, layerFailureBoundOfBounds program (p level) (treeBound level) (treeBound (level + 1)) * ↑(retained level) + ↑(retained (level + 1)) < ↑(p level) * ↑(retained level)) : ∃ (rho : PartialAssignment n), ShallowUpTo program rho rounds (treeBound rounds) ∧ retained rounds ≤ rho.liveCount

Iterated semantic depth reduction along explicit restriction, tree-bound, and survivor schedules. The result is one cumulative restriction satisfying the scheduled final invariant. This raw form permits arbitrary internal NOT gates.

theorem Algebraic.AC0.Program.exists_shallowUpTo_with_liveCount_bounds {n g : ℕ} (program : Program signature n g) (_normal : NegationsAtInputs program) (rounds : ℕ) (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, layerFailureBoundOfBounds program (p level) (treeBound level) (treeBound (level + 1)) ≤ ↑(p level)) (room : ∀ level < rounds, layerFailureBoundOfBounds program (p level) (treeBound level) (treeBound (level + 1)) * ↑(retained level) + ↑(retained (level + 1)) < ↑(p level) * ↑(retained level)) : ∃ (rho : PartialAssignment n), ShallowUpTo program rho rounds (treeBound rounds) ∧ retained rounds ≤ rho.liveCount

Compatibility wrapper for the checked input-negation presentation.