Iterated semantic AC0 depth reduction

This module iterates the existential one-layer switching step. A schedule retained i specifies a lower bound on the number of live variables after logical layer i. It suffices to check, for every layer below the target depth,

delta * retained i + retained (i + 1) < p * retained i,

where delta is the charged one-step failure bound, together with delta <= p. A monotonicity lemma lifts this scheduled inequality to the possibly larger live count produced at runtime. Finite induction then yields one cumulative restriction satisfying the semantic shallow-tree invariant at the target depth and the final survivor bound.

The theorem remains parametric in the numerical schedule. Choosing and simplifying source-facing parameters is deliberately separated from the structural iteration proof.

theorem Algebraic.AC0.Program.layerRoom_mono {delta p : ENNReal} {minimum current next : ℕ} (deltaFinite : delta ≠ ⊤) (deltaLe : delta ≤ p) (minimumLe : minimum ≤ current) (room : delta * ↑minimum + ↑next < p * ↑minimum) : delta * ↑current + ↑next < p * ↑current

The first-moment room inequality is monotone in the current live count when the bad-event bound is at most the survival probability.

theorem Algebraic.AC0.Program.layerFailureBound_ne_top {n g : ℕ} (program : Program signature n g) (p : NNReal) (bound : ℕ) : layerFailureBound program p bound ≠ ⊤

The explicit charged switching failure bound is finite.

theorem Algebraic.AC0.Program.exists_shallowUpTo_with_liveCount_raw {n g : ℕ} (program : Program signature n g) (depth bound : ℕ) (oneLeBound : 1 ≤ bound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : layerFailureBound program p bound ≤ ↑p) (room : ∀ level < depth, layerFailureBound program p bound * ↑(retained level) + ↑(retained (level + 1)) < ↑p * ↑(retained level)) : ∃ (rho : PartialAssignment n), ShallowUpTo program rho depth bound ∧ retained depth ≤ rho.liveCount

Iterated semantic depth reduction along an explicit survivor schedule. The result is one cumulative restriction, not a sampled or searched-for witness. This raw form permits arbitrary internal NOT gates.

theorem Algebraic.AC0.Program.exists_shallowUpTo_with_liveCount {n g : ℕ} (program : Program signature n g) (_normal : NegationsAtInputs program) (depth bound : ℕ) (oneLeBound : 1 ≤ bound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ → ℕ) (initial : retained 0 ≤ n) (failureLe : layerFailureBound program p bound ≤ ↑p) (room : ∀ level < depth, layerFailureBound program p bound * ↑(retained level) + ↑(retained (level + 1)) < ↑p * ↑(retained level)) : ∃ (rho : PartialAssignment n), ShallowUpTo program rho depth bound ∧ retained depth ≤ rho.liveCount

Compatibility wrapper for the checked input-negation presentation.