3 Håstad’s Switching Lemma

3.1 Overview

This chapter formalises Håstad’s Switching Lemma (1987) via Razborov’s decision-tree path encoding. Informally:

If $f$ is a width-$w$ DNF and $\rho $ is a uniformly random $s$-restriction, then the probability that $f\! \restriction \! \rho $ requires a decision tree of depth $\gt d$ is at most $(5sw/n)^d$ (or a constant-factor variant thereof).

The Lean statement, SwitchingLemma2.switching_lemma, is a combinatorial counting inequality rather than a probability bound; the two are equivalent after rearranging. References: Håstad (1987); Razborov’s simplified proof; O’Donnell, Analysis of Boolean Functions, Ch. 4.

3.2 The formalised statement

Theorem 3.1 Switching Lemma – Lean statement

Let $n\gt 0$, let $f:\{ 0,1\} ^n\to \{ 0,1\} $ be a DNF formula, and fix $w,s,d\in \mathbb {N}$. Assume

$\text{width}(f)\le w$ (width counted as list length, see Section 3.3),
$5s \le n$,
$f$ satisfies the non-contradictory clause hypothesis hnd: for every term $t\in f$ and every pair of literals $\ell _1,\ell _2\in t$, if $\ell _1.\mathrm{var}=\ell _2.\mathrm{var}$ then $\ell _1=\ell _2$.

Then

\[ \bigl|\{ \, \rho : \rho \text{ is an $s$-restriction and } \mathrm{dtDepth}(f|_\rho )\gt d\, \} \bigr| \cdot n^d \; \le \; \mathrm{numSRestrictions}(n,s)\, \cdot \, (10\, s\, w)^d. \]

3.3 Faithfulness critique

The Lean statement is faithful to the classical lemma modulo a handful of subtle modelling choices. This section documents each one so a user of SwitchingLemma2.switching_lemma knows precisely what they are signing up for.

3.3.1 How DNFs are modelled

Recall (Literal, Term, DNF in TCSlib/BooleanAnalysis/Circuit.lean):

A literal is a pair $(v,\mathrm{neg})\in \mathrm{Fin}\, n\times \mathrm{Bool}$.
A term is a list of literals, not a set or a Finset.
A DNF is a list of terms.
Term.width is defined as List.length, i.e. literal occurrences are counted with multiplicity.
DNF.width is the (list-)maximum of the term widths.

Consequence 1 – Width vs. literal count.

In the textbook, “width $w$” means each term involves at most $w$ distinct variables. In our formalisation, f.width ≤ w is the stronger statement “each term has at most $w$ literal occurrences”. For a syntactically clean DNF (no repeated literals inside a clause) the two notions coincide and the hypothesis is trivial to supply. For a DNF with repeated literals, the formalised width can be strictly larger, which means the user must either dedup before applying the theorem or accept a looser bound. This is not an unsoundness, but it is a papercut that is worth flagging.

Consequence 2 – The hnd hypothesis.

The parameter

\[ \texttt{hnd} \; :\; \forall t\in f,\; \forall \ell _1,\ell _2\in t,\; \ell _1.\mathrm{var}=\ell _2.\mathrm{var}\; \Rightarrow \; \ell _1=\ell _2 \]

is not the same as “each term uses distinct variables”. It only forbids a term from containing both a literal and its negation (a self-falsifying term). It does allow a term to contain the same literal twice. Two remarks:

The classical statement does not explicitly require hnd; self-falsifying clauses are implicitly removed as identically false. Our formalisation makes this requirement explicit, so the user must discharge a proof obligation that is mechanical but nonzero. For a concrete DNF built from literals read off a file or a syntactic representation, decide usually suffices.
hnd is used crucially in SwitchingLemma2.encode_go_not_kills_first_clause and its callers to guarantee that, when the encoder processes the free-var literals of a term, the variable-to-literal lookup is well-defined (no variable appears with two different polarities in the same term). Without it, the round-trip property fails.

3.3.2 The restriction regime: $5s \le n$

Classical Hastad is typically stated for any $s$, with the bound reading $(5pw)^d$ where $p = s/n$. The formalisation bakes in the hypothesis $5s\le n$, i.e. $p\le 1/5$. This is not an artefact of the combinatorics per se but of the particular inductive proof of the Vandermonde identity (SwitchingLemma2.choose_mul_pow_bound) used to convert $\binom {n}{s-d}(4n)^d\le \binom {n}{s}(5s)^d$. For restrictions with $p\gt 1/5$ one must either generalise that lemma or apply the theorem vacuously via the $d\gt s$ branch (bad_filter_empty_of_d_ge_s).

