Existential AC0 layer advancement with live variables

The probabilistic switching theorem is useful for depth reduction only after one extracts a concrete refinement that both advances the semantic layer invariant and keeps enough variables live. This module performs exactly that averaging step.

For current live count m, requested survivor count k, and charged switching failure bound delta, the sole numerical premise is

delta * m + k < p * m.

No restriction is computed or searched for: existence follows from the exact first moment of the survivor count and the proved bad-event probability.

theorem Algebraic.AC0.Program.ShallowUpTo.mono {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level smaller larger : ℕ} (shallow : ShallowUpTo program rho level smaller) (le : smaller ≤ larger) : ShallowUpTo program rho level larger

Increasing the common tree-depth allowance preserves the semantic layer invariant.

noncomputable def Algebraic.AC0.Program.layerFailureBound {n g : ℕ} (program : Program signature n g) (p : NNReal) (bound : ℕ) : ENNReal

Charged-size failure bound for one semantic switching step.

Equations

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

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

A one-step switching estimate plus sufficient first-moment room produces one refinement that advances the invariant and retains the requested number of live variables. This raw form permits arbitrary internal NOT gates.

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

Compatibility wrapper for the checked input-negation presentation.