# On bounded depth proofs for Tseitin
formulas on the grid; revisited††thanks:  Supported by the Approximability and
Proof Complexity project funded by the Knut and Alice Wallenberg Foundation.

Johan Håstad and Kilian Risse  KTH Royal Institute of Technology

###### Abstract

We study Frege proofs using depth-$d$ Boolean formulas for the Tseitin
contradiction on $n\times n$ grids. We prove that if each line in the proof is
of size $M$ then the number of lines is exponential in $n/(\log M)^{O(d)}$.
This strengthens a recent result of Pitassi et al. [PRT22]. The key technical
step is a multi-switching lemma extending the switching lemma of Håstad
[Hås20] for a space of restrictions related to the Tseitin contradiction.

The strengthened lemma also allows us to improve the lower bound for standard
proof size of bounded depth Frege refutations from exponential in
$\tilde{\Omega}(n^{1/59d})$ to exponential in $\tilde{\Omega}(n^{1/(2d-1)})$.

##  1 Introduction

Mathematicians like proofs, formal statements where each line follows by
simple reasoning rules from previously derived lines. Each line derived in
this manner, assuming that the reasoning steps are sound, can give us some
insight into the initial assumptions of the proof. A particularly interesting
consequence is contradiction. Deriving an obviously false statement allows us
to conclude that the initial assumptions, also called axioms, are
contradictory. We continue the study of Frege proofs of contradiction where
each line in the proof is a Boolean formula of depth $d$. This subject has a
long tradition, so let us start with a very brief history.

A very basic proof system is resolution: each line of such a proof simply
consists of a disjunction of literals. The derivation rules of resolution are
also easy to understand and simple to implement, but the proof system
nevertheless gives rise to reasonably short proofs for some formulas. It is
far from easy to give lower bounds for the size of proofs in resolution but it
has been studied for a long time and by now many strong bounds are known. An
early paper by Tseitin [Tse68] defined an important class of contradictions
based on graphs that is central to this and many previous papers. For each
edge there is a variable and the requirement is that the parity of the
variables incident to any given node sum to a particular bit which is called
the charge of that vertex. If the sum of the charges is one modulo two this is
a contradiction. For a subsystem of resolution, called regular resolution,
Tseitin proved exponential lower bounds on refutations of these formulas.
After this initial lower bound it took almost another two decades before the
first strong lower bound for general resolution was obtained by Haken [Hak85],
whose lower bound applied to the pigeonhole principle (PHP). Many other
resolution lower bounds followed, but as we are not so interested in
resolution and rather intend to study the more powerful proof system with
formulas of larger, though still bounded, depth $d$ on each line, let us turn
to such proof systems.

The study of proofs with lines limited to depth $d$ dates back several
decades. A pioneering result was obtained by Ajtai [Ajt94] who showed that the
PHP cannot be proved in polynomial size for any constant depth $d$.
Developments continued in the 1990s and polynomial size proof were ruled out
for values of $d$ up to $O(\log\log n)$ for both the PHP [PBI93, KPW95] as
well as the Tseitin contradiction defined over complete [UF96] and expander
graphs [Ben02].

These developments followed previous work where the computational power of the
class of circuits111When the depth is small, there is no major difference
between circuits and formulas so the reader should feel free to ignore this
difference. of depth $d$ was studied [Sip83, FSS84, Yao85, Hås86, Raz88,
Smo87]. It is not surprising that it is easier to understand the computational
power of a single circuit rather than to reason about a sequence of formulas
giving a proof. This manifested itself in that while the highest value of $d$
for which strong bounds were known for size of proofs remained at $O(\log\log
n)$, the results for circuit size extended to almost logarithmic depth.

This gap was (essentially) closed in two steps. First Pitassi et al. [PRST16]
proved superpolynomial lower bounds for $d$ up to $o(\sqrt{\log n})$ and then
Håstad [Hås20] extended this to depth $\Theta(\frac{\log n}{\log\log n})$
which, up to constants, matches the result for circuits.

The key technique used in most of the described results is the use of
restrictions. These set most of the variables to constants which simplifies
the circuit or formulas studied. If done carefully one can at the same time
preserve the contradiction refuted or the function computed. Of course one
cannot exactly preserve the contradiction and to be more precise a
contradiction with parameter $n$ before the restriction turns into a
contradiction of the same type but with a smaller parameter, $n/T$, after the
restriction.

The simplification under a restriction usually takes place in the form of a
switching lemma. This makes it possible to convert depth $d$ formulas to
formulas of depth $d-1$. A sequence of restrictions is applied to reduce the
depth to (essentially) zero making the circuit or formula straightforward to
analyze. The balance to be struck is to find a set of restrictions that leave
a large resulting contradiction but at the same time allows a switching lemma
to be proved with good parameters.

In proof complexity the most commonly studied measure is the total size of a
proof. There are two components to this size, the number of reasoning steps
needed and the size of each line of the proof. In some cases, such as
resolution, each line is automatically bounded in size and hence any lower
bound for proof size is closely related to the number of proof steps. In some
other situation the line sizes may grow and an interesting question is whether
this can be avoided.

This line of investigation for Frege proofs with bounded depth formulas was
recently initiated by Pitassi et al. [PRT22]. They consider the Tseitin
contradiction defined over the grid of size $n\times n$, a setting where
strong total size lower bounds for Frege refutations of bounded depth had
previously been given by Håstad [Hås20]. If each line of the refutation is
limited to size $M$ and depth $d$, then Pitassi et al. [PRT22] showed that the
Frege proof must consist of at least $\exp(n/2^{O(d\sqrt{\log M})})$ many
lines. For most interesting values of $M$ this greatly improves the bounds
implied by the results for total proof size. In particular if $M$ is a
polynomial the lower bounds are of the form $\exp(n^{1-o(1)})$, as long as
$d=o(\sqrt{\log n})$, in contrast to the total size lower bounds of the form
$\exp(n^{\Omega(1/d)})$. Pitassi, Ramakrishnan, and Tan [PRT22] rely on the
restrictions introduced by Håstad [Hås20] but analyze them using the methods
of Pitassi et al. [PRST16].

We study the same Tseitin contradiction on the grid and improve the lower
bounds to $\exp(n/(\log M)^{O(d)})$, a bound conjectured by Pitassi et al.
[PRT22]. These bounds are the strongest bounds that can be proved by the
present methods and even if we cannot match them by constructing actual proofs
we can at least represent the intermediate results of a natural proof by such
formulas. We discuss this in more detail below.

###  1.1 Overview of proof techniques

The structure of the proof of our main result follows the approach of [PRT22]
but relies on proving much sharper variants of the switching lemma.

In a standard application of a switching lemma to proof complexity one picks a
restriction and demands that switching happens to all depth two formulas in
the entire proof. Each formula switches successfully with high probability and
by an application of a union bound it is possible to find a restriction to get
them all to switch simultaneously.

The key idea of [PRT22] is that one need not consider all formulas in the
proof at the same time. Rather one can focus on the sub-formulas of a given
line. It is sufficient to establish that these admit what is called an $\ell$
partial common decision tree of small depth. This is a decision tree with the
property that at each leaf, each of the formulas can be described by a
decision tree of depth $\ell$. It turns out that this is enough to analyze the
proof and establish that it cannot derive contradiction. The key property is
that it is sufficient to only look at the constant number of formulas involved
in each derivation step and analyze each such step separately.

The possibility to compute a set of formulas by an $\ell$ common partial
decision tree after having been hit by a restriction is exactly what is
analyzed by what has become known as a “multi-switching lemma” as introduced
by [Hås14, IMP12]. This concept was introduced in order to analyze the
correlation of a small circuits of bounded depth with parity but turns out to
also be very useful in the current context.

Even though there is no general method, it seems like when it is possible to
prove a standard switching lemma there is good hope to also prove a multi-
switching lemma with similar parameters. This happens when going from [Hås86]
to [Hås14] and when going from [PRST16] to [PRT22]. We follow the same
approach here and this paper very much builds on [Hås20]. We need a slight
modification of the space of restrictions and changes to some steps of the
proof, but a large fraction of the proof remains untouched. Let us briefly
touch on the necessary changes.

The switching lemma of Håstad [Hås20] has a failure probability to not switch
to a decision tree of depth $s$ of the form $(As)^{\Omega(s)}$ where $A$
depends on other parameters. As a first step one needs to eliminate the factor
$s$ in the base of the exponent. This triggers the above mentioned change in
the space of restrictions. This change enables us to prove a standard
switching lemma with stronger parameters and, as a warm-up, we give this proof
in the current paper. This results in an improvement of the lower bound for
total proof size from $\exp(\tilde{\Omega}(n^{1/58d}))$ to
$\exp(\tilde{\Omega}(n^{1/(2d-1)}))$. Even though the exponent’s exponent is
probably still off by a factor of $2$, this is a substantial improvement in
the parameters.

The high level idea of the proof of the multi-switching lemma is that for each
of the formulas analyzed we try to construct a decision tree of depth $\ell$.
If this fails then we take the long branch in the resulting decision tree and
instead query these variables in the common decision tree. A complication that
arises is that the answers on the long path in the local decision tree and the
answers on a potentially long branch in the common decision tree are
different. This causes us to analyze a new combinatorial game on the grid, as
defined in Section 3.1.

###  1.2 Constructing small proofs

Let us finally comment on a possible upper bound; how to construct efficient
refutations. If we are allowed to reason with linear equations modulo two then
the Tseitin contradiction has efficient refutations. In particular on the grid
we can sum all equations in a single column giving an equation containing
$O(n)$ variables that must be satisfied. Adding the corresponding equation for
the adjacent column maintains an equation of the same size and we can keep
adding equations from adjacent columns until we have covered the entire grid.
We derive a contradiction and we never use an equation containing more than
$O(n)$ variables.

If we consider resolution then it is possible to represent a parity of size
$m$ as a set of clauses. Indeed, looking at the equation
$\sum_{i=1}^{m}x_{i}=0$ we can replace this by the $2^{m-1}$ clauses of full
width where an odd number of variables appear in negative form. Now replace
each parity in the above proof by its corresponding clauses. It is not
difficult to check that Gaussian elimination can be simulated by resolution.
Given linear equation $L_{1}=b_{1}$ and $L_{2}=b_{2}$ with $m_{1}$, and
$m_{2}$ variables respectively, and both containing the variable $x$ we want
to derive all clauses representing $L_{1}\oplus L_{2}=b_{1}\oplus b_{2}$. We
have $2^{m_{1}-1}$ clauses representing the first linear equation and the
$2^{m_{2}-1}$ clauses representing the second linear equation. Now we can take
each pair of clauses and resolve over $x$ and this produces a good set of
clauses. If $L_{1}$ and $L_{2}$ do not have any other common variables we are
done. If they do contain more common variables then additional resolution
steps are needed but these are not difficult to find and we leave it to the
reader to figure out this detail. We conclude that Tseitin on the grid allows
resolution proofs of length $2^{O(n)}$.

Let us consider proofs that contain formulas of depth $d$ and let us see how
to represent a parity. Given $\sum_{i=1}^{m}x_{i}=0$ we can divide the
variables in to groups of size $(\log M)^{d-1}$ and write down formulas of
depth $d$ and size $M$ that represent the parity and the negation of the
parity of each group. Assume that the output gate of each of these formulas is
an or. We now use the above clause representation of the parity of the groups
and get a set of $2^{m/(\log M)^{d-1}}$ formulas of size $mM/(\log M)^{d-1}$
that represent the linear equations This means that we can represent each line
in the parity proof by about $2^{n/(\log M)^{d-1}}$ lines of size about $M$.
We do not know how to syntactically translate a Gaussian elimination step to
some proof steps in this representation and thus we do not actually get a
proof, only a representation of the partial results.

###  1.3 Organization

Let us outline the contents of this paper. We start in Section 2 and Section 3
with some preliminaries. In Section 4 we define the set of restrictions used
in the current paper which are almost the same as in [Hås20]. We give some
details how decision trees should be modified using local consistency in
Section 5. The important tool for turning switching lemmas to lower bounds for
proofs is by something called $t$-evaluations and we recall this in Section 6.
Next we show how to construct these evaluations and derive our two main
theorems assuming the new switching lemmas in Section 7. The strengthened
version of the standard switching lemma is given in Section 8 and the
extension to a multi-switching lemma is presented in Section 9. Large portions
of the proof for the standard switching lemma as well as many definitions are
identical to the proof of [Hås20]. We end with some conclusions in Section 10.

##  2 Preliminaries

We have a graph $G$ which we call “the grid” but to avoid problems at the
perimeter we in fact use the torus. In other words we have nodes indexed by
$(i,j)$, for $0\leq i,j\leq n-1$ where $n$ is an odd integer and a node
$(i,j)$ is connected to the four nodes at distance 1, i.e. where one
coordinate is identical and the other moves up or down by 1 modulo $n$. For
each node $v$ we have a charge $\alpha_{v}$ and for each edge $e$ in the graph
we have a variable $x_{e}$. A Tseitin formula is given by a set of linear
equalities modulo 2. That is, for each vertex $v$ in $G$ we have

$\sum_{e\ni v}x_{e}=\alpha_{v}.$

The main case we consider, which we call “the Tseitin contradictions” is when
$\alpha_{v}=1$ for each $v$. We do use more general charges in intermediate
steps and hence the following lemma from [Hås20] is useful for us.

######  Lemma 2.1.

Consider the Tseitin formulas with charges $\alpha_{v}$. If
$\sum_{v}\alpha_{v}=0$ this formula is satisfiable and has $2^{r_{n}}$
solutions where the positive integer $r_{n}$ depends only on $n$ and not on
the value of $\alpha_{v}$.

As a converse to the above lemma, when $\sum_{v}\alpha_{v}=1$ it is easy to
see, by summing all equations, that the system is contradictory. In particular
the Tseitin contradictions with $\alpha_{v}=1$ for all $v$ are indeed
contradictions for graphs with an odd number of nodes. We note that each
Tseitin formula for the grid graph can be written as a 4-CNF formula by having
8 clauses of length four for each node.

We are interested in proofs in the form of deriving the constant false from
these axioms. The exact reasoning rules turn out not to be of central
importance but are stated in Section 6. The important properties of these
rules are that they are sound and of constant size.

The sub-formulas that appear in this proof are allowed to contain only
$\lor$-gates and negations. We simulate $\land$ using $\land
F_{i}=\neg\lor\neg F_{i}$ and we define the depth of a formula to be the
number of alternations of $\lor$ and $\neg$.

##  3 Properties of assignments on the grid and some games

We are interested in solutions to subsystems of the Tseitin contradictions. It
follows from Lemma 2.1 that as soon as we drop the constraints at a single
node we have a consistent system and indeed many solutions.

On a set $X$ of nodes we say that a partial assignment is complete if it gives
values to exactly all variables with at least an endpoint in $X$. The support
of a partial assignment $\alpha$ is denoted by $\operatorname*{supp}(\alpha)$
and is the set of nodes adjacent to a variable given a value. Note that the
support of a complete assignment on $X$ also includes the neighbors of $X$.

We consider partial assignments that give values to few variables and in
particular we are interested in cases where the size of the set $X$ is at most
$2n/3$ and hence cannot touch all rows or columns of the grid. Let $X^{c}$
denote the complement of $X$.

In this case, $X^{c}$ contains a giant component containing almost all nodes
of the grid. This follows as there are at least $n/3$ complete rows and
columns in $X^{c}$ and the nodes of these rows and columns are all connected.
The other, small, components of $X^{c}$ are important to control as an
assignment on $X$ might fail to extend in a consistent way to such a
component. To avoid this problem, for a set $X$ we let the closure of $X$,
$\mathrm{cl}(X)$ denote all nodes either in $X$ or in small connected
components of $X^{c}$. Note that $\mathrm{cl}(X)^{c}$ is exactly the giant
component of $X^{c}$.

