Equational lemma: if an entry \((idx, dir)\) with \(idx \lt w\) is immediately followed by the marker \((w, \mathrm{false})\), then \(\mathrm{parseAux}\) emits the triple \((\langle idx, h\rangle , dir, \mathrm{true})\) followed by the parse of the rest.

Equational lemma: if an entry \((idx, dir)\) is immediately followed by another in-range entry \((idx', dir')\), then \(\mathrm{parseAux}\) emits the triple \((\langle idx, h\rangle , dir, \mathrm{false})\) followed by the parse of the remaining list starting at \((idx', dir')\).

Equational lemma: a single in-range entry \((idx, dir)\) parses to the singleton \([(\langle idx, h\rangle , dir, \mathrm{false})]\).

Equational lemma: \(\mathrm{parseAux}\) of the empty list is the empty list.

Round-trip identity: for every triple list \(ts\), applying \(\mathrm{triplesToAux}\) and then \(\mathrm{parseAux}\) recovers \(ts\).

\(\mathrm{triplesToAux}\, (ts_1 \mathbin {+\! \! +} ts_2) = \mathrm{triplesToAux}\, ts_1 \mathbin {+\! \! +} \mathrm{triplesToAux}\, ts_2\).

The aux output length of \(\mathrm{processClauseLits}\) plus the remaining path length never exceeds the initial path length.

On a nonempty block, \(\mathrm{triplesToAux}(\mathrm{markLast}\, block)\) equals the block mapped into \(\mathbb {N} \times \mathrm{Bool}\) followed by a single \((w, \mathrm{false})\) termination marker.

If \(block \neq []\) then \(\mathrm{markLast}\, block \neq []\).

\((\mathrm{markLast}\, block).\mathrm{length} = block.\mathrm{length}\).

On a nonempty block, the last element of \(\mathrm{markLast}\, block\) has marker flag equal to true.

\((\mathrm{toFinBlock}\, w\, l\, h).\mathrm{length} = l.\mathrm{length}\).

Mapping the \(\mathrm{Fin}\) blocks back to \((\mathbb {N} \times \mathrm{Bool})\) via \(p \mapsto (p.1.\mathrm{val}, p.2)\) recovers the original list \(l\).

If \(l \neq []\) then \(\mathrm{toFinBlock}\, w\, l\, h \neq []\).

When the processed literals come from \(t.\mathrm{zipIdx}\), every entry of the aux output of \(\mathrm{processClauseLits}\) has first coordinate strictly less than \(t.\mathrm{length}\).

The aux output of \(\mathrm{razborovEncode.go}\) (started with empty accumulator) can be written as \(\mathrm{triplesToAux}\, w\, ts\) for some triple list \(ts\) whose length is bounded by the path length and whose last element, if any, has marker flag true. This is the main structural invariant of the encoder.

There exists a function \(g\) from aux lists into \(\mathrm{Fin}\, d \to \mathrm{Fin}\, w \times \mathrm{Bool} \times \mathrm{Bool}\) that is injective on the image of the Razborov encoder over bad \(s\)-restrictions with fixed \(\gamma \). This isolates the combinatorial encoding of each of the \(d\) path steps as a triple \((\mathrm{position}, \mathrm{direction}, \mathrm{hasMarker})\).

The number of distinct aux lists produced by the Razborov encoder on bad restrictions with a fixed first component \(\gamma \) is at most \((4w)^d\).

The number of bad \(s\)-restrictions \(\rho \) mapping to a fixed \(\gamma \) under the encoder is at most \((4w)^d\), since each of the \(d\) path steps carries \(w \cdot 2 \cdot 2 = 4w\) possibilities.

The number of restrictions of \(\{ 0,\dots ,n-1\} \) with exactly \(k\) free variables equals \(\binom {n}{k} \cdot 2^{\, n-k}\).

If \(\rho \, v = \mathrm{none}\), then updating \(\rho \) at \(v\) to \(\mathrm{some}\, b\) decreases \(\mathrm{numFree}\) by exactly one: \(\mathrm{numFree}(\rho [v \mapsto b]) + 1 = \rho .\mathrm{numFree}\).

If \(\rho _0\) and \(\sigma \) have the same free variables, then after \(\mathrm{processClauseLits}\) the updated \(\rho _0\) and \(\sigma \) components still agree on which variables are free.

Under the invariants that \(\rho _0\) and \(\sigma \) share free variables and each processed literal’s variable is free in \(\rho _0\), the \(\sigma \)-component of \(\mathrm{processClauseLits}\) has \(\mathrm{numFree}\) decreased by exactly \(\min (\mathrm{lits.length}, \mathrm{path.length})\).

If \(\rho \) is a bad restriction (so \(\mathrm{dtDepth}(f|_\rho ) \gt d\)), then the deepest path of the canonical decision tree \(\mathrm{canonicalDTree}\, f\, \rho \) has length strictly greater than \(d\).

When \(\rho \) is bad, the prefix \((\mathrm{canonicalDTree}\, f\, \rho ).\mathrm{deepPath}.\mathrm{take}\, d\) used by the encoder has length exactly \(d\).

\(\mathrm{processClauseLits}\) consumes exactly \(\min (\mathrm{lits.length}, \mathrm{path.length})\) path entries; the remaining path length plus this minimum equals the original path length.

Updating \(\rho \) at \(v\) to \(\mathrm{some}\, b\) decreases \(\mathrm{numFree}\) by at most one: \(\mathrm{numFree}(\rho [v \mapsto b]) + 1 \geq \rho .\mathrm{numFree}\).

If the initial path length is at most \(\rho _0.\mathrm{numFree}\), then after \(\mathrm{processClauseLits}\) the remaining path length is at most the updated \(\rho _0\)’s \(\mathrm{numFree}\).

