Ratio schedules for AC0 depth reduction

The raw layer iterator asks separately for a failure bound and the strict first-moment room inequality. Parameter calculations are clearer when each round instead specifies a retained fraction q with

delta + q < p and a_(i+1) <= q * a_i.

For a positive current survivor count, these two inequalities imply the exact room condition. This module packages that elementary implication and lifts it to a complete schedule theorem. It separates the conceptual probability slack from later concrete choices of constants and integer rounding.

theorem Algebraic.AC0.Program.layerRoom_of_slack {delta q p : ENNReal} {current next : ℕ} (currentPositive : 0 < current) (slack : delta + q < p) (nextLe : ↑next ≤ q * ↑current) : delta * ↑current + ↑next < p * ↑current

Probability slack plus a multiplicative survivor target implies the strict first-moment room inequality.

theorem Algebraic.AC0.Program.failureLe_of_slack {delta q p : ENNReal} (slack : delta + q < p) : delta ≤ p

A strict slack inequality includes the non-strict failure bound required for monotonicity in the actual live count.

theorem Algebraic.AC0.Program.exists_shallowUpTo_with_liveCount_of_slack {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) (retainedPositive : ∀ level < rounds, 0 < retained level) (q : ℕ → ENNReal) (slack : ∀ level < rounds, layerFailureBoundOfBounds program (p level) (treeBound level) (treeBound (level + 1)) + q level < ↑(p level)) (shrinks : ∀ level < rounds, ↑(retained (level + 1)) ≤ q level * ↑(retained level)) : ∃ (rho : PartialAssignment n), ShallowUpTo program rho rounds (treeBound rounds) ∧ retained rounds ≤ rho.liveCount

Iterated depth reduction from multiplicative survivor ratios and explicit probability slack.