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, SwitchingLemma.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 Håstad’s switching lemma for bounded-width DNFs

Let \(n \ge 1\), and let \(f\) be a DNF formula on \(n\) Boolean variables whose width is at most \(w\), so that every term of \(f\) has at most \(w\) literals. Suppose that \(5s \le n\), that no term of \(f\) contains two distinct literals on the same variable, and that no term of \(f\) repeats a literal. Call a restriction \(\rho \) on the \(n\) variables an \(s\)-restriction if it leaves exactly \(s\) variables free, and call it bad (at depth \(d\)) if the restricted function \(f|_\rho \) has decision-tree depth strictly greater than \(d\). Then the number \(N\) of \(s\)-restrictions that are bad satisfies

\[ N \cdot n^{d} \; \le \; \binom {n}{s}\, 2^{\, n-s}\, (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 SwitchingLemma.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.
LitList.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 SwitchingLemma.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 (SwitchingLemma.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

SwitchingLemma.switching_lemma is stated and the outer structure is complete.
SwitchingLemma.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.
SwitchingLemma.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, DecisionTree.buildFull.
Switching/Defs.lean	Restriction, Restriction.extend, numFree, SwitchingLemma.Restriction.freeVars, SwitchingLemma.Literal.killedBy, SwitchingLemma.Term.fixedBy, SwitchingLemma.restrictFn, SwitchingLemma.IsBadRestriction, SwitchingLemma.IsRestriction, SwitchingLemma.numSRestrictions, SwitchingLemma.first_clause_preserved.
Switching/CanonicalDTree.lean	canonicalDTree (Razborov’s DT), correctness, SwitchingLemma.dtDepth_restrictFn_le_numFree (depth \(\le \) numFree).
Switching/Encoding.lean	razborovEncode, razborovDecode, SwitchingLemma.processClauseLits.
Switching/EncodingProperties.lean	Numerous invariants of the encoder; uses hnd for SwitchingLemma.encode_go_not_kills_first_clause.
Switching/RoundTrip.lean	go_roundtrip_gen (decode \(\circ \) encode = id), SwitchingLemma.razborovEncode_injective.
Switching/MainTheorem.lean	Encoder image parser, exists_aux_injection, SwitchingLemma.aux_image_card_bound, SwitchingLemma.fiber_bound, SwitchingLemma.bad_count_bound, SwitchingLemma.choose_mul_pow_bound, SwitchingLemma.switching_lemma, SwitchingLemma.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 SwitchingLemma.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: restrictions with no narrow CNF

Let \(f\) be a DNF formula on \(n \ge 1\) variables in which no variable occurs more than once within any single term, and let \(w, s \in \mathbb {N}\) satisfy \(5s \le n\) and \(\mathrm{width}(f) \le w\) (that is, every term of \(f\) has at most \(w\) literals). For a restriction \(\rho \) that fixes some variables and leaves the others free, write \(f\! \restriction _\rho \) for the Boolean function obtained by evaluating \(f\) with the fixed coordinates set by \(\rho \) and the free coordinates supplied as input. Then the number of restrictions \(\rho \) leaving exactly \(s\) of the \(n\) variables free for which \(f\! \restriction _\rho \) agrees with no CNF formula of width at most \(w\) satisfies

\[ \bigl|\{ \rho : \rho \text{ leaves exactly } s \text{ variables free, and } f\! \restriction _\rho \text{ has no width-}{\le }w\text{ CNF}\} \bigr| \cdot n^{w} \; \le \; \binom {n}{s}\, 2^{\, 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.