Simultaneous switching for bounded bottom gates

This module connects shared AC0 programs to the finite-family switching lemma. It indexes by all g internal gates. Each eligible depth-one gate of fan-in at most t is represented by its exact bounded DNF or CNF; every other index is padded by a constant formula. Thus the union bound costs at most g, without enumerating a subtype of gates or unfolding the shared circuit into a formula.

The public endpoint bounds the probability that any eligible internal gate's restricted scalar function lacks a shallow decision tree. This is the simultaneous bottom-layer estimate needed before an explicit gate-replacement construction.

def Algebraic.AC0.Program.IsBoundedBottomAnd {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : Prop

The indexed gate is a logical-depth-one AND of fan-in at most the stated bound.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.AC0.Program.IsBoundedBottomOr {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : Prop

The indexed gate is a logical-depth-one OR of fan-in at most the stated bound.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Algebraic.AC0.Program.isBoundedBottomAndDecidable {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : Decidable (IsBoundedBottomAnd program widthBound gate)

Bounded bottom-AND membership is decidable from the stored line.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Algebraic.AC0.Program.isBoundedBottomOrDecidable {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : Decidable (IsBoundedBottomOr program widthBound gate)

Bounded bottom-OR membership is decidable from the stored line.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.AC0.Program.isBoundedBottomAnd_iff_exists {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : IsBoundedBottomAnd program widthBound gate ↔ ∃ (fanIn : ℕ), (program.lines gate).op = Op.and fanIn ∧ logicalGateDepths program gate = 1 ∧ fanIn ≤ widthBound

Existential fan-in characterization of a bounded bottom AND gate.

theorem Algebraic.AC0.Program.isBoundedBottomOr_iff_exists {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : IsBoundedBottomOr program widthBound gate ↔ ∃ (fanIn : ℕ), (program.lines gate).op = Op.or fanIn ∧ logicalGateDepths program gate = 1 ∧ fanIn ≤ widthBound

Existential fan-in characterization of a bounded bottom OR gate.

def Algebraic.AC0.Program.RepresentsBoundedBottomAnd {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) (formula : DNF n) : Prop

A bounded DNF represents an eligible bottom AND gate exactly.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.AC0.Program.RepresentsBoundedBottomOr {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) (formula : CNF n) : Prop

A bounded CNF represents an eligible bottom OR gate exactly.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.AC0.Program.exists_representsBoundedBottomAnd {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound : ℕ) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (depthOne : logicalGateDepths program gate = 1) (bounded : fanIn ≤ widthBound) : ∃ (formula : DNF n), RepresentsBoundedBottomAnd program widthBound gate formula

Every eligible bottom AND gate has a bounded DNF representation.

theorem Algebraic.AC0.Program.exists_representsBoundedBottomOr {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound : ℕ) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (depthOne : logicalGateDepths program gate = 1) (bounded : fanIn ≤ widthBound) : ∃ (formula : CNF n), RepresentsBoundedBottomOr program widthBound gate formula

Every eligible bottom OR gate has a bounded CNF representation.

noncomputable def Algebraic.AC0.Program.paddedAndBottomFormula {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : DNF n

Choose an exact bounded DNF for an eligible gate, and use constant false at every other program index.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.AC0.Program.paddedOrBottomFormula {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : CNF n

Choose an exact bounded CNF for an eligible gate, and use constant true at every other program index.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.AC0.Program.paddedAndBottomFormula_widthAtMost {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : (paddedAndBottomFormula program widthBound gate).WidthAtMost widthBound

Every member of the padded AND family has the common width bound.

theorem Algebraic.AC0.Program.paddedOrBottomFormula_widthAtMost {n g : ℕ} (program : Program signature n g) (widthBound : ℕ) (gate : Fin g) : (paddedOrBottomFormula program widthBound gate).WidthAtMost widthBound

Every member of the padded OR family has the common width bound.

theorem Algebraic.AC0.Program.paddedAndBottomFormula_eval_of_bottom {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound : ℕ) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (depthOne : logicalGateDepths program gate = 1) (bounded : fanIn ≤ widthBound) (input : Fin n → Bool) : (paddedAndBottomFormula program widthBound gate).eval input = program.gateFunction interpretation gate input

At an eligible AND gate, the padded formula computes the internal gate function.

theorem Algebraic.AC0.Program.paddedOrBottomFormula_eval_of_bottom {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound : ℕ) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (depthOne : logicalGateDepths program gate = 1) (bounded : fanIn ≤ widthBound) (input : Fin n → Bool) : (paddedOrBottomFormula program widthBound gate).eval input = program.gateFunction interpretation gate input

At an eligible OR gate, the padded formula computes the internal gate function.

theorem Algebraic.AC0.Program.paddedAndBottomFormula_restrict_eval_of_bottom {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound : ℕ) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.and fanIn) (depthOne : logicalGateDepths program gate = 1) (bounded : fanIn ≤ widthBound) (rho : PartialAssignment n) : ((paddedAndBottomFormula program widthBound gate).restrict rho).eval = ScalarFunction.restrict (program.gateFunction interpretation gate) rho

Restricting the padded AND formula agrees with semantic restriction of the internal gate function.

theorem Algebraic.AC0.Program.paddedOrBottomFormula_restrict_eval_of_bottom {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound : ℕ) (gate : Fin g) {fanIn : ℕ} (operation : (program.lines gate).op = Op.or fanIn) (depthOne : logicalGateDepths program gate = 1) (bounded : fanIn ≤ widthBound) (rho : PartialAssignment n) : ((paddedOrBottomFormula program widthBound gate).restrict rho).eval = ScalarFunction.restrict (program.gateFunction interpretation gate) rho

Restricting the padded OR formula agrees with semantic restriction of the internal gate function.

theorem Algebraic.AC0.Program.probability_exists_boundedBottomAnd_depthAtLeast_restrict_le_five {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (gate : Fin g), IsBoundedBottomAnd program widthBound gate ∧ DecisionTree.DepthAtLeast (ScalarFunction.restrict (program.gateFunction interpretation gate) rho) pathLength) ≤ ↑g * (5 * ↑p * ↑widthBound) ^ pathLength

Simultaneous switching bound for all bounded bottom AND gates in a shared program.

theorem Algebraic.AC0.Program.probability_exists_boundedBottomOr_depthAtLeast_restrict_le_five {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (gate : Fin g), IsBoundedBottomOr program widthBound gate ∧ DecisionTree.DepthAtLeast (ScalarFunction.restrict (program.gateFunction interpretation gate) rho) pathLength) ≤ ↑g * (5 * ↑p * ↑widthBound) ^ pathLength

Simultaneous switching bound for all bounded bottom OR gates in a shared program.

theorem Algebraic.AC0.Program.probability_exists_boundedBottomAnd_not_depthAtMost_restrict_le_five {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound depthBound : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (gate : Fin g), IsBoundedBottomAnd program widthBound gate ∧ ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) rho) depthBound) ≤ ↑g * (5 * ↑p * ↑widthBound) ^ (depthBound + 1)

Off-by-one shallow-tree form for all bounded bottom AND gates.

theorem Algebraic.AC0.Program.probability_exists_boundedBottomOr_not_depthAtMost_restrict_le_five {n g : ℕ} (program : Program signature n g) (normal : NegationsAtInputs program) (widthBound depthBound : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (RandomRestriction.probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (gate : Fin g), IsBoundedBottomOr program widthBound gate ∧ ¬DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) rho) depthBound) ≤ ↑g * (5 * ↑p * ↑widthBound) ^ (depthBound + 1)

Off-by-one shallow-tree form for all bounded bottom OR gates.