######  Definition 3.1.

An assignment $\alpha$ with $X=\operatorname*{supp}(\alpha)$ is locally
consistent if it can be extended to a complete assignment on $\mathrm{cl}(X)$
that satisfies all parity constraints on this set.

We extend this definition to say that two assignments are consistent with each
other if they do not give different values to the same variable and when you
look at the union of the two assignment this gives a locally consistent
assignment. The following lemma from [Hås20] is many times useful.

######  Lemma 3.2.

Suppose $\alpha$ is a locally consistent assignment where
$|\operatorname*{supp}(\alpha)|\leq n/2$ and $x_{e}$ a variable not in
$\operatorname*{supp}(\alpha)$. Then there is a locally consistent assignment
$\alpha^{\prime}$ that extends $\alpha$ and gives a value to $x_{e}$.

We are interested in complete assignments on some sets $X$ and the grid and in
particular how it looks from the outside. Let a border assignment be an
assignment to the variables with one end-point in $X$ and one outside $X$.
Such an assignment $\alpha$ is achievable iff there is an assignment that has
the border assignment $\alpha$ and satisfies the parity conditions on $X$.

######  Lemma 3.3.

Let $X$ be a connected set. The a border assignment $\alpha$ is achievable iff
the parity of the bits $\alpha$ equals the parity of the size of $X$.

###### Proof.

By induction on $|X|$, and the base case when $X$ is a singleton is obvious.
For the induction step take any $v$ such that removing $v$ keeps $X$
connected. Of the variables next to $v$ some are forced by the border
assignment. Fix the rest of the variables next to $v$ that satisfies the
parity constraint at $v$. Apply induction to $X$ with $v$ removed and the
border assignment including the just made assignment to the variables next to
$v$. ∎

By a simple extension we have the following.

######  Lemma 3.4.

Let $X$ be a connected set. The a border assignment $\alpha$ is achievable by
a locally consistent assignment iff the parity of the bits $\alpha$ equals the
parity of the size of $X$ and this is true also for the border assignment of
any small connected component of the complement of $X$.

A process that is useful is the following dynamic matching game. We have two
players, one adversarial player that supplies nodes while the other, matching
player $P_{M}$, is supposed to dynamically create a matching that contains the
nodes given by the adversarial player. Our strengthened lower bound for the
size of a proof uses the same combinatorial lemma as the proof in [Hås20]
namely the following.

######  Lemma 3.5.

[Hås20] When the dynamic matching game is played on the $n\times n$ grid,
$P_{M}$ can survive for at least $n/2$ moves.

The purpose of this lemma is to find which variables to include in the
extended decision tree used. As discussed in the introduction our new lower
bound for the number of lines of a proof with short lines needs a multi-
switching lemma and it turns out that the decision which variables to include
is described by a more complicated combinatorial game. We now discuss this
game. The reader that wants motivation for this game is encouraged to first
read the proof of the standard switching lemma to find the reason for Lemma
3.5 and then start reading the proof of the multi-switching lemma.

###  3.1 Another game on the grid

The game is played on the grid between an adversary $A$ and a player $P$. They
take turns picking vertices and edges on the $n\times n$ grid. Once a vertex
is picked it can never be picked again. The set of picked vertices is called
$S$. The vertices outside $S$ are called “free”. The total number of picked
nodes always remains less than $n/2$ and hence there is always a large
connected component in the complement of $S$. Other connected components in
the complement are called “small”. Some of the picked elements are called
“active”.

The task of $P$ is to pick as few vertices as possible such that the following
properties hold.

  1. 1.

The number of picked nodes has the correct parity in some special components
of $S$ described below.

  2. 2.

The size of any small component in the complement of $S$ is even.

The game starts with an empty grid, and takes place in rounds where $A$
decides when to start the next round. $A$ can do two types of moves.

  1. 1.

Pick an arbitrary new vertex $v$ and make it active. This is called a “simple”
move.

  2. 2.

Declare that a round is over. In this case $A$ can make any edge between an
active vertex and a free vertex active. Each connected component must have an
even number of activated edges leading in to it.

This second type of move is called a completion move. When this move is
completed all vertices become inactive and the next round starts.

After a simple move $P$ must pick some vertices to form a connected component
of even size jointly with the just placed vertex. $P$ must also make sure that
each connected component of the complement is of even size. Any vertex picked
by $P$ in response to a simple move becomes active. Note that in this
situation $P$ picks an odd number of vertices and hence at least one.

After a completion move $P$ must pick the free vertices with at least one
adjacent active edge. It may pick some more vertices to achieve the following.

  1. 1.

The parity of the size of each connected component of the just picked vertices
must equal to the parity of active edges adjacent to it.

  2. 2.

The number of vertices in any small connected component in the complement is
even.

Although this looks complicated please note that if the there is only one
active edge going in to the nodes $P$ must pick and these do not split any
connected component of the complement, then these forced nodes is all that $P$
needs to select.

What forces $P$ to act in general is the creation of small odd size components
in the complement of $S$ due to making the “obvious” choices. For any such
component $C$, $P$ needs to add vertices to $S$ to make it of even size. It is
also restricted to only adding vertices adjacent to a supplied starting
vertex. This vertex is in $S$ but connected to at least some vertex in $C$. We
call this “evenizing” with starting point $w$. All connected components of the
complement created in this process must be made of to be of even size. It is
simple to see that this can always be done, simply add any vertex adjacent to
$w$. If this does not split $C$ in to at least two components then $P$ is
done. Otherwise $P$ can simply recurse on any created component of odd size
with the chosen vertex as the starting point. We must prove that, over the
course of the entire game, $A$ cannot force $P$ to add too many vertices. To
get some understanding of the problems, let us first give an example where $P$
is forced to make many moves.

Example. Suppose $C$ consists of the vertices $(1,x)$ for $1\leq x\leq t$
jointly with $(2,x)$ for even $x$ at most $t-1$ and $(0,x)$ for odd $x$ at
most $t-1$. This has an odd number of vertices (in fact $2t-1$) and suppose
the starting vertex is $(1,0)$. $P$ needs to add $(1,1)$ since this is the
only vertex in $C$ connected to $(1,0)$. This creates the isolated vertex
$(0,1)$ and a component of size $2t-3$ that is very similar to the starting
component. It is easy to see that $P$ ends up picking all vertices of this
component.

We set up a potential function to prove that such massive responses as in the
example can only happen rarely. For each connected component of the complement
consider its edges to elements of $S$. For each edge to an active vertex we
assign four points and for each other edge one point. Suppose the total number
of points for component $C_{i}$ is $f_{i}$ and this number is called the score
of $C_{i}$. We have a parameter $T$ and we say that each component of size at
most $T$ is ultra small. We later fix $T$ to a suitable constant. A component
that is not ultra small is called sizeable. This includes the large component.
We now define the potential as

$\sum_{i}f_{i}+G-D(F-1)$

where the sum is over components that are sizeable, $F$ the number of
components that are sizeable, $D$ is a constant to be chosen suitably, and $G$
is the number of ultra small components. For $G$ we only count a component the
first time it becomes ultra small. Further splitting of an ultra small
component is ignored. The reason for using $(F-1)$ is that we want to start
the potential at 0 and hence not count the large component in this number.

We want to prove that this potential increases by at most a constant for each
simple move and decreases by at least one half for other moves. By setting $T$
large enough (after we have chosen $D$) we make sure that $f_{i}\geq 2D$ for
any component of size at least $T$.

Let us first analyze simple moves. When $A$ chooses a vertex it might increase
$\sum_{i}f_{i}$ by at most 16\. This might also cause a component of the
complement of $S$ to split. To analyze the cost of such a split we first pay
the increase by the addition of the extra vertex to $S$ in the form of
increase to $f_{i}$. We then see how the splitting of a component of the
complement affects the potential. First note that splitting an ultra small
component does not affect the potential (remember that we do not count this as
an increase in $G$) and thus we are interested in splitting a sizeable
component. We have sequence of simple lemmas.

######  Lemma 3.6.

If a sizeable component splits into ultra small components then the potential
decreases by at least $D-4$.

###### Proof.

Suppose $C_{i}$ splits. This means that the term $f_{i}-D$ disappears in the
potential. By construction this is at least $D$. We might have an increase of
$G$ by 4 but no other increase. The lemma follows. ∎

Next we have.

######  Lemma 3.7.

If a sizeable component splits and the result contains at least two sizeable
components then the potential decreases by at least $D$.

###### Proof.

The creation of a sizeable component increases $F$. Any ultra small component
created increases $G$ by one but at the same time its score is removed from
the sum causing a decrease of that sum by at least 4\. ∎

Finally we analyze the third possibility.

######  Lemma 3.8.

If a sizeable component splits into a sizeable component and one or more ultra
small components the potential decreases by at least three for each component
split off.

###### Proof.

The value of $F$ does not change. Any ultra small component created increases
$G$ by one but its score of at least 4 is removed from the sum
$\sum_{i}f_{i}$. ∎

The above lemmas imply that the splitting of components only decreases the
potential. What remains is to analyze the cost when $P$ is forced to evenize
an odd size component. By “cost” we here mean increase in potential. We might
have a negative cost which is a decrease in potential.

######  Lemma 3.9.

The cost of evenizing a component with an active starting point is at most
$11-m/2$ where $m$ is the number of moves made by $P$ in sizeable components.
The cost of evenizing an ultra small component is 0.

###### Proof.

We prove the lemma by induction over the size of the component. If the
component is ultra small then no term of the potential can change so there is
no cost.

As a first attempt let $P$ pick an arbitrary vertex, $v$, next to the starting
which we call $w$. If this does not result in any new odd size component we
are done. We have added at most three more edges at cost four each while
eliminating the cost of $(v,w)$. As a result $f_{i}$ might have increased by
at most 8 giving the same increase in the potential and $P$ has made one move
in sizeable component.

Now suppose that choosing $v$ creates some new odd size components that have
to be evenized. We know that this number must be even and since any component
has to be adjacent to $v$ and since $v$ has at most three neighbors other than
$w$ there must be exactly two such components and call them $C_{1}$ and
$C_{2}$. Let $v_{i}$ be an element in $C_{i}$ that is a neighbor of $v$.
Suppose the scores of these two components are $f_{1}$ and $f_{2}$ and the
score of the component that splits is $f$. Note that $f$ is measured before
$v$ is placed in $S$ while $f_{1}$ and $f_{2}$ are measured after this has
happened and thus we need to keep track of what happens to edges next to $v$.
One fact to our advantage is that while $(v,w)$ was counted in $f$ its four
points do not appear in neither $f_{1}$ or $f_{2}$.

There are a number of cases depending on the status of the fourth neighbor of
$v$ (on top of $w$, $v_{1}$ and $v_{2}$). It can be in a third, new,
component, be an element of $S$, or belong to $C_{1}$ or $C_{2}$. In the first
case that third component is of even size and hence need not be evenized. If
it is sizeable we get a decrease in potential of at least $D$ and if it is
ultra small by at least three. In either case we are doing strictly better
then if this node belongs to $S$ and hence we can ignore this case and we may
assume that we get exactly two new components.

If neither of these two new components is ultra small, then the potential
decreases by Lemma 3.7. The total increase in the score is bounded by 8 as we
eliminate the score of $(v,w)$ and add at most 3 new edges with three points
each. The cost, by induction, to evenize $C_{1}$ and $C_{2}$ is at most
$22-(m_{1}+m_{2})/2$ where $m_{i}$ is the number of moves of $P$ made in
sizeable components when evenizing $C_{i}$. The total change to the potential
is thus bounded from above by $30-(m_{1}+m_{2})/2-D$ and making sure that
$D\geq 20$ the lemma follows in this case.

Now suppose $C_{1}$ and $C_{2}$ are both ultra small. Then $G$ increases by
two but we have a decrease of $D$ in potential by Lemma 3.6 and in this case
we in fact have a total decrease in the potential and no more moves in
sizeable components. This establishes the lemma in this case.

Finally assume that $C_{1}$ is ultra small while $C_{2}$ is not. In this case
we get an increase of $G$ by one while $F$ does not change. We need to analyze
the change in scores and the cost of possible recursive calls.

If the fourth neighbor of $v$ (on top of $v_{1}$, $w$ and $v_{2}$) does not
belong to $C_{2}$ then $f_{2}\leq f-3$. This follows as the only new edge in
$C_{2}$ that was not present in $C$ is $(v_{2},v)$ but this is compensated by
$(v,w)$ being present in $C$ but not in $C_{2}$. On top of this at least three
points have disappeared from $f$ when forming $C_{1}$. For the recursive costs
we have that, by induction, the cost to evenize $C_{2}$ is at most
$11-m_{2}/2$. As $C_{1}$ is ultra small we have no cost for its recursive
call. The net cost is thus bounded from above by $1-3+11-m_{2}/2\leq 10-m/2$
and the lemma follows also in this case.

Finally consider the case when the missing neighbor of $v$, call it
$v_{2}^{\prime}$, belongs to $C_{2}$. This causes the potential addition of 4
to $f_{2}$ by the edge $(v,v_{2}^{\prime})$ and this needs to be addressed.
Unfortunately this leads to a rather tedious case analysis.

Suppose without loss of generality that $w$ is to the left of $v$. We first
have three cases whether $v_{1}$ is to right, above, or below $v$. The cases
above and below are symmetric so in fact we can drop the case of $v_{1}$ being
below $v$.

Let us assume that $v_{1}$ is to the right of $v$ and $v_{2}$ above and
$v_{2}^{\prime}$ is below. The situation looks like in Figure 1, where we note
that the vertices to the right of $v_{2}$ and $v_{2}^{\prime}$ must be in $S$
to make removing $v$ disconnect $C_{1}$ and $C_{2}$.

$w$$v$$v_{1}$$v_{2}$$v_{2}^{\prime}$ Figure 1: The larger circles are elements
of $S$

Now suppose that we can remove $v_{2}$ from $C_{2}$ and keep it connected.
Then $P$ can pick $v$ and $v_{2}$ and the remaining part of $C_{2}$ is even
and there is no recursive call. Let us compare $f_{2}$ and $f$. We have lost
at least 3 points from $f$ that now belongs to $C_{1}$. We also lost 4 points
from $(w,v)$ becoming internal of $S$. We gain 4 points from
$(v,v_{2}^{\prime})$. Finally we can have two new edges next to $v_{2}$ (going
left and up). There is a net gain in potential of at most 5 and the lemma
follows also in this case as $P$ only made two moves.

The case when we can remove $v_{2}^{\prime}$ and keep $C_{2}$ is connected is
symmetric and hence we need to consider the case when both create new
components and thus we can assume that both removing $v_{2}$ and
$v_{2}^{\prime}$ splits $C_{2}$. The two components that $C_{2}$ splits to
when $v_{2}$ is removed must then be connected to $v_{2}$ from top and from
the left and for $v_{2}^{\prime}$ the two components attach from left and
below.

Put both of $v_{2}$ and $v_{2}^{\prime}$ into $S$. Then $C_{2}$ splits in to
three components, two of which might have to be evenized. If two of these are
sizeable then we have increased $F$ by one. The analysis is very much as
before and the extra decrease of $D$ provided by Lemma 3.7 well compensates
for the two recursive evenizing calls.

The case when $C_{2}$ splits into three ultra small components is also very
similar to previous cases. There is no recursive call and Lemma 3.6 provides a
large decrease. The case that remains to analyze is that we have exactly two
ultra small components.

