Parity under finite restrictions

Schnorr.xorOn support is parity on an explicit finite set of coordinates. Fixing one coordinate to zero erases it from the support, while flipping any supported coordinate complements the result.

The main lower bound says that every finite-arity decision tree computing parity on support has depth at least support.card. This is the parity-side contradiction needed after a switching argument leaves many variables free.

@[simp]

theorem Complexity.Schnorr.xorOn_empty {N : ℕ} (input : BitString N) : xorOn ∅ input = false

theorem Complexity.Schnorr.xorOn_insert {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (hindex : index ∉ support) (input : BitString N) : xorOn (insert index support) input = xorOp (input index) (xorOn support input)

Insert one fresh parity coordinate.

theorem Complexity.Schnorr.xorOn_update_of_not_mem {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (hindex : index ∉ support) (value : Bool) (input : BitString N) : xorOn support (Function.update input index value) = xorOn support input

Updating a coordinate outside the support does not change parity.

theorem Complexity.Schnorr.xorOn_update_false_eq_erase {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (input : BitString N) : xorOn support (Function.update input index false) = xorOn (support.erase index) input

Fixing one coordinate to zero erases it from the parity support.

theorem Complexity.Schnorr.xorOn_flip {N : ℕ} (support : Finset (Fin N)) (index : Fin N) (hindex : index ∈ support) (input : BitString N) : xorOn support (Function.update input index !input index) = !xorOn support input

Flipping any supported coordinate complements parity.

theorem Complexity.Schnorr.xorOn_univ_eq_xorBool {N : ℕ} (input : BitString N) : xorOn Finset.univ input = xorBool N input

Parity on the full finite support is the library's existing recursive xorBool function.

theorem Complexity.Schnorr.xorOn_applyTo {N : ℕ} (support : Finset (Fin N)) (restriction : Restriction.On N) (input : BitString N) : xorOn support (restriction.applyTo input) = xorOp (xorOn support (restriction.applyTo fun (x : Fin N) => false)) (xorOn ({index ∈ support | restriction index = none}) input)

Restricting parity separates into the parity of the fixed coordinates and the parity of the surviving free coordinates.

theorem Complexity.Schnorr.xorBool_applyTo {N : ℕ} (restriction : Restriction.On N) (input : BitString N) : xorBool N (restriction.applyTo input) = xorOp (xorBool N (restriction.applyTo fun (x : Fin N) => false)) (xorOn restriction.freeVariables input)

Full parity under a restriction is parity on exactly the free variables, possibly complemented by the fixed coordinates.

theorem Complexity.Schnorr.card_support_le_depth {N : ℕ} (tree : DecisionTree.On N) (support : Finset (Fin N)) (computes : ∀ (input : BitString N), DecisionTree.On.eval input tree = xorOn support input) : support.card ≤ tree.depth

A decision tree computing parity on support must query to depth at least the number of supported coordinates.

theorem Complexity.Schnorr.card_support_le_depth_offset {N : ℕ} (tree : DecisionTree.On N) (support : Finset (Fin N)) (offset : Bool) (computes : ∀ (input : BitString N), DecisionTree.On.eval input tree = xorOp offset (xorOn support input)) : support.card ≤ tree.depth

Complementing parity by a fixed offset does not reduce its decision-tree depth.

theorem Complexity.Schnorr.freeVariables_card_le_depth_of_restricted_xor {N : ℕ} (tree : DecisionTree.On N) (restriction : Restriction.On N) (computes : ∀ (input : BitString N), DecisionTree.On.eval input tree = xorBool N (restriction.applyTo input)) : restriction.freeVariables.card ≤ tree.depth

Any decision tree computing full parity after a restriction must query at least the number of coordinates that the restriction leaves free.