For any literal/index list and any path, the combined output of SwitchingLemma2.processClauseLits is bounded: the length of its auxiliary entry list plus twice the length of its remaining path is at most \(2 \cdot |\mathrm{path}|\).

On non-empty literal and path lists, SwitchingLemma2.processClauseLits satisfies the strengthened bound: the auxiliary-entry length plus one, plus twice the remaining path length, is still at most twice the length of the input path.

The output produced by the encoder loop SwitchingLemma2.razborovEncode’s go grows in a controlled way: its second component has length at most \(|\mathrm{acc}| + 2 \cdot |\mathrm{path}|\), where \(\mathrm{acc}\) is the accumulator and \(\mathrm{path}\) the current path.

For a bad restriction \(\rho \) of a DNF \(f\) with depth parameter \(d\), the encoded output SwitchingLemma2.razborovEncode has length at most \(2d\).

If a variable \(v\) is the variable of no literal in the input list, then SwitchingLemma2.processClauseLits leaves the \(\sigma \) restriction unchanged at \(v\); that is, the resulting \(\sigma \) agrees with the input \(\sigma \) on \(v\).

If a variable \(v\) is the variable of no literal in the input list, then SwitchingLemma2.processClauseLits leaves the \(\rho _0\) restriction unchanged at \(v\); the resulting \(\rho _0\) agrees with the input \(\rho _0\) on \(v\).

If \(\rho _0\, v \neq \mathrm{none}\), then after running SwitchingLemma2.processClauseLits the resulting \(\rho _0\) at \(v\) is still not \(\mathrm{none}\); the routine never turns a set value into an unset one.

If \(\rho _0\, v \neq \mathrm{none}\) (so \(v\) is non-free), then the first component \(\gamma \) of the encoder loop SwitchingLemma2.razborovEncode’s go returns \(\sigma \, v\) at \(v\); the encoder does not alter \(\sigma \) on non-free variables.

The encoder loop SwitchingLemma2.razborovEncode’s go run with an accumulator decomposes into a run on the empty accumulator: its result can be expressed in terms of the corresponding empty-accumulator computation together with the supplied accumulator.

The first component of the encoder loop SwitchingLemma2.razborovEncode’s go does not depend on the accumulator: running with accumulator \(\mathrm{acc}\) yields the same first component as running with the empty accumulator.

If \(\sigma \, v = \mathrm{none}\), then the decoder’s processEntries routine leaves \(v\) unset; the resulting \(\sigma \) is still \(\mathrm{none}\) at \(v\).

If \(\sigma \, v = \mathrm{none}\), then the decoder loop SwitchingLemma2.razborovDecode’s go leaves \(v\) unset; its resulting \(\sigma \) is still \(\mathrm{none}\) at \(v\).

The remaining path, the \(\rho _0\) output, and the auxiliary entry list produced by SwitchingLemma2.processClauseLits are all independent of the input \(\sigma \): for any two starting restrictions \(\sigma _1, \sigma _2\) these three components coincide.

The second component (the emitted bit list) of the encoder loop SwitchingLemma2.razborovEncode’s go does not depend on the \(\sigma \) argument: starting from \(\sigma _1\) or \(\sigma _2\) gives the same output.

Every entry \(e\) in the auxiliary list produced by SwitchingLemma2.processClauseLits has its index \(e.1\) equal to the index of some literal \(li\) from the input list.

Suppose every input literal pair occurs in \(t.\texttt{zipIdx}\) and no input literal has variable \(v\). Then for every auxiliary entry \(e\) of SwitchingLemma2.processClauseLits, the literal at position \(e.1\) in \(t\) does not have variable \(v\).

Suppose every input literal pair occurs in \(t.\texttt{zipIdx}\) and all input literals are free under \(\rho _0\). Then for every auxiliary entry \(e\) of SwitchingLemma2.processClauseLits, the literal at position \(e.1\) in \(t\) has a variable that is free under \(\rho _0\) (its \(\rho _0\) value is \(\mathrm{none}\)).

Folding the decoder’s \(\sigma \)-update over a list of entries leaves \(v\) unchanged when no entry targets \(v\); that is, if for every entry the literal at its position in \(t\) does not have variable \(v\), the folded \(\sigma \) agrees with the initial \(\sigma \) at \(v\).

Folding the decoder’s \(\rho _0\)-update over a list of entries leaves \(v\) unchanged when no entry targets \(v\); if for every entry the literal at its position in \(t\) does not have variable \(v\), the folded \(\rho _0\) agrees with the initial \(\rho _0\) at \(v\).

If \(\sigma \, v = \mathrm{none}\), then folding the decoder’s \(\sigma \)-update over any list of entries still gives \(\mathrm{none}\) at \(v\); the fold never sets a previously unset variable to a value via the \(\sigma \)-update.