We have (remember we also have $C_{1}$) created three ultra small components.
Each decreases the score by at least three and increase $G$ by three for a net
decrease of 6. The edge $(v,w)$ is now interior to $S$ while it is counted in
$f$. The only new edges in $f_{2}$ are one from each of $v_{2}$ and
$v_{2}^{\prime}$. Thus we have net decrease of 2. We still have one recursive
call on the remaining component that is sizeable but this costs, by induction,
at most $11-m/2$ where $m$ is the number of nodes chosen by $P$ in this
recursive call. The lemma follows in the case when both $v_{2}$ and
$v_{2}^{\prime}$ disconnect $C_{2}$.

We have the final case when $v_{2}$ is to the right of $v$ and
$v_{2}^{\prime}$ is below. Suppose first that adding either $v_{2}$ or
$v_{2}^{\prime}$ to $S$ does not disconnect $C_{2}$. Then if $P$ removes this
vertex and $v$ and there is no recursive call. Suppose it removes
$v_{2}^{\prime}$ (the case of $v_{2}$ being similar). Then we might get three
new edges costing four points next to $v_{2}^{\prime}$ and the edge
$(v,v_{2})$ is of the same cost while the cost of $(v,w)$ disappears. At least
three points disappear with the creation of $C_{1}$ while there is an increase
of one for $G$. This implies that there is an increase of at most 10 and as
$P$ has picked two vertices the lemma follows in this case.

We need to analyze the situation when both removing either $v_{2}$ and
$v_{2}^{\prime}$ disconnects $C_{2}$. Let us first observe that the vertex
$v_{2}^{\prime\prime}$ in the picture belong to $C_{2}$ since otherwise
removing $v_{2}$ does not disconnect $C_{2}$. The situation is like in Figure
2.

$w$$v$$v_{2}$$v_{1}$$v_{2}^{\prime}$$v_{2}^{\prime\prime}$ Figure 2: The
larger circle in an elements of $S$

Now, consider putting all four vertices $v$, $v_{2}$ $v_{2}^{\prime}$, and
$v_{2}^{\prime\prime}$ in $S$. This splits $C_{2}$ into a number of components
as we may have one component hanging off each side of the square. If at least
two are sizeable we get an increase in $F$ and Lemma 3.7 takes care of of the
local costs and we can apply induction. Similarly if all components are ultra
small Lemma 3.6 tells us that there is a decrease in potential. We need to
analyze what happens when exactly one component is sizeable.

In fact we must have three ultra small components hanging off the square each
giving a net decrease of at least 2. Indeed we have $C_{1}$ and the ultra
small components created when $v_{2}$ and $v_{2}^{\prime}$ are removed. Since
we have a sizeable component we must have one component hanging off each of
the four sides of the cube, as we cannot have two components attaching to the
same side.

We only have one recursive call with a cost of $11-m/2$, and we have net
decrease in 6 from the ultra small components. Finally for edges, we do not
any more count the cost of $(v,w)$ and we can only have two new edges entering
the component of the recursive call. The new edges to the ultra small
components do not count. Thus apart from the recursive call we have a net
decrease of 2 and this compensates for the four points added by $P$. ∎

The above takes care of all simple moves. Let us look at completion moves.

######  Lemma 3.10.

A completion decreases the potential by at least the number of active edges
chosen by $A$. This includes the forced response by $P$

###### Proof.

The first that happens is that an edge which costs 4 is replaced by an
inactive vertex next to it. This results in at most three edges of cost one
and is hence a decrease of at least one in potential. If several active edges
go to the same vertex $P$ has to add two vertices but this gives a decrease of
at least two. Now unless this causes a split of a component we are done.

If it splits an ultra small component then there is no further change in the
potential. If it splits a sizeable component then we might have to evenize two
components and the following lemma is what we need.

######  Lemma 3.11.

The cost of evenizing a component with an inactive starting point is at most
$3-m$ where $m$ is the number of vertices added by $P$ to sizeable components.
The cost of evenizing an ultra small component is at most 0.

Let us assume this lemma then finish the proof of Lemma 3.10. As many times
previously unless we get exactly one non ultra small component it is easy to
prove that there is a decrease so assume that this is the case. Each ultra
small component decreases the potential by a least three and this is
sufficient to pay for the evenizing of the component and this is demonstrated
by Lemma 3.11. ∎

The proof of Lemma 3.11 is surprisingly much simpler than the proof of Lemma
3.9. The key difference is that new edges added only cost one and not four.
This makes it much easier to compensate the cost of new edges by the loss in
potential due to the appearance of ultra small components.

###### Proof of Lemma 3.11.

If the response of putting a vertex, $v$, next to the starting vertex is
sufficient then we have $m=1$ and the potential increases by at most 2 as
three edges are added and one is removed. The lemma is thus true in this case
and let us analyze what happens to the potential if $v$ causes the component
of the complement to split. As before, unless it is a sizeable component that
splits and the result is exactly one sizeable component and one or more ultra
small components, we do have a substantial decrease in the potential due to
the loss of a term $D$.

As in the previous proof the worst case is when $v$ splits the component into
two components $C_{1}$ and $C_{2}$ where the first is sizeable and the the
second is ultra small and the third neighbor of $v$ belongs to $C_{1}$. In
this case we have added two more edges of $v$ into $C_{1}$. We have removed
one edge (between $v$ and the starting point) and lost the cost of at least
three edges that are now part of $C_{2}$. This is a net loss of two to the
potential. We need to evenize $C_{1}$ and this cost by induction at most
$3-m_{1}$ if $P$ picks $m_{1}$ vertices in this process. Finally we have one
more ultra small component and thus the total cost is at most $2-m_{1}$. Since
$P$ picks $m_{1}+1$ vertices in total, the lemma follows. ∎

We finally state the conclusion of this section.

######  Lemma 3.12.

If $A$ makes $s$ simple moves in the game, then the total number of moves is
bounded by $O(s)$.

###### Proof.

The potential increases by $O(1)$ for each simple move of $A$. The evenizing
of any odd component created costs at most $O(1)$ but is decreased by $1/2$
for any vertex chosen by $P$ is a sizeable component. We conclude that the
total number of moves in sizeable components is at most $O(s)$.

As the number of ultra small component created is bounded by the potential,
their number is $O(s)$. In each such component there are $O(1)$ moves. ∎

##  4 Restrictions

We use (essentially) the same space of random restriction as [Hås20]. The only
difference is the choice in the number of live centers in the partial
restrictions. This is the parameter $k$ below which changes its value from
$Cs(n/T)^{2}$ to $C\log n(n/T)^{2}$. For completeness we repeat all definitons
from [Hås20] but we keep the description brief and for intuition and
motivation we refer to [Hås20].

###  4.1 Full restrictions

In an $n\times n$ grid we make sub-squares of size $T\times T$ where $T$ is
odd. In each sub-square we choose222For simplicity we assume that some
arithmetical expressions that are supposed to be integers are in fact exact as
integers. By a careful choice of parameters this can be achieved but we leave
this detail to the reader. $\Delta=\sqrt{T}/2$ of the nodes and call them
centers. These are located evenly spaced on the diagonal of the $3T/4\times
3T/4$ central sub-square. This implies that they have separation
$3\sqrt{T}/2=3\Delta$ in both dimensions. A schematic picture of this is given
in Figure 3.

$T$$T$ Figure 3: The centers and central areas

The centers in neighboring sub-squares are connected by paths that are edge-
disjoint except close to the endpoints. Let us describe how to connect a given
center to a center in the sub-square on top. As there are $T/4=\Delta^{2}$
rows between the two central areas, for each pair of centers (the $j$th
center, $c_{j}$ in the bottom sub-square and $i$th center $c_{i}^{\prime}$ in
the top sub-square) we can designate a unique row, $r_{ij}$ in this middle
area.

To connect $c_{j}$ to $c_{i}^{\prime}$ we first go $i$ steps to the left and
then straight up to the designated row $r_{ij}$. This is completed by starting
at $c_{i}^{\prime}$ and then going $j$ steps to the right and down to the
designated row. We finally use the appropriate segment from the designated row
to complete the path (which might be in either direction). A picture of this
is given in Figure 4. We index the centers from $1$ to $\Delta$ and hence each
path consists of 5 non-empty segments. The first and last segments are totally
within the central area while the middle segment is totally in the area
between the central areas. Segments two and four go from the central areas to
the area in-between.

$c_{j}$$i$$r_{ij}$$j$$c_{i}^{\prime}$ Figure 4: A path

Connecting $c_{j}$ to a center $c_{i}^{\prime}$ in a sub-square to the left is
done in an analogous way. There is a unique column $c_{ij}$ reserved for the
pair and the path again consists of five non-empty segments. The first and
last segments consist of $i$ vertical edges up from $c_{j}$, and $j$ vertical
edges down from $c_{i}^{\prime}$. We add horizontal segments connecting to the
designated column $c_{ij}$ the and middle segment is along this column. The
below lemma is proved in [Hås20].

######  Lemma 4.1.

The described paths are edge-disjoint except for the at most $\Delta$ edges
closest to an endpoint. For each edge $e$, if there is more than one path
containing $e$, these paths all have the same endpoint closest to $e$.

We let the term closest endpoint of an edge denote the closest endpoint
breaking ties in an arbitrary way. The key property we need is that the
“closest endpoint” of a path through an edge is uniquely defined by the edge.

We define the direction of a path to be the relative positions of the sub-
squares of its two endpoints. It is true that the paths are undirected but at
times when we consider paths from a fixed center $v$ it is convenient to think
of such paths as starting at $v$ and thus speak of paths going left or right
from $v$ rather than sideways. We note that apart from having the same closest
endpoint, all paths through one fixed edge $e$ have the same direction.

A restriction is defined by first choosing one center in each $T\times T$ sub-
square and then the paths described above connecting these centers. Note that
these paths are edge-disjoint. The chosen centers naturally form a $n/T\times
n/T$ grid if we interpret the paths between the chosen centers as edges. We
proceed to make the correspondence more complete by assigning values to
variables.

We choose a solution to the Tseitin formula with charges 0 at the chosen
centers and 1 at other nodes. As the number of chosen centers is odd, by Lemma
2.1, there are many such solutions. For variables not on the chosen paths
these are the final values while for variables on the chosen paths we call
them suggested values.

For each path $P$ between two chosen centers we have a new variable $x_{P}$
and for each variable $x_{e}$ on $P$ it is replaced by $x_{P}$ if the
suggested value of $x_{e}$ is 0 and otherwise it is replaced by $\bar{x}_{P}$.

We claim that with these substitutions we have reduced the Tseitin problem on
an $n\times n$ grid to the same problem on an $n/T\times n/T$ grid. This is
true in the sense that we have an induced grid when we interpret paths as new
edges and we need to see what happens to the axioms.

Given a formula $F$ we can apply a restriction $\sigma$ to it in the natural
way resulting in a formula denoted by $F\lceil_{\sigma}$. Variables given
constant values are replaced by constants while surviving variables are
replaced by the appropriate negation of the corresponding path-variable. A
restriction has a natural effect on the Tseitin contradiction as follows.

  * •

The axioms for nodes not on a chosen paths are all reduced to true as all
variables occurring in them are fixed in such a way that the axioms are true.

  * •

The axioms for interior nodes of a chosen path are reduced to tautologies as
the axiom is true independent of the value of the involved variable(s)
$x_{P}$. This is true as flipping a single $x_{P}$ changes the value of two
variables next to any such node.

  * •

The axioms at the chosen centers turn into the axioms of the smaller instance.

These just defined restrictions are called full restrictions and a typical
full restriction is denoted by $\sigma$. Note that these full restrictions are
really “affine restrictions” in the vocabulary of [RST15] as they do not only
assign values to variables but also identify several old variables with the
same new variable that might also be negated. For simplicity, however, we keep
the simpler term “restrictions”.

###  4.2 Partial restrictions and pairings

A typical partial restriction is called $\rho$ and as we mostly discuss
partial restrictions we simply call them “restrictions” while we use the term
“full restrictions” when that is what we have in mind. At the same time as
describing partial restrictions we give a probability distribution on such
restrictions.

Let $k$ be an odd integer of the form $C\log n(n/T)^{2}$ for a constant $C$ to
be determined. The first step of constructing $\rho$ is picking $k$ centers
uniformly at random from the set of all $\Delta(n/T)^{2}$ centers defined in
the previous section. These are the alive centers. In the future we only
consider the case when the number of live centers in each sub-square is
between a factor $.99$ and $1.01$ of its expected value $C\log n$. By choosing
$C$ appropriately the probability of this being false is can be made to be
$1/n$.

We define charges that are 0 for all live centers and 1 for dead centers. As
the number of live centers is odd we can apply Lemma 2.1 and pick a random
solution with these charges to the Tseitin formula. For edges not on paths
between live centers these are final values while for variables on such paths
we call them preferred values.

The choice of the centers together with the fixed and preferred variables is
denoted by $\rho$. The choice of $\rho$ is the main probabilistic event. Note
that by Lemma 2.1 the number of possible values for fixed and preferred values
is independent of which centers are alive and even of $k$ as long as it is
odd.

We now describe how to turn a partial restriction $\rho$ into a full
restriction $\sigma$. Choose one center to survive in each sub-square333This
choice can be done in an arbitrary way but to be definite let us choose the
center from the lowest numbered row.. These are called the chosen centers and
paths between such centers correspond to the variables that remain and are
called chosen paths. Centers that were alive through the first part of the
process but are not chosen are called non-chosen. The centers killed already
by $\rho$ are simply called dead. We proceed to define a pairing.

######  Definition 4.2 (pairing).

A pairing $\pi$ is a graph supported on the non-chosen centers. Each component
of $\pi$ is either a single edge or a star of size four with one center and
three nodes of degree one. Connected centers are located in adjacent sub-
squares.

The following lemma follows from the proof of the corresponding lemma from
[Hås20] which had the paramter $s$ instead of $\log n$.

######  Lemma 4.3.

If each sub-square has between $.99C\log n$ and $1.01C\log n$ non-chosen
centers, a pairing $\pi$ exists.

Let us establish some notation. As the original grid is also a graph with
edges we from now on use the term “grid-edges” to refer to edges in the
original grid. The chosen centers form a smaller grid and this also has edges
and we call these “new grid-edges”. We only consider paths in the original
grid and we keep the shorter term “path” for these. In other words, from now
on an “edge” is a connection between two live centers and corresponds to a
path in the grid-graph. A “new grid-edge” corresponds to a chosen path and is
thus also an edge in the graph of the live centers. We say that two chosen
centers are neighbors if they are in adjacent sub-squares.

Some edges are conflicting in that we do not allow them to be present in the
graph at the same time. More precisely we allow at most one path in each of
the four directions from a center. As picking a path corresponds to changing
the variables on this path this is the same as saying that the variables can
only change values at most once.

As stated above $\pi$ makes it possible to turn $\rho$ into $\sigma$.
Variables not on live paths take their fixed values. Variables on live paths
but not on chosen paths take their preferred values unless they are on a path
chosen by $\pi$ in which case these values are negated. On the chosen paths,
the preferred values now becomes suggested and this completes the description
of $\sigma$. Thus $\sigma$ is obtained deterministically from $\rho$ and $\pi$
and when we want to stress this dependence we sometimes write
$\sigma(\rho,\pi)$.

We use the term “preferred values” as a vast majority of the variables will
eventually be fixed to these values as very few variables appear on the paths
of $\pi$ or turn into suggested values. On the other hand “suggested values”
are much less certain as the path-variables should be thought of as equally
likely to be 0 and 1 and thus these variables are equally likely to take also
the non-suggested value.

As an intermediate between $\rho$ and the full restriction $\sigma$ we have
$\rho$ and some information in the form of existence or non-existence of
edges. We have the following definition.

######  Definition 4.4 (information piece).

