Switching lemmas against parity

This module connects the width-sensitive switching encoding to the exact decision-tree lower bound for parity under a finite restriction. If a CNF or DNF computes N-bit parity, then every restriction leaving at least queryCount variables free belongs to its switching bad event.

The resulting cardinality inequality is division-free and applies to arbitrary formulas: contradictory DNF terms and tautological CNF clauses are cleaned without changing semantics or increasing width.

theorem Complexity.DNF.freeVariables_card_le_switchingDepth_of_xorBool {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) : restriction.freeVariables.card ≤ (formula.switchingDecisionTreeUnder restriction).depth

A DNF switching tree for restricted parity must have depth at least the number of variables left free by the restriction.

theorem Complexity.DNF.freeVariables_atLeast_implies_switchingBad {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (queryCount : ℕ) (restriction : Restriction.On N) (hfree : queryCount ≤ restriction.freeVariables.card) : formula.switchingBad queryCount restriction

Every restriction leaving at least queryCount variables free is bad for a DNF that computes parity.

theorem Complexity.DNF.freeVariables_eventCount_le_switchingBad {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) ≤ RandomRestriction.eventCount q (formula.switchingBad queryCount)

The count of restrictions leaving many variables free is bounded by the DNF switching bad-event count.

theorem Complexity.DNF.switchingParity_width_counting_bound {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

Width-sensitive finite counting obstruction for any DNF computing parity.

The formula is cleaned internally, so no consistency hypothesis is required and the displayed width is that of the original DNF.

theorem Complexity.DNF.switchingParity_width_one_free_bound {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q : ℕ) : ((2 * q + 1) ^ N - (2 * q) ^ N) * q ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1))

Explicit one-surviving-variable specialization of the DNF switching obstruction. The event count has been evaluated exactly.

theorem Complexity.CNF.freeVariables_card_le_switchingDepth_of_xorBool {N : ℕ} (formula : CNF N) (restriction : Restriction.On N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) : restriction.freeVariables.card ≤ (formula.switchingDecisionTreeUnder restriction).depth

A CNF switching tree for restricted parity must have depth at least the number of variables left free by the restriction.

theorem Complexity.CNF.freeVariables_atLeast_implies_switchingBad {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (queryCount : ℕ) (restriction : Restriction.On N) (hfree : queryCount ≤ restriction.freeVariables.card) : formula.switchingBad queryCount restriction

Every restriction leaving at least queryCount variables free is bad for a CNF that computes parity.

theorem Complexity.CNF.freeVariables_eventCount_le_switchingBad {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) ≤ RandomRestriction.eventCount q (formula.switchingBad queryCount)

The count of restrictions leaving many variables free is bounded by the CNF switching bad-event count.

theorem Complexity.CNF.switchingParity_width_counting_bound {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

Width-sensitive finite counting obstruction for any CNF computing parity.

The formula is cleaned internally, so no consistency hypothesis is required and the displayed width is that of the original CNF.

theorem Complexity.CNF.switchingParity_width_one_free_bound {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q : ℕ) : ((2 * q + 1) ^ N - (2 * q) ^ N) * q ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1))

Explicit one-surviving-variable specialization of the CNF switching obstruction. The event count has been evaluated exactly.