Switching-lemma substrate

This module exposes both an elementary one-query-at-a-time decision tree and the complete-block tree used in switching arguments. Its finite encoding theorems include an elementary arity-dependent bound and a width-only bound for consistent DNFs. The latter replays the canonical complete-block path from bounded literal positions, branch bits, and phase markers.

theorem Complexity.Switching.card_pathCode (N queryCount : ℕ) : Fintype.card (PathCode N queryCount) = (2 * N) ^ queryCount

The elementary deepest-path code has exactly (2 * N) ^ queryCount possible values.

theorem Complexity.Switching.card_widthPathCode (width queryCount : ℕ) : Fintype.card (WidthPathCode width queryCount) = (4 * (width + 1)) ^ queryCount

Width-sensitive per-query advice has exactly (4 * (width + 1)) ^ queryCount possible values.

theorem Complexity.DNF.consistent_consistentPart {N : ℕ} (formula : DNF N) : formula.consistentPart.Consistent

Removing contradictory terms leaves a termwise-consistent DNF.

theorem Complexity.DNF.eval_consistentPart {N : ℕ} (formula : DNF N) (input : BitString N) : formula.consistentPart.eval input = formula.eval input

Contradictory-term cleanup preserves the represented Boolean function.

theorem Complexity.DNF.width_consistentPart_le {N : ℕ} (formula : DNF N) : formula.consistentPart.width ≤ formula.width

Contradictory-term cleanup cannot increase DNF width.

theorem Complexity.DNF.firstLiveTerm_reduced {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) : Option.map Prod.snd (formula.firstLiveTerm restriction) = (restrict restriction formula).terms.head?

The reduced component of the first surviving original term is exactly the first term in the syntactically restricted DNF.

theorem Complexity.DNF.firstLiveTerm_spec {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) (original reduced : List (Literal N)) (hfirst : formula.firstLiveTerm restriction = some (original, reduced)) : ∃ (before : List (List (Literal N))) (after : List (List (Literal N))), formula.terms = before ++ original :: after ∧ restrictTerm restriction original = some reduced ∧ ∀ term ∈ before, restrictTerm restriction term = none

A successful first-live lookup provides an ordered-list decomposition: the selected original term survives with the stated reduction, and every earlier term is killed.

theorem Complexity.DNF.firstLiveTerm_comp {N : ℕ} (formula : DNF N) (first second : Restriction.On N) (original reduced final : List (Literal N)) (hfirst : formula.firstLiveTerm first = some (original, reduced)) (hsecond : restrictTerm second reduced = some final) : formula.firstLiveTerm (first.comp second) = some (original, final)

Extending a restriction preserves its first live term whenever that term's reduced remainder survives the extension.

theorem Complexity.DNF.switchingDecisionTreeUnder_eq {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) : formula.switchingDecisionTreeUnder restriction = (restrict restriction formula).switchingDecisionTree

Retaining the original DNF while accumulating a restriction gives exactly the same complete-block tree as simplifying first.

theorem Complexity.DNF.eval_canonicalDecisionTree {N : ℕ} (formula : DNF N) (input : BitString N) : DecisionTree.On.eval input formula.canonicalDecisionTree = formula.eval input

The canonical DNF decision tree computes the same finite Boolean function.