An _information piece_ is either in form of an edge $(v,w)$ for two centers
$v$ and $w$ or $(v,\delta,\bot)$ where $v$ is a center and $\delta$ is a
direction (i.e. “left”, “right” “up” or “down”). The former says that there is
an edge from $v$ to $w$ while the latter says that there is no edge from $v$
in the direction $\delta$.

We note that, as edges are undirected, $(v,w)$ and $(w,v)$ denote the same
information. We also use sets of information pieces.

######  Definition 4.5 (consistent information set).

An _information set_ $I$ is a collection of information pieces. Its _support_
, denoted by $\operatorname*{supp}(I)$, is the set of centers mentioned in
these pieces. An information set $I$ is _consistent_ if

  1. 1.

it does not have two different pieces of information from the same center in
one fixed direction, and

  2. 2.

if $I$ has information in all four directions from a center $v$ then it has an
odd number of edges touching $v$.

A partial assignment to some path-variables naturally corresponds to a set of
information pieces. An assignment of 0 to a path-variable gives two non-edges,
in the appropriate directions, with closest end-points at the two chosen
centers connected by this path. An assignment of 1 gives an information piece
in the form of an edge between the two chosen centers. We use the term
“consistent” both for sets of information pieces and partial assignments.
Consistency for assignments requires an odd number of ones adjacent to any
center that has all its variable assigned and this exactly corresponds to the
property of information pieces in all four directions in the definition above.
This makes the two notions close and hence using “consistent” for both should
hopefully not confuse the reader.

Jointly with $\rho$ an information set fixes the values of some more variables
as follows.

######  Definition 4.6 (forcing).

Let $\rho$ be a restriction and $I$ an information set. A variable $x_{e}$ is
considered forced by $(\rho,I)$ iff either its closest endpoint, $v$, is not
live in $\rho$ or if the information of $v$ in the direction of $e$ is
contained in $I$. It is forced to its preferred value in $\rho$ unless the
relevant information piece states that there is an edge from $v$ in the
direction of $e$ that corresponds to a path that passes through $e$ in which
case it takes the opposite value. Variables not on live paths take the value
given by $\rho$.

There are other situations where the value of a variable might be determined
by $\rho$ and $I$, such as the lack, or scarcity, of live centers in a sub-
square but we do not use this information in the reasoning below. We need the
notion of a closed information set.

######  Definition 4.7 (closed information set).

An information set $I$ is closed if $I$ is consistent and for each
$v\in\operatorname*{supp}(I)$, the set $I$ contains the information in all
four directions.

The definition implies that for any $v\in\operatorname*{supp}(I)$, in any
direction $\delta$ where there is not an element of $\operatorname*{supp}(I)$,
we have a non-edge $(v,\delta,\bot)$. When considered as a graph such an
information set is an odd-degree graph (with degrees one and three) on the
centers of $\operatorname*{supp}(I)$.

Note that if we have a closed information set $I$ then if we consider all
variables forced by $(\rho,I)$ this can be described by a restriction where
the centers in the $\operatorname*{supp}(I)$ are killed. We simply negate the
values of any preferred variable on any path in $I$ and then forget that the
centers in $\operatorname*{supp}(I)$ were alive.

Thus, if we let such a closed information set operate on a restriction $\rho$
we get a restriction with fewer live centers where the number of killed
centers is exactly the number of centers in the support of the corresponding
graph.

###  4.3 Generalized restrictions

In our proof we allow generalized (partial) restrictions. These are like
standard restrictions but we allow the violation of the Tseitin condition at
some dead centers. Such centers are called bad and we keep a close track on
their number. These generalized restrictions are only used for book-keeping
reasons.

##  5 Decision trees

We have decision trees where each internal node is marked with a variable and
the outgoing edges are marked with 0 and 1. The leaves of a decision tree are
labeled by 0 and 1. We allow decision trees of depth 0 which are constants 0
or 1.

All decision trees considered in this paper have a depth that is smaller than
half the dimension of the grid we are currently considering. For each branch
in a decision tree there is minimal partial assignment, $\tau$ such that any
extension of this partial assignment creates an assignment that follows this
path. We use this $\tau$ to identify that branch and we call it consistent if
$\tau$ is consistent in the sense of Definition 3.1.

We trim decision trees to maintain the property that all branches of a
decision tree are consistent. When a decision tree is created this is not a
problem but trimming takes place when we consider what happens under a partial
assignment $\tau$ or a full restriction $\sigma$. In that latter case, the
initial decision tree uses the variables $x_{e}$ while the resulting decision
tree uses the new variables $x_{P}$.

We sometimes think of a decision tree $T$ as the set of all branches leading
from the root to the leaves. These have labels and fit together in a tree
structure and each corresponds to a partial assignment $\tau^{\prime}$ as
discussed above. When creating the decision tree after $\tau$ or $\sigma$ the
idea is to keep all branches that are consistent with the new information.

In the case of a partial assignment $\tau$ we keep all branches corresponding
to $\tau^{\prime}$ such that $\tau$ and $\tau^{\prime}$ are consistent as
discussed after Definition 3.1. In the case of a full restriction $\sigma$ the
situation is not difficult but slightly more complicated so let us define this
explicitly.

The assignment $\tau^{\prime}$ assigns values to some variables $x_{e}$. Some
of these are given values by $\sigma$ while the rest are now on chosen paths.
To be consistent we require that for the variables given values by both
$\sigma$ and $\tau^{\prime}$, the two values agree. For each variable $x_{e}$
given a value by $\tau^{\prime}$ we get a value for the corresponding path-
variable $x_{P}$. For $\sigma$ and $\tau^{\prime}$ to be consistent we require
that no $x_{P}$ gets two conflicting values and that the values $x_{P}$ are
consistent in the sense of Definition 3.1 when considered as an assignment on
the smaller grid.

The key property that we need is that if the depth of $T$ is small enough then
at least some branch of $T$ is consistent with $\tau$ or $\sigma$. In the
former case we make sure that the total number of assigned variables under
$\tau$ and $\tau^{\prime}$ is at most half the dimension of the grid and in
the latter case that the depth is a most half the dimension of the grid after
$\sigma$. This together with the fact for each internal node of $T$ has out-
degree two and Lemma 3.2 makes sure that some branch is consistent.

Once we have identified which branches remain it is easy to see that they form
a decision tree. In fact it is also possible to define the new decision tree
by a dynamic process where we start at the root of $T$ and consider each node
in the tree. As we walk down the tree we can, for each node, check whether
both values of the current variable are consistent with the partial assignment
of the branch so far jointly with $\tau$ or $\sigma$. For a full restriction
$\sigma$ we of course take into account that once we have determined the value
on one variable on a path, all the other variables on the same path are
determined. If only one value is consistent we eliminate the other sub-tree
while if both values are consistent we have found a node in the new tree. In
some situations we might get a tree which has a single branch consistent with
$\tau$ or $\sigma$. This is considered a depth-0 tree with only one leaf. For
a decision tree $T$ we let ${T\lceil_{\tau}}$ we the decision tree after we
have applied $\tau$.

We let a 1-tree be a decision tree where all leaves are labeled 1 and define a
0-tree analogously. Special cases of such trees are trees of depth 0. We say
${T\lceil_{\pi}}=b$ if the decision tree given by ${T_{i}\lceil_{\pi}}$ is a
$b$-tree.

We say that a decision tree $\mathcal{T}$ is an $\ell$ common partial decision
tree for $T_{1},\ldots,T_{m}$ of depth $t$ if

  1. 1.

$\mathcal{T}$ is of depth $t$, and

  2. 2.

for every $T_{i}$ and branch $\pi$ in $\mathcal{T}$ there are decision trees
$T(i,\pi)$ of depth $\ell$ such that the following holds. Let
$\mathcal{T}_{i}$ be the decision tree obtained from $\mathcal{T}$ by
appending the trees $T(i,\pi)$ at the corresponding leaf $\pi$ of
$\mathcal{T}$. Then, if a branch $\pi^{\prime}$ in $\mathcal{T}_{i}$ ends in a
leaf labeled $b$, it holds that ${T_{i}\lceil_{\pi^{\prime}}}=b$.

Next we turn to a procedure of representing formulas by decision trees of
small depth.

##  6 Basics for $\bm{t}$-evaluations

The concept of $t$-evaluations was introduced by Krajíček et al. [KPW95] and
is a very convenient tool for proving lower bounds on proof size. The content
of this section is standard and we follow the presentation of Urquhart and Fu
[UF96] while using the notation of Håstad [Hås20]. We need a generalization of
previous notions essentially as introduced by Pitassi et al. [PRT22].

A tree $T$ represents $T_{1}\vee\ldots\vee T_{s}$ if for every branch $\pi$ of
$T$ ending in a leaf labeled $1$ it holds that there is an $i\in[s]$ such that
${T_{i}\lceil_{\pi}}=1$, and if $\pi$ ends in a leaf labeled $0$, then for all
$i\in[s]$ it holds that ${T_{i}\lceil_{\pi}}=0$. The set of formulas $\Gamma$
has a $t$-evaluation $\varphi$, mapping formulas from $\Gamma$ to decision
trees of depth at most $t$, if the following holds.

  1. 1.

$\varphi$ maps constants to the appropriate decision tree of depth $0$,

  2. 2.

axioms are mapped by $\varphi$ to $1$-trees,

  3. 3.

if $\varphi(F)=T$ then $\varphi(\lnot F)$ is a decision tree with the same
topology as $T$ but where the value at each leaf is negated, and

  4. 4.

if $F=\vee_{i\in[s]}F_{i}$, then $\varphi(F)$ represents
$\vee_{i\in[s]}\varphi(F_{i})$.

Each line of a proof has its own $t$-evaluation. In order to argue about the
proof we need that these different $t$-evaluations are consistent, as
explained next.

Let us first define what it means for decision trees to be consistent. Two
decision trees $T_{1},T_{2}$ are consistent if for every branch $\pi$ of
$T_{1}$ ending in a leaf labeled $b$ it holds that ${T_{2}\lceil_{\pi}}=b$ and
vice-versa. Further, $T_{1}$ and $T_{2}$ are $\lnot$-consistent, if for every
branch $\pi$ of $T_{1}$ ending in a leaf labeled $b$, it holds that
${T_{2}\lceil_{\pi}}=\lnot b$ and vice-versa.

Let us say that two formulas are isomorphic if they only differ in the order
of the or’s, and let us say that two formulas $F,G=\lnot G^{\prime}$ are
$\lnot$-isomorphic if $F$ and $G^{\prime}$ are isomorphic.

Consider a $t$-evaluation $\varphi$ defined over a set of formulas $\Gamma$
and similarly let $\varphi^{\prime}$ be a $t$-evaluation defined over the set
of formulas $\Gamma^{\prime}$. The two $t$-evaluations $\varphi$ and
$\varphi^{\prime}$ are consistent if

  1. 1.

for all isomorphic formulas $F\in\Gamma$ and $F^{\prime}\in\Gamma^{\prime}$ it
holds that $\varphi(F)$ and $\varphi^{\prime}(F^{\prime})$ are consistent, and

  2. 2.

for all $\lnot$-isomorphic formulas $F\in\Gamma$ and
$F^{\prime}\in\Gamma^{\prime}$ it holds that $\varphi(F)$ and
$\varphi^{\prime}(F^{\prime})$ are $\lnot$-consistent.

We say that a Frege proof has a $t$-evaluation if for every line $\nu$ in the
proof we have a $t$-evaluation $\varphi^{\nu}$ and for all lines
$\nu,\nu^{\prime}$ it holds that $\varphi^{\nu}$ and $\varphi^{\nu^{\prime}}$
are consistent.

Let us consider a Frege proof of depth $d$ and for a line $\nu$ in the proof
let $\Gamma^{\nu}$ be the set of subformulas occuring on line $\nu$. In the
following we construct a sequence of restrictions
$\sigma_{1},\sigma_{2},\ldots,\sigma_{d}$ such that for every line and all
formulas of depth at most $k$ we have consistent $t(k)$-evaluations if the
formulas are hit by the concatenation $\sigma_{k}^{*}$ of the first $k$
restrictions in the sequence. When considering proof size we in fact have that
all $t(k)$ are equal to the same value $t$, while in the proof when we lower
bound the number of small lines, the value $t(k)$ grows as a function of $k$.
In fact, in the latter situation, each line has a common part to all decision
trees of that line and this common part increses in size with $k$.

Getting back to $t(k)$-evaluations, put different we build by induction on $k$
for every line $\nu$ a $t(k)$-evaluation for all formulas in

$\Gamma^{\nu}_{k}=\\{{F\lceil_{\sigma_{k}^{*}}}\mid
F\in\Gamma^{\nu}\wedge\mathsf{depth}(F)\leq k\\}$

that are pairwise consistent and we look to extend these $t(k)$-evaluations to
$\Gamma^{\nu}_{k+1}$. To make sure that the domain of the $t$-evaluations does
not decrease when we apply a restriction we use the lemma below from [Hås20].
The fact that we allow consistent $t(k)$-evaluations, instead of a single
$t(k)$-evaluation for the entire proof, does not change the proof which is a
simple and fairly formal verifiction and hence omitted.

######  Lemma 6.1.

Let $\varphi$ and $\varphi^{\prime}$ be two consistent $t$-evaluations
respectively defined on the set of formulas $\Gamma$ and $\Gamma^{\prime}$,
and let $\sigma$ be a full restriction whose output is a grid of size $n$.
Then, provided that $t<n/4$, ${\varphi(F)\lceil_{\sigma}}$ and
${\varphi^{\prime}(F)\lceil_{\sigma}}$ are consistent $t$-evaluations whose
domain includes ${\Gamma\lceil_{\sigma}}$, and
${\Gamma^{\prime}\lceil_{\sigma}}$ respectively.

The important step of the argument is to use a switching lemma to extend the
domain of the $t(k)$-evaluation from $\Gamma^{\nu}_{k}$ to
$\Gamma^{\nu}_{k+1}$. We give that argument in the next section and here we
turn to formulating the punch line once we have a $t(k)$-evaluation for a
small Frege proof, where we think of $t(k)$ as small.

It turns out that under these assumptions all lines in the proof are
represented by $1$-trees. As the the constant false is represented by a
$0$-tree we can thus not derive the desired contradiction. Hence in order to
obtain the desired contradiction the Frege proof must be large, respectively
long in the case of Frege proofs of bounded line size.

In order to formalize this argument we need to fix a Frege system so we can
argue about the derivation rules. By a result of Cook and Reckhow [CR79] the
precise choice of the Frege system is not important and we choose the same
system as [PRST16, Hås20, PRT22]. This system consists of the following rules.

  * •

(Excluded middle) $(p\lor\neg p)$

  * •

(Expansion rule) $p\rightarrow(p\lor q)$

  * •

(Contraction rule) $(p\lor p)\rightarrow p$

  * •

(Association rule) $p\lor(q\lor r)\rightarrow(p\lor q)\lor r$

  * •

(Cut rule) $p\lor q,\neg p\lor r\rightarrow q\lor r$

These rules should be understood in the following manner: a depth $d$ Frege
proof can at any time, by excluded middle, write down a line of the form
$(p\lor\neg p)$ for any formula $p$ if the line is of depth at most $d$.
Similarly the expansion rule says that if we have derived the formula $p$,
then we can write down the line $(p\lor q)$ for any formula $q$ such that the
line is of depth at most $d$. The crucial lemma is as follows.

######  Lemma 6.2.

Suppose we have a derivation using the above rules starting from the Tseitin
axioms defined on the $n\times n$ grid, that also has a $t$-evaluation. Then,
if $t\leq n/8$, each line in the derivation is mapped to a 1-tree. This, in
particular, implies that we cannot derive contradiction.

