Existential AC0 layer advancement with separate bounds

This module combines two-parameter layer switching with exact live-variable averaging. If the current invariant has source bound s and the next layer should have target bound t >= s, define

delta = andOrCost(program) * (5 * p * s)^(t + 1).

Whenever delta * m + k < p * m, where m is the current live count, there exists a refinement that advances one layer at target bound t and leaves at least k variables live. This is an existence theorem from a proved first moment, not a search procedure.

noncomputable def Algebraic.AC0.Program.layerFailureBoundOfBounds {n g : ℕ} (program : Program signature n g) (p : NNReal) (sourceBound targetBound : ℕ) : ENNReal

Charged-size switching failure bound with distinct incoming normal-form width and outgoing decision-tree depth.

Equations

• Algebraic.AC0.Program.layerFailureBoundOfBounds program p sourceBound targetBound = ↑(Cslib.Circuits.Program.cost Algebraic.AC0.andOrCost program) * (5 * ↑p * ↑sourceBound) ^ (targetBound + 1)

theorem Algebraic.AC0.Program.layerFailureBoundOfBounds_self {n g : ℕ} (program : Program signature n g) (p : NNReal) (bound : ℕ) : layerFailureBoundOfBounds program p bound bound = layerFailureBound program p bound

The two-parameter failure bound specializes to the original common-bound definition.

theorem Algebraic.AC0.Program.ShallowUpTo.exists_refine_succ_with_liveCount_bounds_raw {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level sourceBound targetBound : ℕ} (shallow : ShallowUpTo program rho level sourceBound) (sourceLeTarget : sourceBound ≤ targetBound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ) (room : layerFailureBoundOfBounds program p sourceBound targetBound * ↑rho.liveCount + ↑retained < ↑p * ↑rho.liveCount) : ∃ (extension : PartialAssignment n), ShallowUpTo program (rho.refine extension) (level + 1) targetBound ∧ retained ≤ (rho.refine extension).liveCount

Sufficient first-moment room produces a refinement that advances from the source bound to the target bound while retaining the requested live count. This raw form permits arbitrary internal NOT gates.

theorem Algebraic.AC0.Program.ShallowUpTo.exists_refine_succ_with_liveCount_bounds {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level sourceBound targetBound : ℕ} (_normal : NegationsAtInputs program) (shallow : ShallowUpTo program rho level sourceBound) (sourceLeTarget : sourceBound ≤ targetBound) (p : NNReal) (atMostOne : p ≤ 1) (retained : ℕ) (room : layerFailureBoundOfBounds program p sourceBound targetBound * ↑rho.liveCount + ↑retained < ↑p * ↑rho.liveCount) : ∃ (extension : PartialAssignment n), ShallowUpTo program (rho.refine extension) (level + 1) targetBound ∧ retained ≤ (rho.refine extension).liveCount

Compatibility wrapper for the checked input-negation presentation.