theorem Complexity.DNF.depth_canonicalDecisionTree_le_vars {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.depth ≤ formula.vars.card

Canonical decision-tree depth is bounded by the number of variables actually occurring in the DNF.

theorem Complexity.DNF.depth_canonicalDecisionTree_le_arity {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.depth ≤ N

In particular, canonical decision-tree depth never exceeds the declared input arity.

theorem Complexity.DNF.vars_canonicalDecisionTree_subset {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.vars ⊆ formula.vars

Every query in the canonical DNF tree occurs in the DNF itself.

theorem Complexity.DNF.pathReadOnce_canonicalDecisionTree {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.PathReadOnce

The canonical DNF tree never repeats a variable along one path.

theorem Complexity.DNF.eval_switchingDecisionTree {N : ℕ} (formula : DNF N) (input : BitString N) : DecisionTree.On.eval input formula.switchingDecisionTree = formula.eval input

The complete-block DNF switching tree computes the original formula.

theorem Complexity.DNF.vars_switchingDecisionTree_subset {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.vars ⊆ formula.vars

Every query in the complete-block tree occurs in the DNF itself.

theorem Complexity.DNF.pathReadOnce_switchingDecisionTree {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.PathReadOnce

The complete-block DNF tree never repeats a variable along one path.

theorem Complexity.DNF.depth_switchingDecisionTree_le_vars {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.depth ≤ formula.vars.card

Complete-block switching-tree depth is bounded by actual support size.

theorem Complexity.DNF.depth_switchingDecisionTree_le_arity {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.depth ≤ N

Complete-block switching-tree depth never exceeds the declared arity.

theorem Complexity.DNF.switchingBad_width_encoding_bound {N : ℕ} (formula : DNF N) (hconsistent : formula.Consistent) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

Width-only finite counting form of the DNF switching lemma.

For a consistent width-w DNF, every bad restriction together with one of q ^ queryCount copy-label choices injects into a seed and queryCount advice symbols, each drawn from a set of size 4 * (w + 1). This is the combinatorial form needed to derive the corresponding probability bound under RandomRestriction.

theorem Complexity.DNF.switchingBad_consistentPart_width_encoding_bound {N : ℕ} (formula : DNF N) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.consistentPart.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

Every DNF has an equivalent consistent sub-DNF to which the width-only encoding applies without increasing the original width.

theorem Complexity.DNF.switchingBad_arity_encoding_bound {N : ℕ} (formula : DNF N) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (2 * N) ^ queryCount

Elementary arity-dependent counting bound for the DNF switching bad event.

The proof injectively records the first queryCount coordinates and branch values of a complete-block deepest path. Consequently the auxiliary factor is (2 * N) ^ queryCount. A genuine switching lemma must replace this ambient arity factor by a bound in the DNF width.

theorem Complexity.CNF.consistent_consistentPart {N : ℕ} (formula : CNF N) : formula.consistentPart.Consistent

Removing tautological clauses leaves a consistent CNF.

theorem Complexity.CNF.eval_consistentPart {N : ℕ} (formula : CNF N) (input : BitString N) : formula.consistentPart.eval input = formula.eval input

Tautological-clause cleanup preserves the represented Boolean function.

theorem Complexity.CNF.width_consistentPart_le {N : ℕ} (formula : CNF N) : formula.consistentPart.width ≤ formula.width

Tautological-clause cleanup cannot increase CNF width.

theorem Complexity.CNF.switchingDecisionTreeUnder_eq {N : ℕ} (formula : CNF N) (restriction : Restriction.On N) : formula.switchingDecisionTreeUnder restriction = (restrict restriction formula).switchingDecisionTree

Accumulating the restriction in the dual DNF gives the same CNF switching tree as syntactically restricting the CNF first.

theorem Complexity.CNF.switchingBad_eq_neg {N : ℕ} (formula : CNF N) (queryCount : ℕ) (restriction : Restriction.On N) : formula.switchingBad queryCount restriction ↔ formula.neg.switchingBad queryCount restriction

The CNF bad event is exactly the DNF bad event for its De Morgan dual.

theorem Complexity.CNF.switchingBad_width_encoding_bound {N : ℕ} (formula : CNF N) (hconsistent : formula.Consistent) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

Width-only finite counting form of the CNF switching lemma, obtained without loss from the corresponding theorem for the dual DNF.

theorem Complexity.CNF.switchingBad_consistentPart_width_encoding_bound {N : ℕ} (formula : CNF N) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.consistentPart.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

Every CNF has an equivalent consistent sub-CNF to which the width-only encoding applies without increasing the original width.

theorem Complexity.CNF.eval_canonicalDecisionTree {N : ℕ} (formula : CNF N) (input : BitString N) : DecisionTree.On.eval input formula.canonicalDecisionTree = formula.eval input

The canonical CNF decision tree computes the same finite Boolean function.

theorem Complexity.CNF.depth_canonicalDecisionTree_le_vars {N : ℕ} (formula : CNF N) : formula.canonicalDecisionTree.depth ≤ formula.vars.card

Canonical CNF decision-tree depth is bounded by actual support size.

theorem Complexity.CNF.depth_canonicalDecisionTree_le_arity {N : ℕ} (formula : CNF N) : formula.canonicalDecisionTree.depth ≤ N

Canonical CNF decision-tree depth never exceeds the declared arity.

theorem Complexity.CNF.eval_switchingDecisionTree {N : ℕ} (formula : CNF N) (input : BitString N) : DecisionTree.On.eval input formula.switchingDecisionTree = formula.eval input

The complete-block CNF switching tree computes the original formula.

theorem Complexity.CNF.vars_switchingDecisionTree_subset {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.vars ⊆ formula.vars

Every query in the complete-block CNF tree occurs in the CNF itself.

theorem Complexity.CNF.pathReadOnce_switchingDecisionTree {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.PathReadOnce

The complete-block CNF tree never repeats a variable along one path.

theorem Complexity.CNF.depth_switchingDecisionTree_le_vars {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.depth ≤ formula.vars.card

Complete-block CNF switching-tree depth is bounded by actual support.

theorem Complexity.CNF.depth_switchingDecisionTree_le_arity {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.depth ≤ N

Complete-block CNF switching-tree depth never exceeds declared arity.