The proof in the standard case of this lemma is again a tedious and formal
verification and can be found in full in [Hås20]. The proof is by induction
over the number of derivation steps and the key property is to take any path
that leads to 0 in the derived formula and find a path that leads to a 0 in
one of the assumptions. The fact that all decision trees are of depth less
than $n/8$ ensures that it is possible to find a branch of any decision tree
that is consistent with the given $0$-branch.

In the current case, where each line has its own $t$-evaluation, due to
consistency, not much is different. We can again take any $0$-branch in the
decision tree of a derived formula and find a $0$-branch in one of the
assumptions. Instead of repeating all cases let us do only the most
interesting one: the cut rule.

We have $F=(q\lor r)$ derived on line $\nu$ and suppose $\varphi^{\nu}(F)$ is
not a $1$-tree. Take a supposed leaf with label $0$ in $\varphi^{\nu}(F)$ and
let $\tau$ be the assignment leading to this leaf. We know that
${\varphi^{\nu}(q)\lceil_{\tau}}$ and ${\varphi^{\nu}(r)\lceil_{\tau}}$ are
both $0$-trees by the definition of a $t$-evaluation.

Now suppose $(p\lor q)$ was dervied on line $\nu^{\prime}<\nu$ and $(\neg
p\lor r)$ was derived on line $\nu^{\prime\prime}<\nu$. By consistency of
$\nu$ and $\nu^{\prime}$ we know that
${\varphi^{\nu^{\prime}}(q)\lceil_{\tau}}$ is a 0-tree and, as also $\nu$ and
$\nu^{\prime\prime}$ are consistent, so is
${\varphi^{\nu^{\prime\prime}}(r)\lceil_{\tau}}$.

Now, if any branch in ${\varphi^{\nu^{\prime}}(p)\lceil_{\tau}}$ ends in a
leaf labeled $0$, then ${\varphi^{\nu^{\prime}}(p\lor q)\lceil_{\tau}}$ can be
extended to reach a $0$-leaf. This is in contradiction to the inductive
assumption. For similar reasons ${\varphi^{\nu^{\prime\prime}}(\neg
p)\lceil_{\tau}}$ is a $1$-tree. This contradicts the assumed consistency of
$\nu^{\prime}$ and $\nu^{\prime\prime}$.

##  7 Proofs of the main theorems

We first reprove the main theorem of [Hås20] with improved parameters.

######  Theorem 7.1.

For $d\leq O(\frac{\log n}{\log{\log n}})$ the following holds. Any depth-$d$
Frege refutation of the Tseitin contradiction defined on the $n\times n$ grid
requires size

$\exp\bigl{(}\Omega(n^{1/(2d-1)}(\log n)^{O(1)})\bigr{)}\enspace.$

As outlined in the previous section, we construct a $t$-evaluation for all
sub-formulas occurring in a short and shallow Frege proof. By Lemma 6.2 we
then conclude that all shallow Frege proofs of the Tseitin contradiction must
be long. For the total size lower bound we in fact do not create distinct
$t$-evaluations per line but rather a single one, used on each line. Such a
$t$-evaluation is clearly consistent and hence satisfies our needs. Let
$\Gamma$ denote the set of sub-formulas occurring in the alleged proof. Our
plan is to proceed as follows for $i=0,1,2,\ldots,d$.

  * •

We have a $t$-evaluation for all formulas of $\Gamma$ that were originally of
depth $i$.

  * •

Pick a random full restriction $\sigma_{i}$ and extend the $t$-evaluation to
all formulas of $\Gamma\lceil_{\sigma_{i}}$ of original depth at most $i+1$.

At the starting point, $i=0$, each formula is a literal which is represented
by a natural decision tree of depth $1$. In order to extend the $t$-evaluation
to larger depth we use the following lemma, central to the argument.

######  Lemma 7.2 (Switching Lemma).

There is a constant $A$ such that the following holds. Suppose there is a
$t$-evaluation that includes $F_{i},1\leq i\leq m$ in its domain and let
$F=\lor_{i=1}^{m}F_{i}$. Let $\sigma$ be a random full restriction from the
space of restrictions defined in Section 4. Then the probability that
$F\lceil_{\sigma}$ cannot be represented by a decision tree of depth at most
$s\geq t$ and the number of live variables in each center is in the interval
$[.99C\log n,1.01C\log n]$ is at most

$\big{(}A(\log n)^{27}t\Delta^{-1}\big{)}^{s/108}\enspace.$

We postpone the proof of this lemma to Section 8 and see how to use it when
studying a refutation of size $N$. We start with a $t_{1}$-evaluation with
$t_{1}=1$ for single literals and apply the lemma with $s=\Omega(\log N)$ in
the first step, while we choose $t_{i}=s$ in later steps. We set
$\Delta_{i}=\Omega(t_{i}(\log n)^{27})$ and hence have that
$T_{i}=4\Delta_{i}^{2}$ for each step.

We start with the original Tseitin contradiction on the $n\times n$ grid.
Start with $n_{0}=n$ and set $n_{i+1}=n/T_{i}$ for $i=0,1,\ldots,d-1$. We are
going to choose a sequence of full restrictions $\sigma_{i}$ mapping a grid of
size $n_{i}$ to a grid of size $n_{i+1}$ randomly. Let $\sigma_{i}^{*}$ be the
composition of $\sigma_{0},\sigma_{1},\ldots,\sigma_{i}$. Let $\Gamma$ be the
set of sub-formulas that appear in an alleged proof and we let

$\Gamma_{i}=\\{F\lceil_{\sigma_{i}^{*}}\,|\,F\in\Gamma\land depth(F)\leq
i\\}\enspace.$

Let $f_{i}$ be the number of sub-formulas of depth at most $i$ in $\Gamma$.

######  Lemma 7.3.

With probability $1-f_{i}2^{-\Omega(s)}$ there is a $t$-evaluation
$\varphi_{i}$ whose domain includes $\Gamma_{i}$.

###### Proof.

This is essentially collecting the pieces. We prove the lemma by induction
over $i$. For $i=0$ we have the $t$-evaluation that maps each literal to its
natural decision tree of depth 1.

When going from depth $i$ to depth $i+1$ we need to define $\varphi_{i+1}$ on
all formulas originally of depth at most $i+1$ and consider any such $F$.

  1. 1.

Each $F$ of depth at most $i$ is, by induction, in the domain of $\varphi_{i}$
and we can appeal to Lemma 6.1.

  2. 2.

If $F$ is of depth $i$ then $\varphi_{i+1}(\neg F)$ is defined from
$\varphi_{i+1}(F)$ negating the labels at the leaves.

  3. 3.

For $F=\lor F_{i}$ where each $F_{i}$ is of at most depth $i$ we apply Lemma
7.2.

The only place where the extension might fail is under step three but, by
Lemma 7.2, the probability of failure for any individual formula is at most
$2^{-\Omega(s)}$ and as we have at most $f_{i}-f_{i-1}$ formulas of depth
exactly $i$ the induction is complete. ∎

Fixing parameters we reprove the main theorem from [Hås20] with stronger
parameters.

###### Proof of Theorem 7.1.

Suppose we have a refutation of size $N\leq\exp(c_{1}(n^{1/(2d-1)}(\log
n)^{-c_{2}}))$ for suitable positive constants $c_{1}$ and $c_{2}$. In the
first iteration we use Lemma 7.2 with $t=1$ and $\Delta=(2tA(\log
n)^{27})^{-1}$ and $s=110\log N$. In later applications we use $t=s$. It is
easy to see that with these numbers we have successful switching at each round
with high probability. The number of live centers are in the desired interval
and we are always able to construct the new $t$-evaluation.

Up to polylogarithmic factors we have that the final side length of the grid
after all the restrictions is $n(\log N)^{-2(d-1)}$ and it is a $t$-evaluation
with $t=O(\log N)$. Thus if $\log N$ is a polylogarithmic factor smaller than
$n^{1/(2d-1)}$ we get a contradiction to Lemma 6.2. ∎

Let us turn our attention to the main result of the present paper.

######  Theorem 7.4.

For any Frege proof of the Tseitin principle defined over the $n\times n$ grid
graph the following holds. If each line of the proof is of size $M$ and depth
$d$, then the number of lines in the proof is

$\exp\left(\Omega\left(\frac{n}{\big{(}(\log n)^{O(1)}\log
M\big{)}^{2d}}\right)\right)\enspace.$

The strategy of the proof is similar to the proof of Theorem 7.1: we again
build a $t$-evaluation for a supposed Frege proof. The main difference is that
instead of creating a single $t$-evaluation for the entire proof we in fact
independently create $t$-evaluations for each line. These $t$-evaluations turn
out to be consistent, as defined in Section 6, and we thus obtain the claimed
bounds.

Suppose we are given a Frege refutation of the Tseitin principle defined over
the $n\times n$ grid consisting of $N$ lines, where each line is a formula of
size $M$ and depth $d$. We denote by $\Gamma^{\nu}$ the set of sub-formulas of
line $\nu$ in the proof and continue to construct a sequence of restrictions
$\sigma_{1},\sigma_{2},\ldots,\sigma_{d}$ such that all formulas of depth at
most $k$ have consistent $t(k)$-evaluations if hit by the concatenation
$\sigma_{k}^{*}$ of the first $k$ restrictions in the sequence, where $t(k)$
is some function dependent on $k$ to be fixed later. That is, for every line
$\nu$ we have a $t(k)$-evaluation $\varphi_{k}^{\nu}$ for all formulas in the
set

$\Gamma^{\nu}_{k}=\\{{F\lceil_{\sigma_{k}^{*}}}\mid
F\in\Gamma^{\nu}\wedge\mathsf{depth}(F)\leq k\\},$

and all these $t(k)$-evaluations are consistent. In addition to these
$t(k)$-evaluations, for each line $\nu$ we also maintain a decision tree
$\mathcal{T}_{k}(\nu)$. We maintain the property that $\mathcal{T}_{k}(\nu)$
is a $t$ common partial decision tree for all $t(k)$-evaluations
$\varphi^{\nu}_{k}(\Gamma_{k}^{\nu})$ of bounded depth.

These partial common decision trees $\mathcal{T}_{k}(\nu)$ are useful to
extend the $t(k)$-evaluations $\varphi_{k}^{\nu}$ to larger depths. In each
such step, increasing $k$, we apply for each branch $\pi$ from
$\mathcal{T}_{k}(\nu)$ the following multi-switching lemma to the set of
decision trees ${\varphi^{\nu}_{k}(\Gamma_{k}^{\nu})\lceil_{\pi}}$ of depth at
most $t$. We then extend $\mathcal{T}_{k}(\nu)$ in each leaf $\pi$ by the the
partial common decision tree from the lemma to obtain $\mathcal{T}_{k+1}(\nu)$
of slightly larger depth.

######  Lemma 7.5 (Multi-switching Lemma).

There are constants $A$, $c_{1}$, and $c_{2}$ such that the following holds.
Consider formulas $F_{i}^{j}$, for $j\in[M]$ and $i\in[m_{j}]$, each
associated with a decision tree of depth at most $t$ and let
$F^{j}=\lor_{i=1}^{m_{j}}F_{i}^{j}$. Let $\sigma$ be a random full restriction
from the space of restrictions defined in Section 4. Then the probability that
the number of live variables in each center is in the interval $[.99C\log
n,1.01C\log n]$ and $(F^{j}\lceil_{\sigma})_{j=1}^{M}$ cannot be represented
by an $\ell$ common partial decision tree of depth at most $s$ is at most

$M^{s/\ell}\big{(}A(\log n)^{c_{1}}t\Delta^{-1}\big{)}^{s/c_{2}}\enspace.$

We defer the proof of this lemma to Section 9. We apply Lemma 7.5 with mostly
the same parameters so let us fix these. We choose $\ell=t=\log M$ and
$\Delta=D\cdot t\cdot(\log n)^{c_{1}}$, for a sufficiently large constant $D$.
The parameter $s$ depends on $k$ and is fixed to $s=s_{k}=2^{k-1}\log N$. With
these parameters in place we can finally also fix $t(k)=\sum_{i\leq
k}s_{i}+\log M\leq 2^{k}\log N+\log M$.

######  Lemma 7.6.

Suppose that for every line $\nu\in[N]$ we have consistent
$t(k-1)$-evaluations $\varphi^{\nu}_{k-1}$ for formulas in
$\Gamma^{\nu}_{k-1}$ along with a $t$ common partial decision tree
$\mathcal{T}_{k-1}(\nu)$ for $\varphi^{\nu}_{k-1}(\Gamma_{k-1}^{\nu})$ of
depth $\sum_{i<k}s_{i}$. Then, with probability $1-N^{-1}$, there is a full
restriction $\sigma_{k}$ whose output grid is of dimension $n$ and, assuming
that $t(k)\leq n/8$, for every line $\nu\in[N]$ there is a consistent
$t(k)$-evaluation $\varphi^{\nu}_{k}$ for formulas in $\Gamma^{\nu}_{k}$ and a
$t$ common partial decision tree $\mathcal{T}_{k}(\nu)$ for
$\varphi^{\nu}_{k}(\Gamma_{k}^{\nu})$ of depth $\sum_{i\leq k}s_{i}$.

###### Proof.

Let us first extend the common partial decision trees and then explain how to
obtain $\varphi^{\nu}_{k}$ for different lines $\nu\in[N]$.

The interesting formulas of original depth $k$ to consider are the ones with a
top $\vee$ gate. Let us fix a line $\nu\in[N]$ and consider all sub-formulas
$\\{F^{j}=\vee_{i=1}^{m_{j}}F^{j}_{i}\\}_{j=1}^{M_{\nu}}$ of line $\nu$ of
original depth $k$ with a top $\vee$ gate under the restriction
$\sigma_{k-1}^{*}$. As the original depth of every $F_{i}^{j}$ is at most
$k-1$, all these formulas are in the domain of $\varphi^{\nu}_{k-1}$. Let us
further fix a path $\pi$ in $\mathcal{T}_{k-1}(\nu)$ and recall that all
decision trees ${\varphi^{\nu}_{k-1}(F_{i}^{j})\lceil_{\pi}}$ are of depth at
most $t$.

For every $\nu\in[N]$ and branch $\pi$ of $\mathcal{T}_{k-1}(\nu)$ we apply
Lemma 7.5 to the set of formulas ${F_{i}^{j}\lceil_{\pi}}$ with associated
trees ${\varphi^{\nu}_{k-1}(F_{i}^{j})\lceil_{\pi}}$ of depth at most $t$. The
probability of failure of a single application is bounded by $N^{-2^{k}-1}$,
assuming an appropriate choice of the constant $D$. As we invoke Lemma 7.5 at
most $N\cdot 2^{\sum_{i<k}s_{i}}\leq N^{2^{k}}$ times, by a union bound, with
probability at least $1-N^{-1}$, there is a full restriction $\sigma_{k}$ such
that for every line $\nu\in[N]$ and every branch
$\pi\in\mathcal{T}_{k-1}(\nu)$ we get a $t$ common partial decision tree of
depth at most $s_{k}$ for the formulas
$({F^{j}\lceil_{\pi\sigma_{k}}})_{j=1}^{M_{\nu}}$. Let us denote this common
decision tree by $\mathcal{T}(\nu,\pi)$ and attach it to
$\mathcal{T}_{k-1}(\nu)$ at the leaf $\pi$ to obtain $\mathcal{T}_{k}(\nu)$.
The trees $\mathcal{T}_{k}(\nu)$ are of depth at most $\sum_{i\leq k}s_{k}$ as
required.

Let us explain how to define $\varphi^{\nu}_{k}$ for a fixed line $\nu\in[N]$.
Consider any formula $F$ in $\Gamma_{k}^{\nu}$.

  * •