Suppose every input literal pair occurs in \(t.\texttt{zipIdx}\), that \(\rho _0\, v = \mathrm{none}\), and that SwitchingLemma2.processClauseLits sets the \(\rho _0\) component at \(v\). Then folding the decoder’s \(\sigma \)-update over the auxiliary entries yields \(\mathrm{none}\) at \(v\).

Suppose every input literal pair occurs in \(t.\texttt{zipIdx}\) and the decoder’s initial \(\rho _0\) value agrees with the encoder’s at \(v\). Then folding the decoder’s \(\rho _0\)-update over the auxiliary entries of SwitchingLemma2.processClauseLits reproduces the \(\rho _0\) component of that routine at \(v\).

A variant of the previous lemma allowing the decoder’s initial \(\rho _0\) to differ from the encoder’s: provided \(\rho _0\, v = \mathrm{none}\) and SwitchingLemma2.processClauseLits sets the \(\rho _0\) component at \(v\), the \(\rho _0\)-fold over the auxiliary entries still reproduces the routine’s \(\rho _0\) value at \(v\).

Contrapositive of \(\rho _0\)-stability: if \(\rho _0\, v = \mathrm{none}\), the SwitchingLemma2.processClauseLits output keeps \(\rho _0\) unset at \(v\), and there are at least as many path entries as literals, then no input literal has variable \(v\).

If two starting restrictions agree at \(v\) (\(\sigma _1\, v = \sigma _2\, v\)), then the \(\sigma \) output of SwitchingLemma2.processClauseLits at \(v\) is the same for both; the value at \(v\) depends only on the initial \(\sigma \) at \(v\).

If \(\rho _0\, v = \mathrm{none}\) and SwitchingLemma2.processClauseLits leaves \(\rho _0\) unset at \(v\), then it also leaves \(\sigma \) unchanged at \(v\); the \(\sigma \) output equals the input \(\sigma \) at \(v\), since \(\rho _0\) and \(\sigma \) are updated at the same variables in lockstep.

At a variable \(v\) that is free under \(\rho _0\) and unset in both \(\sigma _1\) and \(\sigma _2\), the first component \(\gamma \) of the encoder loop SwitchingLemma2.razborovEncode’s go takes the same value at \(v\) whether started from \(\sigma _1\) or \(\sigma _2\).

Characterizes the decoder’s processEntries when run on the auxiliary entries of SwitchingLemma2.processClauseLits followed by a termination marker \((w, \mathrm{false})\) and a remainder: the result is given by folding the decoder’s \(\sigma \)- and \(\rho _0\)-updates over those auxiliary entries, leaving the remainder unconsumed, provided \(t.\mathrm{length} \le w\) and every input literal occurs in \(t.\texttt{zipIdx}\).

If no literal in the input list shares \(l\)’s variable except \(l\) itself, and the initial \(\sigma \) at \(l.\mathrm{var}\) is not \(\mathrm{some}\ l.\mathrm{neg}\), then after SwitchingLemma2.processClauseLits the \(\sigma \) output at \(l.\mathrm{var}\) is still not \(\mathrm{some}\ l.\mathrm{neg}\).

Suppose \((l, idx)\) is in the input list, no other input literal shares \(l\)’s variable, \(\rho _0\, l.\mathrm{var} = \mathrm{none}\) initially, and SwitchingLemma2.processClauseLits still leaves \(\rho _0\) unset at \(l.\mathrm{var}\). Then the remaining path returned by the routine is empty, since \(l\) was never processed because the path ran out first.

If some input pair \(p\) has variable \(v\) and there are at least as many path entries as literals, then the \(\rho _0\) output of SwitchingLemma2.processClauseLits at \(v\) is not \(\mathrm{none}\).

When the encoder returns \((\sigma , [])\) (an empty emitted list), the decoder loop SwitchingLemma2.razborovDecode’s go recovers \(\sigma \) exactly, given that \(\sigma \) and the decoder’s starting restriction \(\sigma _{\mathrm{dec}}\) agree with \(\sigma \) on both free and non-free variables and that \(\sigma \) is unset wherever \(\rho _0\) is unset.

Let \(f\) be a DNF whose terms contain no two distinct literals on the same variable, and let \(t\) be the first term of \(f\) not killed by \(\rho _0\) (as returned by find?). If \(l \in t\) has \(\rho _0\, l.\mathrm{var} = \mathrm{none}\) and \(\sigma \) is unset wherever \(\rho _0\) is, then the first component of the encoder loop SwitchingLemma2.razborovEncode’s go (for any fuel, path, and empty accumulator) at \(l.\mathrm{var}\) is not \(\mathrm{some}\ l.\mathrm{neg}\); the encoder never assigns the free literal \(l\) its negating value, so it does not kill the first surviving clause.