Semantic AC0 layer invariants

The standard switching-lemma application advances a semantic invariant: after a cumulative restriction, every wire through logical layer i is computed by a decision tree of a common shallow depth. This module defines that invariant, proves its restriction stability and its depth-zero literal base case, and shows that every argument of a connective gate comes from a strictly earlier logical layer.

It also identifies the finite set of AND/OR gates with the source-facing AC0 cost exactly. Later union bounds can therefore charge the mathematical circuit size rather than the raw program gate count, which may include free input negations.

def Algebraic.AC0.Program.connectiveGates {n g : ℕ} (program : Program signature n g) : Finset (Fin g)

The internal gates charged by the source AC0 size measure.

Equations

• Algebraic.AC0.Program.connectiveGates program = {gate : Fin g | Algebraic.AC0.Op.connective (program.lines gate).op ≠ none}

@[simp]

theorem Algebraic.AC0.Program.mem_connectiveGates {n g : ℕ} (program : Program signature n g) (gate : Fin g) : gate ∈ connectiveGates program ↔ Op.connective (program.lines gate).op ≠ none

theorem Algebraic.AC0.Program.andOrCost_eq_indicator (operation : Op) : andOrCost operation = if operation.connective ≠ none then 1 else 0

AC0 operation cost is the indicator of being an AND or OR gate.

theorem Algebraic.AC0.Program.card_connectiveGates {n g : ℕ} (program : Program signature n g) : (connectiveGates program).card = Program.cost andOrCost program

The charged AC0 cost is exactly the number of connective gates.

def Algebraic.AC0.Literal.decisionTree {n : ℕ} (literal : Literal n) : DecisionTree n

The one-query decision tree computing a literal.

Equations

• literal.decisionTree = Algebraic.AC0.DecisionTree.query literal.index (Algebraic.AC0.DecisionTree.leaf !literal.value) (Algebraic.AC0.DecisionTree.leaf literal.value)

@[simp]

theorem Algebraic.AC0.Literal.decisionTree_eval {n : ℕ} (literal : Literal n) (input : Fin n → Bool) : literal.decisionTree.eval input = literal.eval input

The literal tree has exactly the expected Boolean semantics.

@[simp]

theorem Algebraic.AC0.Literal.decisionTree_depth {n : ℕ} (literal : Literal n) : literal.decisionTree.depth = 1

A literal decision tree has depth one.

theorem Algebraic.AC0.Literal.depthAtMost_eval {n : ℕ} (literal : Literal n) : DecisionTree.DepthAtMost literal.eval 1

Every literal function has semantic decision-tree depth at most one.

def Algebraic.AC0.Program.ShallowUpTo {n g : ℕ} (program : Program signature n g) (rho : PartialAssignment n) (level bound : ℕ) : Prop

After rho, every wire up through level has a decision tree of depth at most bound. This is the semantic induction invariant used in the standard switching-lemma application.

Equations

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

theorem Algebraic.AC0.Program.ShallowUpTo.restrict {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (extension : PartialAssignment n) : ShallowUpTo program (rho.refine extension) level bound

Further restricting inputs preserves a semantic layer-depth bound.

theorem Algebraic.AC0.Program.shallowUpTo_zero_raw {n g : ℕ} (program : Program signature n g) (rho : PartialAssignment n) : ShallowUpTo program rho 0 1

Original inputs and arbitrary chains of NOT gates establish the depth-zero base of the semantic layer invariant.

theorem Algebraic.AC0.Program.shallowUpTo_zero {n g : ℕ} (program : Program signature n g) (_normal : NegationsAtInputs program) (rho : PartialAssignment n) : ShallowUpTo program rho 0 1

Original inputs and checked input negations establish the depth-zero base of the semantic layer invariant.

theorem Algebraic.AC0.Program.argument_logicalWireDepth_lt_gateDepth {n g : ℕ} (program : Program signature n g) (gate : Fin g) (connective : Op.connective (program.lines gate).op ≠ none) (argument : Fin (arity (program.lines gate).op)) : logicalWireDepths program ((program.lines gate).wires argument) < logicalGateDepths program gate

Each argument of an AND or OR gate has strictly smaller source logical depth than the gate itself.

theorem Algebraic.AC0.Program.argument_logicalWireDepth_le_of_gateDepth_le_succ {n g : ℕ} (program : Program signature n g) (gate : Fin g) (level : ℕ) (connective : Op.connective (program.lines gate).op ≠ none) (gateDepth : logicalGateDepths program gate ≤ level + 1) (argument : Fin (arity (program.lines gate).op)) : logicalWireDepths program ((program.lines gate).wires argument) ≤ level

If a connective gate is in the next logical layer, each argument lies in the current layer or below.

theorem Algebraic.AC0.Program.ShallowUpTo.argument {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) (connective : Op.connective (program.lines gate).op ≠ none) (gateDepth : logicalGateDepths program gate ≤ level + 1) (argument : Fin (arity (program.lines gate).op)) : DecisionTree.DepthAtMost (ScalarFunction.restrict (program.wireFunction interpretation ((program.lines gate).wires argument)) rho) bound

A layer invariant supplies a shallow tree for every argument of a connective gate in the next layer.

theorem Algebraic.AC0.Program.ShallowUpTo.gate {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (gate : Fin g) (gateDepth : logicalGateDepths program gate ≤ level) : DecisionTree.DepthAtMost (ScalarFunction.restrict (program.gateFunction interpretation gate) rho) bound

The invariant specializes to any internal gate in the covered layers.