If $F$ is of depth less than $k$, then $F$ is in the domain of
$\varphi^{\nu}_{k-1}$ and we can appeal to Lemma 6.1.

  * •

If $F$ is of depth $k-1$ then $\varphi^{\nu}_{k}(\lnot F)$ is defined from
$\varphi^{\nu}_{k}(F)$ negating the labels at the leaves.

  * •

For $F=\vee_{i}F_{i}$ of depth $k$ we use the previously constructed common
partial decision trees. We define $\varphi^{\nu}_{k}(F)$ to be the decision
tree whose first $\sum_{i\leq k}s_{i}$ levels are equivalent to
$\mathcal{T}_{k}(\nu)$ followed by $t$ levels unique to $F$ obtained from the
multi-switching lemma.

Let us check that the decision trees $\mathcal{T}_{k}(\nu)$ are indeed $t$
common partial decision trees for $\varphi^{\nu}_{k}(\Gamma_{k}^{\nu})$. By
construction this clearly holds for formulas of depth $k$ with a top $\vee$
gate. As $\mathcal{T}_{k}(\nu)$ is equivalent to $\mathcal{T}_{k-1}(\nu)$ on
the upper levels, and restrictions only decrease the depth of decision trees,
by the initial assumptions this also holds for formulas of depth less than
$k$. As the $t(k)$-evaluations of formulas of depth $k$ with a top
$\lnot$-gate are defined in terms of formulas of depth less than $k$, we also
see that $\mathcal{T}_{k}(\nu)$ is a $t$ common partial decision tree for such
formulas.

Last we need to check that each $\varphi^{\nu}_{k}$ is a $t(k)$-evaluation
plus that these are pairwise consistent.

By Lemma 6.1 all the properties hold for formulas of depth less than $k$. Let
us verify the $t(k)$-evaluation properties for formulas of depth $k$.

Property 1 is immediate, as $k>0$. As we only consider consistent decision
trees, property 2 also follows. Further, property 3 is satisfied by
construction. Property 4 can be established by checking the property for each
branch $\pi$ in $\mathcal{T}_{k-1}(\nu)$ separately; for a fixed $\pi$ we see
by Lemma 7.5 that this indeed holds.

Finally we need to establish that two $t(k)$-evaluations $\varphi^{\nu}_{k}$
and $\varphi^{\nu^{\prime}}_{k}$ are consistent for formulas of depth $k$. By
the inductive hypothesis we clearly have that $\lnot$-isomorphic formulas are
$\lnot$-consistent. Further, isomorphic formulas with a top $\lnot$ gate are
consistent. Hence we are only left with checking consistency for isomorphic
formulas of depth $k$ with a top $\lor$ gate.

Let $F=\vee_{i}F_{i}$ and $F^{\prime}=\vee_{i}F_{i}^{\prime}$ be two
isomorphic formulas from $\Gamma_{k}^{\nu}$ and $\Gamma_{k}^{\nu^{\prime}}$
respectively. For the sake of contradiction suppose
${\varphi^{\nu}_{k}(F)\lceil_{\pi}}=1$ but
${\varphi^{\nu^{\prime}}_{k}(F^{\prime})\lceil_{\pi}}=0$ for some assignment
$\pi$. In the following we use that $t(k)\leq n/8$ and hence there are
consistent branches as claimed. By property 2 we know that for some $F_{i}$ it
holds that ${\varphi^{\nu}_{k}(F_{i})\lceil_{\pi}}=1$. As $F$ and $F^{\prime}$
are isomorphic formulas we know that there is an $F^{\prime}_{j}$ such that
$F_{i}$ and $F^{\prime}_{j}$ are isomorphic formulas. As such formulas have
consistent decision trees (by induction and Lemma 6.1) we get that
${\varphi^{\nu^{\prime}}_{k}(F^{\prime}_{j})\lceil_{\pi}}=1$. But this cannot
be as by property 4 of a $t(k)$-evaluation this implies that
${\varphi^{\nu^{\prime}}_{k}(F^{\prime})\lceil_{\pi}}=1$. This establishes
that the different $t(k)$-evaluations are consistent, as required. ∎

With all pieces in place we are ready to prove Theorem 7.4.

###### Proof of Theorem 7.4.

Suppose we are give a proof of length $N=\exp(n/((\log n)^{c}\log M)^{2d})$,
for some constant $c$. We may assume that $M\leq\exp(n^{1/2d-1/2d(2d-1)})$, as
otherwise we can apply Theorem 7.1.

In order to create the consistent $t(k)$-evaluations $\varphi^{\nu}$ for each
line $\nu\in[N]$ we consecutively apply Lemma 7.6 $d$ times. We start with
$\varphi^{\nu}_{0}$ which maps constants to the appropriate depth $0$ decision
tree and literals to the corresponding depth $1$ decision trees. The partial
common decision trees $\mathcal{T}_{0}(\nu)$ are all empty.

After applying Lemma 7.6 $d$ times we are left with a $t(d)$-evaluation for
the proof. We need to ensure that $t(d)$ is upper bounded by the dimension of
the final grid: $t(d)\leq 2^{d}\log N+\log M$, while the final side length of
the grid is $n\cdot(4\Delta^{2})^{-d}=n\cdot(2D(\log n)^{c_{1}}\log M)^{-2d}$.
For our choice of $N$ and the assumption on $M$ this indeed holds and by Lemma
6.2 the theorem follows. ∎

##  8 The improved standard switching lemma

This section is dedicated to the proof of the switching lemma, restated here
for convenience.

See 7.2

The proof very much follows the proof of [Hås20]. In fact large parts of the
proof are the same. We repeat the proofs to make it possible for a reader not
familiar with the mentioned proof to follow the argument. To make the argument
slightly shorter we do not repeat all proofs of the various lemmas.

For the benefit of the reader completely on top of [Hås20] let us outline the
differences in the following section. This section can be safely skipped by
the less experienced reader.

###  8.1 Changes in the Argument

The key number that has changed is the parameter $k$, the total number of
centers that are alive. In the definition of a partial restriction this
parameter $k$ has changed from $Cs(n/T)^{2}$ to $C\log n(n/T)^{2}$. The fact
that we had $\Omega(s)$ live centers in each square was crucial in finding
live centers to extend the information sets $J_{j}$ to closed sets
$\gamma_{j}$. This process needed $O(s)$ fresh centers from specific squares
and there is nothing that prevents these from all being required to be in the
same square. In the current proof we allow $\gamma_{j}$ to be not closed and
this implies that the restriction $\rho^{*}$ is a generalized restriction
where the Tseitin condition is violated at some vertices. This only happens
when we have $\Omega(\log n)$ exposed non-chosen centers in a sub-square and
results in a single violating vertex. As the there are at most $O(s)$ exposed
centers over all we can have at most $O(s/\log n)$ violating centers. The
number of generalized restrictions with $B$ violating centers is at most a
factor $n^{2B}$ more than the the number of ordinary restrictions. This number
is $2^{O(s)}$ and this factor can be absorbed in the constant $A$ in the
statement of the switching lemma.

###  8.2 Proof Overview

Let us recall the setup. We have a full restriction $\sigma$ as defined in
Section 4 that is made up of a restriction $\rho$ and a pairing $\pi$. The
restriction $\rho$ has $(1\pm 0.01)C\log n$ many live centers in each sub-
square, for a large enough constant $C$. We have a formula
$F=\lor_{i=1}^{m}F_{i}$ and a $t$-evaluation $\varphi$ that includes each
$F_{i}$ in its domain and let $T_{i}=\varphi(F_{i})$. As $\varphi$ is a
$t$-evaluation each such tree $T_{i}$ is of depth at most $t$.

In the following we construct a decision tree $\mathcal{T}$ for
${F\lceil_{\sigma}}$ which is with high probability, over the choice of
$\rho$, of depth at most $s$. The decision tree $\mathcal{T}$ is created in a
similar manner as the canonical decision tree is usually constructed: we
proceed in stages, where in each stage the current branch $\tau$ is extended
by querying variables related to the first $1$-branch $\psi$ in the trees
${T_{1}\lceil_{\sigma\tau}},{T_{2}\lceil_{\sigma\tau}},\ldots,{T_{m}\lceil_{\sigma\tau}}$.
For now it is not so important what the related variables of $\psi$ precisely
are and we can simply think of these as the variables on the branch $\psi$.
Once all these variables have been queried, we check in each new leaf of the
tree whether we traversed the path $\psi$. If so, then we label the leaf with
a $1$ and otherwise we continue with the next stage. If there are no
$1$-branches left, we label the leaf with a $0$.

It is not so hard to see that this process indeed results in a tree
$\mathcal{T}$ that represents $\lor_{i=1}^{m}{T_{i}\lceil_{\sigma}}$: for each
leaf $\tau$ of $\mathcal{T}$ that is labeled $1$ it holds that there is an
$i\in[m]$ such that ${T_{i}\lceil_{\sigma\tau}}=1$ and if $\tau$ is labeled
$0$, then for all $i\in[m]$ we have that ${T_{i}\lceil_{\sigma\tau}}=0$, as
required. It remains to argue that $\mathcal{T}$ is with high probability of
depth at most $s$.

We analyse this event using the labeling technique of Razborov [Raz95]. The
idea of this technique is to come up with an (almost) bijection from
restrictions $\rho$ that give rise to a decision tree $\mathcal{T}$ of depth
larger than $s$ to a set of restrictions that is much smaller than the set of
all restrictions. In a bit more detail, given such a bad $\rho$, we create a
restriction $\rho^{*}$ with fewer live centers such that with a bit of extra
information we can recover $\rho$ from $\rho^{*}$. As the restriction
$\rho^{*}$ has roughly $s$ fewer live centers than $\rho$, and the inversion
requires little extra information, we obtain our statment.

Let us explain how to obtain $\rho^{*}$ from a $\rho$ that gives rise to a
decision tree $\mathcal{T}$ of depth larger than $s$. To this end, we first
need to slightly refine the construction process of $\mathcal{T}$. Namely, we
need to discuss what the related variables of a branch $\psi$ are. Instead of
thinking of this as a set of variables we rather want to think of it as an
information set $J$, as introduced in Section 4. The information set $J$ is a
minimal set that forces, along with the already collected information set on
the branch $\tau$, the branch $\psi$. Once we identified such a set $J$, we
then query all necessary variables to see whether we agree with $J$ (along
with some further variables).

Recall that we are trying to explain how to construct $\rho^{*}$ from a $\rho$
that gives rise to a decision tree $\mathcal{T}$ of large depth. Fix a long
branch $\tau$ in $\mathcal{T}$ and consider all the sets
$J_{1},J_{2},\ldots,J_{g}$ identified on $\tau$. For this proof overview, let
us assume that each $J_{j}$ is closed and the support of these information
sets are pairwise disjoint. Let us stress that this is a simplification and
does not hold in general. Assuming this holds, note that the union
$J^{*}=\cup_{i=1}^{g}J_{j}$ is also closed and recall from Section 4 that all
variables forced by $(\rho,J^{*})$ can be described by a restriction where the
centers in $\operatorname*{supp}(J^{*})$ are killed. This defines the
restricion $\rho^{*}$: it is the restriction that forces all variables forced
by $(\rho,J^{*})$. Assuming that the support of $J^{*}$ is large, we see that
$\rho^{*}$ has much fewer centers that are alive.

What remains is to argue that we can cheaply recover $\rho$ from $\rho^{*}$.
The idea is to remove the set $J_{j}$, starting with $j=1$, one-by-one from
$\rho^{*}$. To do this cheaply we use the decision trees $T_{1},\ldots,T_{m}$.
Recall that the information set $J_{1}$ determines all variables on the first
$1$-branch $\psi_{1}$. This implies in particular that $\rho^{*}$ traverses
the branch $\psi_{1}$. Hence identifying $\psi_{1}$ is for free: it is the
first $1$-branch in $T_{1},\ldots,T_{m}$ traversed by $\rho^{*}$ (assuming
that the set $J_{1}$ is pairwise disjoint from all later sets $J_{j}$). Once
we identified the branch $\psi_{1}$, we want to recover the first part of the
long branch $\tau$ so that we can repeat this argument with $J_{2}$. As
$\psi_{1}$ is of length at most $t$, using only $\log t$ bits per variable, we
indicate which variables are different on $\tau$ from $J_{1}$. This lets us
cheaply recover $\tau$ along with the centers killed by $J_{1}$. Repeating
this argument $g$ times lets us recover $\rho$.

This completes the proof overview. We allowed ourselves several
simplifications and left out a fair number of details. The most significant
simplification is the assumption that all the information sets $J_{j}$ are
closed. In the actual proof we extend each set $J_{j}$ into a closed set
$\gamma_{j}$ and then take the union of these to define $\rho^{*}$. The
process of closing a set $J_{j}$ may even fail at times and therefore
$\rho^{*}$ has to slightly bend the rules of being a restriction. It turns out
that $\rho^{*}$ is a generalized restriction as mentioned in Section 4.3. The
step of closing up the $J_{j}$ is the main source of technical difficulty in
the full proof.

The proof is split into four separate sections. In Section 8.3 we define the
extended canonical decision tree $\mathcal{T}$ and in the susequent Section
8.4 we prove some crucial properties of these decision trees. Section 8.5
explains how to extend the sets $J_{j}$ into closed information sets
$\gamma_{j}$ in order to construct the restriction $\rho^{*}$. Finally, in
Section 8.6 we show how to cheaply recover $\rho$ from $\rho^{*}$ and thereby
prove Lemma 7.2.

###  8.3 Extended Canonical Decision Trees

Let us construct an _extended canonical_ decision tree $\mathcal{T}$ for
${F\lceil_{\sigma}}$. We start with $\mathcal{T}$ the empty tree and extend it
for each branch $\tau$ separately. For every branch $\tau$ we maintain the
following objects throught the creation of $\mathcal{T}$:

  1. 1.

a set $S=S(\tau,\sigma)$ of centers, called the _exposed centers_ ,

  2. 2.

a set $I=I(\tau,\sigma)$ of information pieces as defined in Definition 4.5,
and

  3. 3.

a (state of a) matching game $\mathcal{G}=\mathcal{G}(\tau,\sigma)$, as
described in Section 3, played on the chosen centers of $\sigma$.

Initially the sets $S$ and $I$ are empty, and the matching game $\mathcal{G}$
is a new game with no vertices matched. We require that $S$, $I$ and
$\mathcal{G}$ satisfy the following invariants.

  1. 1.

No element is ever removed from $S$ or $I$. In other words, the sets $S$ and
$I$ only become larger throughout the creation of a branch $\tau$.

  2. 2.

The matched nodes in the game $\mathcal{G}$ are precisely the chosen centers
in $S$.

  3. 3.

The information set $I$ does not contain a path between a chosen center and a
non-chosen center.

  4. 4.

For non-chosen centers in $S$, the set $I$ consists of the closed information
pieces corresponding to their component in $\pi$ (both edges and non-edges).
If one center of such a connected component belongs to $S$, then so does the
entire component. Thus for non-chosen centers in $S$ we have information
pieces in all four directions.

  5. 5.

For every chosen center in $S$ we have queried all incident variables $x_{P}$
in $\tau$ and this is the information that is present as information pieces in
$I$. The one-answers are recorded in the form of a path while the zero answers
as two non-edges, one at the neighboring chosen center in the appropriate
direction which may or may not be an element of $S$. Observe that the value of
$x_{P}$ jointly with $\rho$ determines the value of all variables $x_{e}$ on
the chosen path $P$.

Let us stress the fact that information about $\pi$ comes from the restriction
$\sigma$ and hence in Item 4 we do not query a variable in $\mathcal{T}$.
However, querying a variable $x_{P}$, as done in Item 5, causes a query in the
decision tree $\mathcal{T}$.

