The top-gate obstruction for parity circuits

Standard AC0 depth reduction stops one layer below the circuit output. If the output already lies in the reduced layers, restricted parity's exact decision-tree depth gives the contradiction. Otherwise the output is a genuine next-layer connective: an OR has a bounded-width DNF and an AND has a bounded-width CNF, so the restricted-parity normal-form lower bound applies.

This module packages that case split without assuming that the designated output is syntactically a top AND or OR. Input outputs and input negations are handled by their logical depth. Thus a depth-i+1 parity circuit whose wires through depth i are shallow leaves at most the common tree bound many variables live.

theorem Algebraic.AC0.Program.ShallowUpTo.parityUpToNegation_liveCount_le {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (wire : Wire n g) (wireDepth : logicalWireDepths program wire ≤ level) (phase : Parity.UpToNegation (program.wireFunction interpretation wire)) : rho.liveCount ≤ bound

A shallow invariant covering a wire that computes parity or complemented parity forces the live count below the common tree-depth allowance.

theorem Algebraic.AC0.Program.liveCount_le_of_shallowBelow_computes_parityUpToNegation {n g : ℕ} {program : Program signature n g} {rho : PartialAssignment n} {level bound : ℕ} (shallow : ShallowUpTo program rho level bound) (wire : Wire n g) (wireDepth : logicalWireDepths program wire ≤ level + 1) (phase : Parity.UpToNegation (program.wireFunction interpretation wire)) : rho.liveCount ≤ bound

If a wire at most one logical layer above a shallow prefix computes parity up to output negation, then at most the tree bound many variables are live. The proof follows arbitrary NOT chains backwards until it reaches an input, an already-shallow wire, or a connective gate.

theorem Algebraic.AC0.Circuit.liveCount_le_of_shallowBelowTop_computes_parity_raw {n : ℕ} {circuit : Circuit signature n 1} {rho : PartialAssignment n} {level bound : ℕ} (computes : circuit.ComputesWith interpretation (Parity.target n)) (depthBound : logicalDepth circuit ≤ level + 1) (shallow : Program.ShallowUpTo circuit.program rho level bound) : rho.liveCount ≤ bound

Reducing all but the possible top logical layer of a parity circuit is enough to bound its remaining live variables, even with arbitrary internal NOT gates.

theorem Algebraic.AC0.Circuit.liveCount_le_of_shallowBelowTop_computes_parity {n : ℕ} {circuit : Circuit signature n 1} {rho : PartialAssignment n} {level bound : ℕ} (_normal : Program.NegationsAtInputs circuit.program) (computes : circuit.ComputesWith interpretation (Parity.target n)) (depthBound : logicalDepth circuit ≤ level + 1) (shallow : Program.ShallowUpTo circuit.program rho level bound) : rho.liveCount ≤ bound

Compatibility wrapper for the checked input-negation presentation.