If every clause of \(f\) is killed by \(\rho \), the canonical decision tree for \(f|_\rho \) is the leaf \(\mathrm{false}\) and hence has depth \(0\).

If some clause of \(f\) is fixed (satisfied) by \(\rho \), the canonical decision tree for \(f|_\rho \) is the leaf \(\mathrm{true}\) and hence has depth \(0\).

Filtering \(t.\mathrm{zipIdx}\) by a predicate on the literal component has the same length as filtering the original term \(t\) by the same predicate.

The literal component of the \(k\)-th element of the filtered \(t.\mathrm{zipIdx}\) equals the \(k\)-th element of the filtered term \(t\).

When \(f.\mathrm{find?}\) returns an alive clause \(t\) and \(\mathrm{flis}\) is the filtered (zipIdx) list of \(t\)’s free literals under \(\rho \), the variable at position \(k\) of \((\mathrm{canonicalDTree}\, f\, \rho ).\mathrm{deepPath}\) equals the variable of the \(k\)-th free literal, since the canonical tree branches on the free literals of \(t\) in clause order.

The remaining path returned by \(\mathrm{processClauseLits}\) equals \(\mathrm{path}.\mathrm{drop}(\min (\mathrm{lits.length}, \mathrm{path.length}))\).

Provided each literal’s variable is free in \(\rho _0\) and the variables are pairwise distinct, the \(\rho _0\)-component of \(\mathrm{processClauseLits}\) loses exactly \(\min (\mathrm{lits.length}, \mathrm{path.length})\) free variables.

Dropping the free-literal prefix from \((\mathrm{termSubTree}\, t\, \rho _0\, \mathrm{cont}).\mathrm{deepPath}\) yields the deep path of the continuation evaluated at the \(\mathrm{processClauseLits}\)-updated restriction, connecting the canonical tree structure to the encoder’s restriction update.

When the literals are the free literals of the first alive clause and the input path is canonical, \(\mathrm{IsCanonicalPath}\) is preserved by \(\mathrm{processClauseLits}\): the remaining path is again a canonical path for the updated restriction, and its length is at most the depth of the updated canonical tree.

If \(t\) has no duplicate literals and any two literals of \(t\) with the same variable are equal, then the free-variable filter of \(t.\mathrm{zipIdx}\) has pairwise distinct variables.

When the canonical tree depth is at least the path length, \(\mathrm{razborovEncode.go}\) fully consumes the path (never terminating early), and the resulting \(\sigma \) has \(\mathrm{numFree}\) decreased by exactly the initial path length: \((\mathrm{go}\, \dots ).1.\mathrm{numFree} + \mathrm{path.length} = \sigma .\mathrm{numFree}\).

For a bad \(s\)-restriction \(\rho \) with \(d \leq s\), the first component (the \(\gamma \)-output) of \(\mathrm{razborovEncode}\, f\, w\, d\, \rho \) is an \((s-d)\)-restriction, since the encoder fixes exactly \(d\) previously free variables.

For \(d \leq s\), the number of bad \(s\)-restrictions is at most \(\binom {n}{s-d}\, 2^{\, n-(s-d)}\, (4w)^d\): every bad \(s\)-restriction is mapped by \(\mathrm{razborovEncode}\) to a \(\gamma \) with exactly \(s-d\) free variables, each fiber of this map has size at most \((4w)^d\), and there are \(\binom {n}{s-d}\, 2^{\, n-(s-d)}\) possible values of \(\gamma \).

If \(s \leq d\), the set of restrictions that are simultaneously \(s\)-restrictions and bad restrictions for depth \(d\) is empty.

For any Boolean function \(f\) there exists a decision tree \(T\) computing \(f\) with depth at most \(\mathrm{dtDepth}\, f\).

If \(\mathrm{dtDepth}\, f \leq d\), then \(f\) is computed by a DNF of width at most \(d\) and by a CNF of width at most \(d\).

\((l.\mathrm{flipNeg}).\mathrm{eval}\, x = \lnot \, (l.\mathrm{eval}\, x)\).

\((l.\mathrm{flipNeg}).\mathrm{var} = l.\mathrm{var}\).

The map \(\mathrm{Literal.flipNeg}\) is injective.

\((\mathrm{cnfToDualDNF}\, \psi ).\mathrm{width} = \psi .\mathrm{width}\).

\((\mathrm{cnfToDualDNF}\, \psi ).\mathrm{eval}\, x = \lnot \, (\psi .\mathrm{eval}\, x)\).

\(T.\mathrm{negateLeaves}.\mathrm{eval}\, x = \lnot \, (T.\mathrm{eval}\, x)\).

\(T.\mathrm{negateLeaves}.\mathrm{depth} = T.\mathrm{depth}\).

\(\mathrm{dtDepth}(\lnot f) = \mathrm{dtDepth}\, f\).

\(\mathrm{restrictFn}(\lnot f)\, \rho = \lnot \, (\mathrm{restrictFn}\, f\, \rho )\), pointwise.

\(\mathrm{IsBadRestriction}(\lnot f)\, d\, \rho \iff \mathrm{IsBadRestriction}\, f\, d\, \rho \).

If every clause of \(\psi \) has no duplicate literals, then every term of \(\mathrm{cnfToDualDNF}\, \psi \) has no duplicate literals.

If within each clause of \(\psi \) any two literals with the same variable are equal, then the same holds within every term of \(\mathrm{cnfToDualDNF}\, \psi \).

For natural numbers \(n, s, d\) with \(5s \leq n\) and \(d \leq s\),

This is the purely combinatorial inequality used to convert the bad-restriction count into the final \((10\, s\, w)^d\) form of the switching lemma.