AC0 layer switching with separate source and target bounds

The first restriction in the standard parity lower-bound argument starts from the width-one literal layer but aims for decision-tree depth t. Later rounds start and end at depth t. This module therefore separates the incoming normal-form width sourceBound from the desired outgoing decision-tree depth targetBound.

For sourceBound <= targetBound, one logical layer advances except with probability at most

andOrCost(program) * (5 * p * sourceBound)^(targetBound + 1).

Keeping these parameters distinct is quantitatively essential: charging the first round as though its source width were already t would introduce an artificial extra factor of t and lose the standard depth exponent. The proof uses the same exact semantic switching and finite union bounds as the equal-bound theorem; it performs no circuit search or finite experiment.

theorem Algebraic.AC0.Program.ShallowUpTo.succ_of_connective_bounds_raw {n g : ℕ} {program : Program signature n g} {rho extension : PartialAssignment n} {level sourceBound targetBound : ℕ} (shallow : ShallowUpTo program rho level sourceBound) (sourceLeTarget : sourceBound ≤ targetBound) (next : ∀ gate ∈ connectiveGates program, logicalGateDepths program gate ≤ level + 1 → DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) targetBound) : ShallowUpTo program (rho.refine extension) (level + 1) targetBound

Advance the shallow invariant when old layers have a possibly smaller bound than the newly exposed layer. Arbitrary internal NOT gates are handled by the raw one-bound successor theorem.

theorem Algebraic.AC0.Program.ShallowUpTo.succ_of_connective_bounds {n g : ℕ} {program : Program signature n g} {rho extension : PartialAssignment n} {level sourceBound targetBound : ℕ} (_normal : NegationsAtInputs program) (shallow : ShallowUpTo program rho level sourceBound) (sourceLeTarget : sourceBound ≤ targetBound) (next : ∀ gate ∈ connectiveGates program, logicalGateDepths program gate ≤ level + 1 → DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) targetBound) : ShallowUpTo program (rho.refine extension) (level + 1) targetBound

Compatibility wrapper for the checked input-negation presentation.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_gate_not_depthAtMost_refine_le_five_bounds {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level sourceBound targetBound : ℕ} (shallow : ShallowUpTo program rho level sourceBound) (gate : Fin g) (connective : gate ∈ connectiveGates program) (gateDepth : logicalGateDepths program gate ≤ level + 1) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) targetBound) ≤ (5 * ↑p * ↑sourceBound) ^ (targetBound + 1)

A gate represented by source-width normal form fails the target tree-depth bound with the two-parameter switching-lemma estimate.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_gate_in_nextLayer_not_depthAtMost_refine_le_five_bounds {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level sourceBound targetBound : ℕ} (shallow : ShallowUpTo program rho level sourceBound) (gate : Fin g) (connective : gate ∈ connectiveGates program) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => logicalGateDepths program gate ≤ level + 1 ∧ ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) targetBound) ≤ (5 * ↑p * ↑sourceBound) ^ (targetBound + 1)

The next-layer event for one charged gate satisfies the two-parameter bound; gates outside that layer contribute the empty event.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_exists_connective_in_nextLayer_not_depthAtMost_refine_le_five_bounds {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level sourceBound targetBound : ℕ} (shallow : ShallowUpTo program rho level sourceBound) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ∃ gate ∈ connectiveGates program, logicalGateDepths program gate ≤ level + 1 ∧ ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) (rho.refine extension)) targetBound) ≤ ↑(Program.cost andOrCost program) * (5 * ↑p * ↑sourceBound) ^ (targetBound + 1)

Union bound over the connective gates in the next layer, retaining separate source-width and target-depth parameters.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_not_succ_refine_le_five_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) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ¬ShallowUpTo program (rho.refine extension) (level + 1) targetBound) ≤ ↑(Program.cost andOrCost program) * (5 * ↑p * ↑sourceBound) ^ (targetBound + 1)

One random restriction advances the semantic invariant from source bound sourceBound to target bound targetBound, except with the standard charged two-parameter switching probability. This raw form permits arbitrary internal NOT gates.

theorem Algebraic.AC0.Program.ShallowUpTo.probability_not_succ_refine_le_five_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) : (RandomRestriction.probability n p atMostOne fun (extension : PartialAssignment n) => ¬ShallowUpTo program (rho.refine extension) (level + 1) targetBound) ≤ ↑(Program.cost andOrCost program) * (5 * ↑p * ↑sourceBound) ^ (targetBound + 1)

Compatibility wrapper for the checked input-negation presentation.