Further, observe that there is a crucial difference between Item 4 and Item 5:
on the non-chosen centers we have information pieces in $I$ only on the
centers in $S$. In contrast $I$ may contain information pieces from chosen
centers that are not in $S$.

Let us discuss the creation of $\mathcal{T}$. We proceed in stages. In each
stage we fix a branch $\tau$ in $\mathcal{T}$. We go over the decision trees
$T_{i}=\varphi(F_{i})$ one by one. Suppose we consider $T_{i}$. Take the first
(in some fixed order) branch $\psi$ in $T_{i}$ that leads to a leaf labeled
$1$ which is consistent with $\tau$ and $\sigma$. If there is no such branch,
then we continue with $T_{i+1}$ and if there is no such branch $\psi$ for any
$T_{i}$, then we label the $\tau$ leaf of $\mathcal{T}$ by $0$ and continue
with a different branch $\tau^{\prime}$ of $\mathcal{T}$ until all leaves of
$\mathcal{T}$ are labelled. But for now let us assume that there is a branch
$\psi$ as described.

For the variables appearing on $\psi$ we have unique values required to reach
this leaf. We let a _possible forcing information_ $J$ be an information set
that jointly with $I$ and $\rho$ forces444Recall from Definition 4.6 that a
variable is forced if we have the relevant information at its closest
endpoint. all variables on $\psi$ to take these unique values. Let us call
$\psi$ the _forceable branch_. The intuition is that if the information set
$J$ agrees with the actual input, then indeed $\psi$ is followed and we can
safely end with a $1$-leaf. In most cases, however, the actual input does not
agree with $J$ and we need to continue evaluating the extended canonical
decision tree $\mathcal{T}$. We require the following properties of $J$.

  1. 1.

If $J$ contains a non-edge from a chosen center it also contains a non-edge in
the “reverse direction”. As an example if it contains a non-edge going left
from a chosen center $v$ then it contains a non-edge going right from the
chosen center in the sub-square to the left of $v$.

  2. 2.

The information set $J$ does not contain a path between a chosen center and a
non-chosen center.

  3. 3.

The information sets $I$ and $J$ are consistent and disjoint.

  4. 4.

The part of $J$ on the non-chosen centers is closed and consistent with $\pi$,
that is, $J$ contains a subset of the components of $\pi$ in the form of a
closed set of information pieces.

  5. 5.

$J$ is minimal given the above properties and the fact that, along with $I$,
it should determine the values of all the variables on the forceable branch
$\psi$.

Note that a set $J$ may not be unique for a given path $\psi$. If there are
several sets as described above, choose one in a fixed but otherwise
aribitrary manner. While the choice is not essential for what follows, we do
need to establish that whenever some $T_{i}$ can still reach a 1-leaf, then
there is a possible forcing information $J$. We postpone this to the following
section (see Lemma 8.1) and for now assume that such a set $J$ exists whenver
we have a branch $\psi$ as described.

Denote by $U$ the set of closest endpoints of variables on $\psi$ that are
chosen centers but not contained in $S$. A somewhat subtle point to note is
that $U$ may contain a closest endpoint of a variable that is determined by
$I$: the set $I$ may contain information pieces about chosen centers outside
the set of exposed centers $S$. The set $U$ is needed to ensure that we treat
such centers correctly.

Let us continue the construction of the extended canonical decision tree
$\mathcal{T}$ at $\tau$. Add $U$ and all centers in $\operatorname*{supp}(J)$
to $S$ along with the centers described next. Let the adversary in the game
$\mathcal{G}$ supply $U$ along with all chosen centers in
$\operatorname*{supp}(J)$. We apply Lemma 3.5 and add all nodes provided by
$P_{M}$ to $S$ (we tacitly assume throughout that $|S|\leq n/2$). Observe that
this game is played on nodes of the grid and does not take into account any
other information from $I$ or $J$.

Finally we need to update $I$ and extend $\mathcal{T}$. This is
straightforward for the non-chosen centers added to $S$: for every such non-
chosen center $v$ we add the information from $v$’s connected component in
$\pi$ to $I$ (in the form of edges and non-edges).

For every chosen center added to $S$ we query all the incident variables,
thereby extending $\mathcal{T}$. For every newly created consistent extension
$\tau^{\prime}$ of $\tau$ we need to update the set $I$. Record one-answers as
an edge and zero-answers as two non-edges including the other endpoint of a
potential chosen path, i.e., the chosen center in the adjacent sub-square in
the given direction. Recall that we only consider consistent branches
$\tau^{\prime}$ (as assignments) and hence we create consistent information
sets.

Finally, for every consistent $\tau^{\prime}$ extending $\tau$, we check
whether the information set $I(\tau^{\prime},\sigma)$ traversed the forceable
branch $\psi$ of $T_{i}$. This can clearly be done: all variables on $\psi$
have their closest endpoint in $S$ and each exposed center has information
pieces in all four directions. If $\psi$ is indeed followed, we label the leaf
$\tau^{\prime}$ with a $1$. Otherwise, if the forceable branch is not
followed, then we proceed with the next stage.

This completes the description of the creation of the extended canonical
decision tree $\mathcal{T}$ for ${F\lceil_{\sigma}}$. It is straightforward to
check that the invariants hold after every completed stage.

###  8.4 Some Properties of Extended Canonical Decision Trees

In this section we prove two important properties of extended canoncial
decision trees, along with some auxilary lemmas. The first important property
is that the decision tree $\mathcal{T}$ does indeed represent
$\lor_{i=1}^{m}{T_{i}\lceil_{\sigma}}$. Secondly, we show that the
construction process of $\mathcal{T}$ is independent of the choice of the
negations of the preferred values along the paths between chosen centers. This
allows us to focus on long branches that have well-behaved information sets
$I$.

Before proving these two statements, recall that we postponed the proof of the
claim that if it is possible to each a 1-leaf of $T_{i}$, then there is a
possible forcing information $J$. Let us establish this fact. Observe that at
any point when forming the extended canonical decision tree, the information
$I$ comes from information in $\pi$ and from queries already done in the
decision tree $\mathcal{T}$ with answers $\tau$. Remember that $\sigma$
includes all the information from $\pi$.

######  Lemma 8.1.

If there is a $1$-branch $\psi$ in ${T_{i}\lceil_{\sigma}}$ that is consistent
with $\tau$, then there is a possible forcing information $J$ for $\psi$.

###### Proof.

Let $\psi^{\prime}$ be the branch in $T_{i}$ that gives rise to $\psi$.
Consider the assignment $\tau^{\prime}$ to the path variables $x_{P}$ such
that the $1$-leaf of ${T_{i}\lceil_{\sigma}}$ is reached. Let us find a
possible $J$ such that $\psi^{\prime}$ is followed.

The information pieces next to chosen centers are simply those given by
$\tau^{\prime}$. These are, by definition, consistent with $\tau$ and can
hence be included in $J$.

The information pieces next to non-chosen centers are the relevant information
pieces from $\pi$. As all information pieces from $\pi$ are consistent,
consistency is automatically satisfied for these pieces.

Dropping any non-required piece and all the pieces already in $I$ makes $J$
disjoint from $I$ and minimal. Clearly $J$ forces $\psi^{\prime}$ to be
followed. This completes the proof of the lemma. ∎

As an immediate corollary we have that the decision tree $\mathcal{T}$ is
indeed a legitimate choice for $\varphi({F\lceil_{\sigma}})$.

######  Corollary 8.2.

The extended canonical decision tree $\mathcal{T}$ represents
$\vee_{i=1}^{m}{T_{i}\lceil_{\sigma}}$.

The creation of the extended canononical decision tree depends on $\rho$ and
$\pi$ but not, in a serious way, on the negations of the preferred values
along the paths between the chosen centers. The following lemma makes this
intuition precise.

######  Lemma 8.3.

Let $\sigma_{1}$ be obtained from $\rho_{1}$ and $\pi$ and $\sigma_{2}$ from
$\rho_{2}$ and $\pi$ where $\rho_{1}$ and $\rho_{2}$ pick the same set of
centers and fixed values. Assume furthermore that the only difference between
$\rho_{1}$ and $\rho_{2}$ is that for each chosen path $P$ there is a bit
$c_{P}$ such that for each grid-edge $e$ on $P$ the preferred values of
$x_{e}$ differ by $c_{P}$ in $\rho_{1}$ and $\rho_{2}$. Then the only
difference between the extended canonical decision trees of
$F\lceil_{\sigma_{1}}$ and $F\lceil_{\sigma_{2}}$ is the labeling of the
internal edges.

###### Proof.

This follows by inspection of the procedure for forming the extended canonical
decision tree. The only difference is that variables on chosen paths in one
case are forced by a path and in the other case by two non-edges. This does
not cause any difference in the construction of $\mathcal{T}$ as the supports
of the two corresponding sets $J_{1}$ and $J_{2}$ are identical by Item 1 of a
possible forcing information. ∎

This lemma is crucial in our analysis. It allows us to focus on long branches
whose information set $I$ is well-behaved in the following sense.

######  Definition 8.4 (Closed branch).

Let $\mathcal{T}$ be an extended canonical decision tree. A branch $\tau$ in
$\mathcal{T}$ is _closed_ if the information set $I(\tau,\sigma)$ contains a
path between two chosen centers $u,v$ if and only if the matching game
$\mathcal{G}(\tau,\sigma)$ matched $u$ to $v$.

This slightly overloads the notion “closed” but as the information pieces
given by the answers on a closed branch $\tau$ is (essentially) a closed
information set we hope that this causes no confusion. The following lemma is
an immediate consequence of Lemma 8.3.

######  Lemma 8.5.

If the probability that $F\lceil_{\sigma}$ needs a decision tree of depth $s$
is at least $q$, then the probability that the extended canonical decision
tree of $F\lceil_{\sigma}$ contains a closed branch of length at least $s$ is
at least $2^{-s}q$.

This lemma allows us to only analyze closed branches. The main advantage of
considering closed branches is that the information sets $I$ have a nice
structure. We use the following property throught the proof.

######  Lemma 8.6.

On a closed branch, after the completion of a stage, $I$ consists of a closed
part on the exposed vertices $S$ jointly with a set of non-edges from chosen
centers not in $S$ towards chosen centers in $S$.

###### Proof.

The information in $I$ about non-chosen centers in $S$ is from $\pi$ and thus
by definition closed. Further, because we are on a closed branch, the set $I$
is also closed on the chosen centers in $S$. The only other information pieces
in $I$ are non-edges from chosen centers not in $S$ towards chosen centers in
$S$. ∎

Lastly we have an auxillary lemma regarding the size of the set of exposed
centers $S$.

######  Lemma 8.7.

In each stage at most $8t$ vertices are added to the set of exposed vertices
$S$.

###### Proof.

A forceable branch $\psi$ is of length at most $t$ as the trees $T_{i}$ are of
depth at most $t$. For each variable $x_{e}$ on $\psi$ there are at most $2$
chosen centers in $\operatorname*{supp}(J)\cup U$ if the closest endpoint of
$x_{e}$ is chosen and at most $4$ non-chosen centers if the closest endpoint
is non-chosen.

When adding $\operatorname*{supp}(J)\cup U$ to $S$ we add at most $1$ extra
center per chosen center in $\operatorname*{supp}(J)\cup U$ to $S$. We
conclude that at most $8t$ vertices are added to $S$ in a given stage. ∎

###  8.5 From $\bm{\rho}$ to $\bm{\rho^{*}}$

We want to bound the number of restrictions $\rho$ (as defined in Section 4)
that give rise to an extended canonical decision tree $\mathcal{T}$ of depth
at least $s$. In light of Lemma 8.5 we can focus on $\mathcal{T}$ that contain
a _closed_ branch $\tau$ of length at least $s$. Let us fix such a $\rho$
along with the extended canonical decision tree $\mathcal{T}$ and the closed
branch $\tau$ of length at least $s$.

The goal of this section is to construct a restriction $\rho^{*}$ that is
related to $\rho$ but has fewer live variables. In the following section we
then show how to recover $\rho$ from $\rho^{*}$ with a bit of extra
information. As $\rho^{*}$ has fewer live variables there are fewer such
restrictions and, assuming we require only little extra information to recover
$\rho$, we thus establish that there are very few $\rho$ that cause the
extended canonical decision trees to be of depth at least $s$.

Recall that an information set $\gamma^{*}$ is closed if for every center $v$
in $\operatorname*{supp}(\gamma^{*})$ the set $\gamma^{*}$ contains
information in all four directions of $v$ and, furthermore, $\gamma^{*}$ has
an odd number of edges incident to every such $v$. The idea is to reduce the
number of live variables with the help of a closed information set
$\gamma^{*}$. Consider all variables forced by $(\rho,\gamma^{*})$. Observe
that $(\rho,\gamma^{*})$ can be described by a restriction $\rho^{*}$ where
all the centers in $\operatorname*{supp}(\gamma^{*})$ are killed: negate the
values of any preferred variable on any path in $\gamma^{*}$. In the following
we are going to construct a closed information set $\gamma^{*}$ with large
support (linear in $s$) such that $\rho$ can be recovered from the resulting
$\rho^{*}$ with a bit of extra information.

As suggested in the proof outline, we would like to choose $\gamma^{*}$ to be
the union of all the possible forcing information sets used when creating the
long branch $\tau$. Unfortunately this does not work: a possible forcing
information is not always closed and insisting on a possible forcing
information to be closed creates a dependence between $\mathcal{T}$ and the
negations of the preferred values along paths between chosen centers. As such
it becomes difficult to prove the crucial Lemma 8.5.

So it is not obvious how to guarantee that the possible forcing information is
closed. What we can do, however, is to close these information sets _after_ we
have found a long closed branch $\tau$. We can then take $\gamma^{*}$ to be
the union of these newly closed possible forcing information sets. Let us
proceed by explaining how to close the possible forcing information sets.

As $\tau$ is a branch of length $s$, there is a first stage $g$ such that at
the end of stage $g$ at least $s/4$ centers are exposed: only variables
incident to exposed centers are queried and each exposed center causes at most
$4$ queries on the branch $\tau$. Put different, if we let
$\tau_{g}\subseteq\tau$ be the closed path constructed by the end of stage
$g$, then the set of exposed centers $S^{*}_{g}=S(\tau_{g},\sigma)$ is for the
first time of size at least $s/4$. We analyze the event of ever reaching such
a stage $g$.

Note that $|S^{*}_{g}|<s/4+8t$ by Lemma 8.7 and $g\leq s/4$ as in each stage
at least one center is added to the exposed centers $S$. For $j\in[g]$ we let
the forceable branch of stage $j$ in the decision tree $T_{i_{j}}$ be denoted
by $\psi_{j}$, let $J_{j}$ be the corresponding possible forcing information
and $\tau_{j}\subseteq\tau_{g}$ be the branch in $\mathcal{T}$ created by the
end of stage $j$. Denote the information set added at stage $j$ by $I_{j}$ and
let $I_{j}^{*}=I^{*}(\tau_{j},\sigma)$, or equivalently
$I_{j}^{*}=\cup_{i=1}^{j}I_{i}$, be the information set gathered during the
first $j$ stages. In the following we explain how to extend the information
sets $J_{j}$ into (usually) closed sets $\gamma_{j}$. Sometimes this extension
may fail to produce a closed set $\gamma_{j}$ but this happens rarely and
hence enough centers are killed in $\rho^{*}$ to finish the argument.