$0\lt n$.

Required so that $\mathrm{Fin}\, n$ is inhabited. Trivial.

3.3.3 The $(10sw)^d$ constant vs. $(5sw)^d$

Razborov’s encoding yields $(5sw/n)^d$ in the sharpest accounting. The formalised constant is $10sw$ rather than $5sw$. The extra factor of two comes from the combinatorial bound on the encoder image size (aux_image_card_bound via exists_aux_injection), which tags each of the $d$ encoded triples as $\mathrm{Fin}\, w\times \mathrm{Bool}\times \mathrm{Bool}$ (position, polarity, end-of-block marker). A sharper encoder is possible but was sidestepped for proof-engineering simplicity. This is a loss of a constant factor, not an asymptotic one.

3.3.4 Status

SwitchingLemma2.switching_lemma is stated and the outer structure is complete.
SwitchingLemma2.bad_count_bound currently contains a sorry (line 636 of MainTheorem.lean) which is the summation step that passes from “fibre bound” to “total bound”. Everything else is sorry-free.
SwitchingLemma2.RoundTrip.go_roundtrip_gen contains one inductive-step sorry at the re-entry point of the induction hypothesis.

3.4 Dependency graph

The proof is layered across seven Lean files. Information flows downward:

File	Key contents
Circuit.lean	Literal, Term, DNF, CNF, DecisionTree, dtDepth, buildFullDTree.
Switching/Defs.lean	Restriction, Restriction.extend, numFree, SwitchingLemma2.Restriction.freeVars, SwitchingLemma2.Literal.killedBy, SwitchingLemma2.Term.fixedBy, SwitchingLemma2.restrictFn, SwitchingLemma2.IsBadRestriction, SwitchingLemma2.IsRestriction, SwitchingLemma2.numSRestrictions, SwitchingLemma2.first_clause_preserved.
Switching/CanonicalDTree.lean	canonicalDTree (Razborov’s DT), correctness, SwitchingLemma2.dtDepth_restrictFn_le_numFree (depth $\le $ numFree).
Switching/Encoding.lean	razborovEncode, razborovDecode, SwitchingLemma2.processClauseLits.
Switching/EncodingProperties.lean	Numerous invariants of the encoder; uses hnd for SwitchingLemma2.encode_go_not_kills_first_clause.
Switching/RoundTrip.lean	go_roundtrip_gen (decode $\circ $ encode = id), SwitchingLemma2.razborovEncode_injective.
Switching/MainTheorem.lean	Encoder image parser, exists_aux_injection, SwitchingLemma2.aux_image_card_bound, SwitchingLemma2.fiber_bound, SwitchingLemma2.bad_count_bound, SwitchingLemma2.choose_mul_pow_bound, SwitchingLemma2.switching_lemma, SwitchingLemma2.switching_corollary.

Conceptually the proof factors as:

\[ \underbrace{ \texttt{razborovEncode}\text{ is injective on bad restrictions} }_{\text{RoundTrip.lean (needs hnd)}} \; \Rightarrow \; \underbrace{ |\{ \text{bad}\} | \le |\mathrm{image}(\texttt{razborovEncode})| }_{\text{set-theoretic}} \; \Rightarrow \; \underbrace{ |\mathrm{image}| \le (\text{combinatorial count}) }_{\text{MainTheorem.lean}}. \]

The combinatorial count is obtained by fibring the image over the first component $\gamma $ (a restriction with $s-d$ fewer free variables), bounding each fibre by $(4w)^d$ (the aux-data count SwitchingLemma2.aux_image_card_bound), then summing fibres via the Vandermonde-type inequality choose_mul_pow_bound, which is where $5s\le n$ is consumed.

3.5 Corollary: no small CNF approximations

Theorem 3.2 Switching corollary

Under the same hypotheses as Theorem 3.1,

\[ \bigl|\{ \rho : \mathrm{IsRestriction}\ s\ \rho ,\ f|_\rho \text{ has no CNF of width}\le w\} \bigr| \cdot n^w \le \mathrm{numSRestrictions}(n,s)\, (10sw)^w. \]

This uses the fact (dtDepth_le_implies_small_dnf_cnf) that a function with small decision-tree depth admits both a small-width DNF and a small-width CNF.

TCSLib