Parity under partial assignments

This module proves the exact decision-tree resilience of parity needed by the AC0 lower bound. It reuses the library's canonical Boolean-ring parity function from the gate-elimination development.

For every partial assignment rho, the restricted parity function has deterministic decision-tree depth exactly rho.liveCount. The lower bound is an adversary argument on one evaluation path: flipping any live coordinate changes parity, so every live coordinate must occur among that path's queries. The matching upper bound is the structural Shannon tree over the live coordinates.

def Algebraic.AC0.Parity.function (n : ℕ) : ScalarFunction Bool n

Canonical parity scalar function, reusing the gate-elimination definition.

Equations

• Algebraic.AC0.Parity.function n = Algebraic.GateElimination.Xor.parity

def Algebraic.AC0.Parity.target (n : ℕ) : Target Bool n 1

Parity as a one-output circuit target.

Equations

• Algebraic.AC0.Parity.target n = Algebraic.GateElimination.Xor.parityTarget n

@[simp]

theorem Algebraic.AC0.Parity.target_apply {n : ℕ} (input : Fin n → Bool) (output : Fin 1) : target n input output = function n input

def Algebraic.AC0.Parity.targetFamily : Target.Family Bool 1

The all-input-width family of parity targets.

Equations

• Algebraic.AC0.Parity.targetFamily = Algebraic.AC0.Parity.target

@[simp]

theorem Algebraic.AC0.Parity.targetFamily_apply (n : ℕ) : targetFamily n = target n

def Algebraic.AC0.Parity.flip {n : ℕ} (input : Fin n → Bool) (selected : Fin n) : Fin n → Bool

Flip one coordinate of a Boolean input.

Equations

• Algebraic.AC0.Parity.flip input selected index = if index = selected then !input index else input index

@[simp]

theorem Algebraic.AC0.Parity.flip_selected {n : ℕ} (input : Fin n → Bool) (selected : Fin n) : flip input selected selected = !input selected

theorem Algebraic.AC0.Parity.flip_other {n : ℕ} (input : Fin n → Bool) (selected index : Fin n) (different : index ≠ selected) : flip input selected index = input index

theorem Algebraic.AC0.Parity.restrict_ne_flip_of_live {n : ℕ} (rho : PartialAssignment n) (selected : Fin n) (live : selected ∈ rho.liveVariables) (input : Fin n → Bool) : (function n).restrict rho (flip input selected) ≠ (function n).restrict rho input

Flipping a coordinate left live by rho changes restricted parity on every input.

theorem Algebraic.AC0.Parity.liveVariables_subset_evaluationPath {n : ℕ} (rho : PartialAssignment n) (tree : DecisionTree n) (computes : tree.Computes ((function n).restrict rho)) (input : Fin n → Bool) : rho.liveVariables ⊆ (DecisionTree.PathStep.indices (tree.evaluationPath input)).toFinset

Every live parity coordinate must occur on every evaluation path of a tree computing the restricted function.

theorem Algebraic.AC0.Parity.depthAtLeast_liveCount {n : ℕ} (rho : PartialAssignment n) : DecisionTree.DepthAtLeast ((function n).restrict rho) rho.liveCount

Every tree computing parity restricted by rho has depth at least the number of variables still live.

theorem Algebraic.AC0.Parity.depthAtMost_liveCount {n : ℕ} (rho : PartialAssignment n) : DecisionTree.DepthAtMost ((function n).restrict rho) rho.liveCount

The structural Shannon tree over the live coordinates gives the matching upper bound.

theorem Algebraic.AC0.Parity.depthAtMost_iff_liveCount_le {n : ℕ} (rho : PartialAssignment n) (bound : ℕ) : DecisionTree.DepthAtMost ((function n).restrict rho) bound ↔ rho.liveCount ≤ bound

Exact semantic characterization of the depth of restricted parity.