Consider the sets $J_{1},\ldots,J_{g}$ in order. Initially we set
$\gamma_{j}=J_{j}$ and extend it as follows. Recall that when we create the
extended canonical decision tree $\mathcal{T}$, in stage $j$, we add a set
$U_{j}$ of chosen centers to $S^{*}_{j-1}=S(\tau_{j-1},\sigma)$ that are
closest endpoints of variables on $\psi_{j}$. Add all information pieces in
$I^{*}_{j-1}$ incident to a chosen center in $U_{j}$ to $\gamma_{j}$. Note
that because $\tau_{g}$ is a closed branch and $U_{j}$ is disjoint from
$S^{*}_{j-1}$, by Lemma 8.6, all these added information pieces are non-edges
towards chosen centers in $S^{*}_{j-1}$.

We need to close the set $\gamma_{j}$. Let us consider each center
$v\in\operatorname*{supp}(\gamma_{j})$ separately. We want to close
$\gamma_{j}$ at $v$, meaning that (1) there are information pieces in all
directions next to $v$ and (2) an odd number of these edges are present. Note
that the non-chosen part in $\gamma_{j}$ is already closed as this part is
closed in $J_{j}$. Hence we only need to add information pieces next to chosen
centers and we thus focus on the case when $v$ is a chosen center. We claim
that if $v$ has information pieces in all four directions in $\gamma_{j}$,
then $\gamma_{j}$ is closed at $v$: since $I^{*}_{j-1}$ and $J_{j}$ are
consistent (by Item 3) there is an odd number of edges next to $v$.

Otherwise, if $v$ has no information piece in some direction(s), add a non-
edge in all but one such direction to $\gamma_{j}$. In case $v$ already has an
odd number of edges next to $v$, add another non-edge in the final direction.
Else we need to add an edge to an appropriately selected center in the
suitable sub-square $R$. At this point we slightly bend the rules and allow to
connect the chosen center $v$ to a non-chosen center in $R$.

Namely, we add an edge from $v$ to a so-called _fresh center_ in $R$, unless
there are no fresh centers available. A fresh center is a non-chosen but alive
center that is not a member of $S^{*}_{g}$ and is not an element of any of the
sets
$\operatorname*{supp}(\gamma_{1}),\ldots,\operatorname*{supp}(\gamma_{j-1})$.
If we add a fresh center we also add non-edges from the fresh center in the
other three directions, ensuring that $\gamma_{j}$ is closed. Let us emphasize
that we choose which fresh centers to add to $\gamma_{j}$ _after_ the long
branch $\tau_{g}$ has been constructed. This allows us to ensure that these
centers do _not_ appear in $S^{*}_{g}$.

If there is no such fresh center available in $R$, then we do not add anything
and let $\gamma_{j}$ have a center of even degree. Let us call these centers
_bad_. This completes the description of the construction of the sets
$\gamma_{1},\ldots,\gamma_{g}$.

In the following we want to argue that the union of the different $\gamma_{j}$
is closed if we disregard the bad centers. We establish this by arguing that
the $\gamma_{j}$ have pairwise disjoint supports.

######  Lemma 8.8.

For $j\neq j^{\prime}$ it holds that
$\operatorname*{supp}(\gamma_{j})\cap\operatorname*{supp}(\gamma_{j^{\prime}})=\emptyset$.

###### Proof.

Let us assume that $j^{\prime}<j$. By definition (Item 3) $J_{j}$ and
$I^{*}_{j-1}$ are disjoint but their supports may intersect. As $I^{*}_{j-1}$
contains information pieces in all directions of every center in $S^{*}_{j-1}$
(Items 4 and 5), the supports of $J_{j}$ and $I^{*}_{j-1}$ can only intersect
in centers that are not in $S^{*}_{j-1}$. Because the support of
$J_{j^{\prime}}$ was added to the set of exposed centers at the end of stage
$j^{\prime}$ we have that $\operatorname*{supp}(J_{j^{\prime}})\subseteq
S^{*}_{j-1}$. This implies that $\operatorname*{supp}(J_{j^{\prime}})$ does
not intersect $\operatorname*{supp}(J_{j})\cup U_{j}$ as $U_{j}$ is disjoint
from $S^{*}_{j-1}$ by definition.

Further, because $U_{j^{\prime}}$ is a subset of $S^{*}_{j-1}$ and
$\operatorname*{supp}(J_{j})\cup U_{j}$ is disjoint from $S^{*}_{j-1}$, we
have that $U_{j^{\prime}}$ and $\operatorname*{supp}(J_{j})\cup U_{j}$ are
disjoint. As the support of $\gamma_{j}$ consist of the support of $J_{j}$
along with $U_{j}$ and the added fresh centers, we conclude that the support
of $\gamma_{j}$ and the support of $\gamma_{j^{\prime}}$ are disjoint. ∎

The bad centers are the reason that $\rho^{*}$ is a generalized restriction as
defined in Section 4.3. Before formally defining $\rho^{*}$ let us bound the
number of bad centers in the information sets $\gamma_{1},\ldots,\gamma_{g}$.

######  Lemma 8.9.

The number of bad centers in the information sets
$\gamma_{1},\ldots,\gamma_{g}$ is at most $O(s/\log n)$.

###### Proof.

Only chosen centers can become bad. For a chosen center in $\gamma_{j}$ to
become bad, each non-chosen center in a neighboring square either occurs in
$S^{*}_{g}$ or in one of the supports of $\gamma_{i}$, for $i<j$.

We claim that $\sum_{j\leq
g}|\operatorname*{supp}(\gamma_{j})|=O(|S^{*}_{g}|)$. This is readily
verified: when defining $\gamma_{j}$ we start out with the support being
$\operatorname*{supp}(J_{j})\cup U_{j}$ and then enlarge it by at most a
single center per element in the support. Lemma 8.8 implies in particular that

$\displaystyle\sum_{j\leq g}\big{|}\operatorname*{supp}(J_{j})\cup
U_{j}\big{|}=\Big{|}\bigcup_{j\leq g}\operatorname*{supp}(J_{j})\cup
U_{j}\Big{|}\leq|S^{*}_{g}|\enspace,$ (1)

and thus the claim follows.

By definition of $g$ and Lemma 8.7 we have that $|S^{*}_{g}|<s/4+8t$. Further,
by assumption it holds that $t\leq s$ and thus $|S^{*}_{g}|+\sum_{j\leq
g}|\operatorname*{supp}(\gamma_{j})|=O(s)$. Finally, every square contains
$\Omega(\log n)$ non-chosen centers and hence there are at most $O(s/\log n)$
many bad centers. ∎

As mentioned before, closed graphs can be used to define restrictions with
fewer live centers. Let $B$ denote the number of bad centers in the support of
the different $\gamma_{j}$ and let $\gamma^{*}=\cup_{j=1}^{g}\gamma_{j}$. As
each $\gamma_{j}$ is closed (except at the bad centers) and, by Lemma 8.8,
they have pairwise disjoint supports we conclude that $\gamma^{*}$ has at most
$B$ bad centers. We define $\rho^{*}$ to be the restriction defined by $\rho$
composed with the information $\gamma^{*}$. As previously explained, the bad
centers cause $\rho^{*}$ to be a generalized restriction where all centers in
$\operatorname*{supp}(\gamma^{*})$ are now dead. We call these the
_disappearing_ centers. By Lemma 8.9 we have at most $B\leq O(s/\log n)$ bad
centers, while at least $|S^{*}_{g}|\geq s/4$ centers disappear.

###  8.6 Encoding $\bm{\rho}$

We first need to introduce some more notation. Recall that $U_{j}$ is the set
of closest endpoints of variables on the $j$th forceable branch $\psi_{j}$
that are chosen centers but not contained in $S^{*}_{j-1}$. We let $a_{j}$ be
the number of closest endpoints of variables on $\psi_{j}$ that are also in
$\operatorname*{supp}(J_{j})\cup U_{j}$ and let $b_{j}$ be the number of
additional centers in $\gamma_{j}$, i.e.,
$b_{j}=|\operatorname*{supp}(\gamma_{j})|-a_{j}$. We let
$a=\sum_{j=1}^{g}a_{j}$, define $b$ similarly and let
$c=\big{|}\operatorname*{supp}(I^{*}_{g})\setminus\operatorname*{supp}(\gamma^{*})\big{|}$
be the number of centers in the support of $I^{*}_{g}$ that do not appear in
the support of $\gamma^{*}$. The main goal of this section is to prove the
following lemma stating that a restriction $\rho$ that causes the extended
canonical decision tree to have a closed path of length at least $s$ can be
encoded using few bits, given $\rho^{*}$ and $T_{1},\ldots,T_{m}$. Put
different, the mapping from $\rho$ to $\rho^{*}$ can be inverted with a bit of
extra information. Recall that $\Delta$ is the number of centers in each sub-
square.

######  Lemma 8.10.

Suppose we are given $\rho^{*}$ as well as the decision trees
$T_{1},\ldots,T_{m}$ each of depth at most $t$. Then

$\displaystyle a\log t+b\log\Delta+c\log\log n+O(a+b+c)$

many bits are needed to encode $\rho$.

Before diving into the proof of this lemma let us show how the switching lemma
follows from Lemma 8.10. For the proof of the switching lemma we need one
further lemma that relates the parameters $a,b$ and $c$: it is not so hard to
convince oneself that $b+c$ is of order $O(a)$. Indeed, it was shown by Håstad
[Hås20] that $b+c$ is bounded by $25a$.

######  Lemma 8.11 ([Hås20]).

It holds that $b+c\leq 25a$.

###### Proof of Lemma 7.2.

Let us analyze the probability that a random $\rho$ gives rise to a closed
branch of length at least $s$. Let $m=\Delta(n/T)^{2}$ be the total number of
centers and recall that $k=C\log n(n/T)^{2}$ is the total number of live
centers.

Let us first count the number of restrictions $\rho$ that give rise to a
closed branch of length at least $s$. By Lemma 8.10 this is upper bounded by
the number of ways to choose $\rho^{*}$ times $t^{a}\Delta^{b}(\log
n)^{c}A^{a+b+c}$, for some absolute constant $A$. The number of ways to choose
$\rho^{*}$ is555We sum the binomial coefficient over possible values of $a+b$
but this sequence is exponentially increasing and thus dominated by twice the
maximal term. at most $2^{1+r_{n}}{m\choose k-(b+a)}n^{2B}$, where $2^{r_{n}}$
is the number of possibilities for the choice of the fixed and preferred
variables once the choice of centers is fixed, and $B$ is the number of bad
centers.

In order to bound the probability that a restriction gives rise to a closed
branch of length at least $s$ we also need to count the number of restrictions
$\rho$. We can count these restrictions in a similar manner as we counted the
restrictions $\rho^{*}$: there are $2^{r_{n}}{m\choose k}$ many such
restrictions. Thus the probability of having a closed branch of length at
least $s$ is bounded by

$\displaystyle\frac{t^{a}\Delta^{b}(\log
n)^{c}A^{a+b+c}2^{1+r_{n}}\binom{m}{k-(a+b)}n^{2B}}{2^{r_{n}}\binom{m}{k}}\enspace.$
(2)

The quotient of the the binomial coefficients can be bounded by

$\displaystyle\prod_{i=0}^{a+b-1}\frac{k-i}{m+i-k}\leq\left(\frac{k}{m-k}\right)^{a+b}=\left(\frac{C\log
n}{\Delta-C\log n}\right)^{a+b}\leq\Delta^{-(a+b)}(\log
n)^{a+b}A^{a+b}\enspace,$ (3)

for some different constant $A$. We conclude that the probability of a closed
branch of length at least $s$ appearing in the extended canonical decision
tree is at most

$\displaystyle\Delta^{-a}(\log n)^{a+b+c}t^{a}A^{a+b+c}n^{2B}\enspace,$ (4)

for a new constant $A$. Applying Lemma 8.11 and modifying $A$ again we can
bound this by

$\displaystyle\Delta^{-a}(\log n)^{26a}t^{a}A^{a}=(A(\log
n)^{26}t\Delta^{-1})^{a}n^{2B}\enspace.$ (5)

Finally, as the number of exposed centers is at most $a+b+c$ and the number of
queried variables is at most four times the number of exposed centers we have
$a+b+c\geq s/4$ and hence $a\geq s/104$ by Lemma 8.11. By Lemma 8.9 we have
that $n^{2B}\leq 2^{O(s)}$ and we can thus incorporate this factor into the
constant $A$. This concludes the analysis of the probability of the event that
a closed branch of length at least $s$ appears in the extended canonical
decision tree. Lemma 7.2 now follows from Lemma 8.5 and a final modification
of the constant $A$. ∎

The rest of this section is dedicated to the proof of Lemma 8.10. On a very
high level, we want to remove $\gamma^{*}$ from $\rho^{*}$. We do this in
stages, where in each stage we remove a single $\gamma_{j}$ from $\rho^{*}$ by
utilizing the decision trees $T_{1},\ldots,T_{m}$ and reading a bit of extra
information. Let us introduce some notation and note a simple observation in
order to give a bit more detailed proof outline. For convenience let
$I_{0}^{*}=\emptyset$, let $\gamma_{\geq j}^{*}=\cup_{i=j}^{g}\gamma_{i}$, and
let $\rho_{\geq j}^{*}$ be the restriction obtained from composing $\rho$ with
the information $\gamma_{\geq j}^{*}$, i.e., $\rho^{*}_{\geq j}$ forces the
same variables as $(\rho,\gamma_{\geq j}^{*})$ forces.

Recall that the possible forcing information $J_{j}$ along with $I^{*}_{j-1}$
determines all variables on the forceable branch $\psi_{j}$ of stage $j$. As
$\gamma_{j}$ extends $J_{j}$ we observe that
$(\rho,I_{j-1}^{*}\cup\gamma_{j})$ traverses $\psi_{j}$. Further, as
$\gamma_{\geq j}^{*}$ extends $\gamma_{j}$ and is consistent with
$I_{j-1}^{*}$, it also holds that $(\rho,I_{j-1}^{*}\cup\gamma_{\geq j}^{*})$,
or equivalently $(\rho^{*}_{\geq j},I_{j-1}^{*})$, traverses $\psi_{j}$. This
observation allows us to pursue the following high level plan.

We proceed in stages $j=1,\ldots,g$. At the beginning of each stage $j$ we
assume that we know the restriction $(\rho^{*}_{\geq j},I_{j-1}^{*})$. Note
that because $I_{0}^{*}=\emptyset$ and $\rho_{\geq 1}^{*}=\rho^{*}$, we have
that $(\rho_{\geq 1}^{*},I_{0}^{*})$ forces the same variables as $\rho^{*}$
and we hence have the necessary information to start at stage $j=1$. By above
observation the restriction $(\rho^{*}_{\geq j},I_{j-1}^{*})$ traverses the
forceable branch $\psi_{j}$. Let us assume for now that $\psi_{j}$ is the
first $1$-branch traversed, which allows us to identify $\psi_{j}$ for free.
This branch can in turn be used to identify a good fraction of $\gamma_{j}$:
as $\psi_{j}$ is of length at most $t$ we only need to spend $\log t$ bits per
variable on $\psi_{j}$ forced by $J_{j}$ to identify the corresponding closest
center that disappeared. To find the remaining elements of $\gamma_{j}$, along
with its graph structure, we use some additional external information. This
lets us “remove” $\gamma_{j}$ from $\rho_{\geq j}^{*}$ to obtain $\rho_{\geq
j+1}^{*}$. Before we can proceed with stage $j+1$ we also need to recover
$I_{j}$. As a good fraction of the support of $I_{j}$ is already identified by
$\gamma_{j}$ we can again use some external information to obtain the final
missing pieces.

Unfortunately there are some complications. Recall that when we closed up the
information sets $\gamma_{j}$ we potentially added information pieces to
$\gamma_{j}$ that correspond to paths between chosen and non-chosen centers.
Such information pieces are _not_ allowed in a potential forcing information
$J_{j}$. So it may well be that the first $1$-branch traversed by