Earlier results and methods.

Sieben attributes the introduction of polyomino achievement games to Frank Harary (Sieben 2004, sec. 1). His account records handicap-two strategies of Harary, Harborth and Seemann and the nonexistence of a pairing defense for Snaky, and proves victory in \(41\) dimensions (Sieben 2004, sec. 4 and Proposition 4.1). Csernenszky, Martin and Pluhár later gave a computer-free proof of the nonexistence of a pairing defense (Csernenszky et al. 2011, Theorem 10). This rules out a class of Breaker strategies, but does not by itself give Maker a winning strategy.

Halupczok and Schlage-Puchta proved that Snaky wins in three dimensions, loses on an \(8\times8\) board, and has planar handicap number at most one (Halupczok and Schlage-Puchta 2007, Theorem 1). A handicap of one allows Maker two stones on the opening turn, before Breaker’s first reply. Ito and Miyagawa also presented a handicap-one construction (Ito and Miyagawa 2007). Sieben subsequently gave a finite proof sequence for that handicap and described the ordinary planar problem as undecided at the time (Sieben 2008, sec. 1 and Appendix B).

Theorem 1 treats the empty planar board without a handicap. We give three complete constructions, with bounds of \(21\), \(25\), and \(35\) Maker moves. They share a composition rule but retain different information and different openings. The \(21\)-move certificate ends directly with no required Maker stones. The \(25\)-move construction removes already-owned cells from each Breaker-free region and uses required cells as placement anchors. The \(35\)-move construction supplies four explicit conditional statements at arbitrary positions and an opening that reaches one of them. We keep these methods explicit because their content is not determined by the empty-board move bounds alone.

Our method belongs to the proof-tree approach to weak achievement studied by Sieben (Sieben 2008, secs. 2–3). His finite situations and territory-intersection conditions encode ways of combining continuations at Breaker’s turn. Our conditional positions are stated at Maker’s turn, with a separate Breaker-turn consequence for openings in which the pivot is already owned. The formulation explicitly keeps track of arbitrary previous Maker and Breaker ownership and counts actual future Maker moves. We prove its soundness in Section 2. The perpendicular attacks discussed by Halupczok and Schlage-Puchta (Halupczok and Schlage-Puchta 2007, sec. 3) also illuminate why a line of four Maker stones can exert substantial pressure. Section 5 gives a separate, fully stated local result of this kind.

Shaik, Mayer-Eichberger, van de Pol and Saffidine studied bounded-depth QBF encodings of finite Maker–Breaker games, including Snaky on a \(5\times5\) board (Shaik et al. 2023, sec. 2.1 and 6). Boucher and Villemaire study QBF encodings for finite strong achievement games on ordinary and toroidal boards (Boucher and Villemaire 2025, secs. 2.2, 3.3–3.4, and 4). Here the finite object is a proof of sufficient conditions for the infinite weak game. Breaker is free to play outside every displayed region, and the proof covers those replies without a board cutoff.

Proof overview.

A conditional winning position is described by three finite data: a set \(A\) that Maker must own, a set \(T\) that must contain no Breaker cell, and a bound \(h\) on further Maker moves. Starting with the six immediate completions of \(S\), we combine such conditions as follows. Maker claims a chosen cell. The required cells of every child condition then belong to Maker; moreover, the intersection of the child envelopes belongs to Maker. Consequently one new Breaker cell cannot lie in every child envelope, and at least one continuation remains available.

Section 3 specifies \(728\) numbered conditions, including the six bases, by exact integer coordinates and backward references. The final one has \(A=\varnothing\), an envelope of \(251\) cells, and height \(21\). Section 4 turns the recursive proof into one policy chosen before Breaker’s play. The independent four-in-a-row result follows in Section 5. Section 6 distinguishes the mathematical induction, exact data identities, and independent finite calculations. Appendix 7 proves the reduced-envelope construction and its five-class opening. Appendix 8 gives the complete \(35\)-move construction, its unbounded opening, and its conditional tactics. Appendix 9 describes the finite reconstruction supplement. Appendices 10–12 print the three literal certificates, and Appendix 13 explains the standalone verification programs.

Coordinates, placements, and expressions

The coordinate alphabet is

A two-character word XY denotes the point \((x,y)\) whose coordinates are the positions of X and Y in this alphabet, counting from zero. For example, 88 means \((8,8)\), 7A means \((7,10)\), and GG means \((16,16)\). The encoded pivots and translation vectors have nonnegative coordinates; the sets produced after signed transformations may contain negative coordinates.

A reference j:sUV means: take numbered card \(j\), apply the signed coordinate permutation \(R_s\), and then translate by the point encoded by UV. To compute \(R_s\), negate the first coordinate if the bit of weight \(2\) is set, negate the second if the bit of weight \(4\) is set, and then interchange the coordinates if the bit of weight \(1\) is set. The resulting maps are \[ \begin{array}{c|cccc} s&0&1&2&3\\ \hline R_s(x,y)&(x,y)&(y,x)&(-x,y)&(y,-x)\\[2pt] \end{array} \quad \begin{array}{c|cccc} s&4&5&6&7\\ \hline R_s(x,y)&(x,-y)&(-y,x)&(-x,-y)&(-y,-x). \end{array} \tag{5}\] These are precisely the eight matrices in \(\mathcal G\). A bare reference j uses the identity placement. References change neither the child’s height nor the meaning of its winning condition.

Every data line consists of its decimal card number \(j\), a pivot coordinate, and a nonempty ordered list of children. Each child is either a reference or an expression of the form

Such an expression combines its children at the pivot XY using (2). All coordinates inside parentheses remain in the coordinate frame of the line. They are not offsets from the enclosing pivot. When the entire card is later placed by an affine map, that map transports every pivot and set in its proof.

Cards \(0,\ldots,5\) are the six bases (4). The data specify cards \(6,\ldots,727\) in order. Every numbered reference in a line, including a reference inside parentheses, is to a smaller card number. We evaluate innermost expressions first, using (2) for the sets and height. Consequently structural induction on each expression, followed by induction on the line number, proves that every resulting card is a valid claim. The finite calculation determines which sufficient conditions this particular list produces.

Two elementary cards

The first two lines illustrate both the geometry and the encoding:

6 14 4:100 5:101
7 05 6:001 6:405

For card \(6\), the two bases are first transposed; the second is also translated by \((0,1)\). Direct substitution gives \[ A_6=\{(0,y):0\le y\le4\},\qquad T_6=A_6\cup\{(1,3),(1,4),(1,5)\},\qquad h_6=2. \tag{6}\] Claiming \((1,4)\) prepares two copies, completed respectively at \((1,3)\) and \((1,5)\). Unless a copy is already complete, Breaker can occupy at most one of these cells. Figure 2 shows the two alternatives.

For card \(7\), the two copies of \(A_6\) both occupy the column \(x=0\), \(1\le y\le5\). Their additional envelope cells have heights \(4,5,6\) and \(0,1,2\), respectively. These triples are disjoint, so the intersection of the envelopes is precisely the common column. Deleting the pivot \((0,5)\) therefore gives \[\begin{split} A_7&=\{(0,y):1\le y\le4\},\qquad h_7=3,\\ T_7&=\{(0,y):1\le y\le5\} \cup\{(1,y):y\in\{0,1,2,4,5,6\}\}. \end{split}\] The general certificate repeats this mechanism with longer conditional continuations and cells that need not lie near the current line of Maker stones.

The final card

For clarity, Table 1 records how the final empty requirement arises. The last line has \(32\) placed children, grouped by their six card numbers. Each placed required set is exactly \(\{(8,8)\}\). The last column is the number of cells other than \((8,8)\) in the intersection of the envelopes from that group and all preceding groups. The full placements occur in the last line of the certificate.

In particular, the intersection of all child envelopes is exactly \(\{(8,8)\}\): it contains that point because every child requirement does, and the last table entry removes every other point. The union of the child requirements is the same singleton. Equation (2) therefore gives \(A_{727}=\varnothing\). The maximum child height is \(20\), giving the bound \(21\).

The data also illustrate how play may leave an immediately adjacent line. After Maker plays \((8,8)\) and Breaker replies \((7,8)\), the placed child 708:100 is available. Its pivot is \((8,7)\). If Breaker next takes \((8,6)\), the child 684:011 of card \(708\), still under the outer transposition, is available and has pivot \((11,8)\). These are legal illustrative choices, not imposed responses by Breaker. Every other reply is covered by the same intersection rule.

A five-cell fork

Suppose Maker owns the horizontal five \(\{(r,0),\ldots,(r+4,0)\}\). For an endpoint \(e\in\{r,r+4\}\) and a sign \(\varepsilon\in\{-1,1\}\), put \[ H(e,\varepsilon)= \{(e-1,\varepsilon),(e,\varepsilon),(e+1,\varepsilon)\}. \tag{8}\] If this triple is clean at Maker’s turn, claiming its middle cell \((e,\varepsilon)\) creates two one-cell completions, at its other two cells. The two targets use respectively the first and last four-cell subrows of the five; they are reflected or translated copies of \(S\). Breaker can occupy at most one completion, so Maker wins on the next move unless it has already won. This is the horizontal version of Figure 2.

The four triples in (8) are pairwise disjoint. Consequently, if Maker has just created the five and at least two of these triples are clean before Breaker’s response, at least one remains clean afterwards, and the fork wins. The same assertion holds after interchanging the coordinates. For a vertical five we use the notation \[V(c,d)=\{(c,d-1),(c,d),(c,d+1)\},\] where \(c\in\{-1,1\}\) and \(d\) is an endpoint height.

The perpendicular endpoint attack

We first establish a local tactic at the right endpoint of a row. Assume Maker owns the four cells \[(-3,0),\quad(-2,0),\quad(-1,0),\quad(0,0),\] and the set \[ Z=\{(x,y):x\in\{-1,0,1\},\ 1\le |y|\le4\} \tag{9}\] is clean. Other ownership is arbitrary. Maker claims \((0,1)\), forcing \((1,1)\), and then \((0,-1)\), forcing \((1,-1)\). Indeed, the original horizontal body with the respective pair of cells above or below its endpoint is an allowed Snaky. If Breaker declines either forced reply, Maker completes that copy on its next turn.

After those two replies, Maker claims \((0,2)\). Denote the new Breaker reply by \(b\), and set \[E=\{(0,-2)\}\cup V(-1,-2)\cup V(-1,2).\] Figure 3 separates the two possible continuations after this reply. If \(b\notin E\), Maker claims \((0,-2)\). It now owns the vertical five from height \(-2\) to height \(2\), and both \(V(-1,-2)\) and \(V(-1,2)\) are clean before the ensuing Breaker reply. They are disjoint, and neither of the two earlier forced Breaker cells is in either triple. The five-cell fork therefore wins.

If \(b\in E\), Maker instead claims \((0,3)\), creating the vertical five from height \(-1\) to height \(3\). The triple \(V(1,3)\) is clean. The triple \(V(-1,3)\) is also clean unless \[b=(-1,2)\quad\hbox{or}\quad b=(-1,3).\] If both are clean, the same two-triple argument wins. In either exceptional case there is instead an immediate completion at \(q=(-1,-1)\), because Maker already owns the other five cells of \[ \{(0,3),(0,2),(0,1),(0,0),(-1,0),(-1,-1)\} =\{(-y,3-x):(x,y)\in S\}. \tag{10}\] The cell \(q\) lies in the initially clean zone, and differs from \(b\) and from the two earlier forced replies. It is thus free unless Maker already owns it, in which case the target is complete. It also lies outside \(V(1,3)=\{(1,2),(1,3),(1,4)\}\). Breaker must either claim \(q\), leaving that clean triple for the five-cell fork, or leave \(q\) as an immediate winning move. This completes the endpoint tactic.

Every prescribed target or threat cell in this tactic lies in \(\{-3,-2,-1,0\}\times\{0\}\) or in \(Z\). Fresh replacement moves may be elsewhere on the board. In particular, arbitrary Breaker moves outside the stated zone are included in the preceding cases and cannot defeat the tactic.

Proof of the four-in-a-row result

Proposition 7 is a sufficient condition at an arbitrary Maker turn. Its proof does not assume that the four stones were obtained consecutively, and the \(21\)-move theorem does not assume that its three-blocker hypothesis occurs during play. The full certificate supplies the empty-board strategy.

Exact reconstruction

All calculations use finite sets of integer pairs. Each primary program parses its literal data, checks the grammar and backward references, applies the specified placements, and reconstructs every required set, envelope, and height. A separate implementation for each dialect independently parses and reconstructs the same data. These programs are supplied with the complete editable source; no strategy search, network connection, or undistributed game tree is needed. Appendix 13 gives the commands.

For the \(21\)-move certificate the reconstruction includes every inline node, its enclosing coordinate frame, and the \(32\) children of the last card. It checks the endpoint, including containment of its 251-cell envelope in \(\{0,\ldots,16\}^2\), the elementary cards, the successive intersections in Table 1, and the nonlocal continuation. There are \(37,042\) local reply classes over all combination nodes. For the \(25\)-move certificate it checks all \(2,010\) reduced compositions, their normalized full cards, the required-size histogram, the five exceptional opening classes, and the elementary and nonlocal examples. For the \(35\)-move certificate it checks all \(616\) templates, \(26,703\) local reply classes, the four terminal interfaces, and the longer tactical identities in Appendix 8.

A local reply check uses the minimal Maker ownership required after the pivot; additional Maker cells only remove possible legal replies. One exterior case represents cells outside the parent envelope, since every child envelope lies inside it. In the reduced encoding this statement is applied after normalization. These finite checks support the set calculations. Their coverage of arbitrary ownership and the infinite board follows from the proved composition rule. Likewise, tests of sample opening coordinates supplement the symbolic whole-grid opening proof in Appendix 8.

The supplied test harnesses compare the full reconstructed cards, not only terminal cardinalities. They also test rejection of malformed or truncated inputs and execution with Python optimization. Programs either use explicit exceptions for required checks or refuse execution when assertions have been disabled. The harnesses state their finite checks separately from the game-theoretic claims.

Literal identities and formal coverage

The literal data are printed in Appendices 10–12. Their literal SHA-256 identities are

21: 3fa12d36a6d4dbb185e3f2808c8dfde13d85ee309afbca030d6ad17ae9fe3d04
25: 41cd04620af889771862dcceda7383afd99933ae03ddb0a566a00d742a8249b0
35: 16d077f0b64df70dd67fb6e9651636d42eaab0ce0f01f46180a57846e38fedc2

The middle file includes its initial newline and all \(41\) index markers. The source guide also records the normalized numeric serialization of that table; it is a separate identity from the full literal. The programs read these files as data and do not execute them as code. Matching bytes do not replace reconstruction, and matching sets do not replace the semantic induction or the move-count argument.

Appendix 9 records the scope of the finite reconstruction supplement for the \(35\)-move certificate. This supplement proves seven finite reconstruction claims. It does not prove a complete winning strategy, the \(21\)- or \(25\)-move construction, or the finite-board corollary. The finite Python reconstructions do not themselves establish a Lean theorem or kernel compilation. All three conventional proofs are given independently of this supplement.

Reduced requirements and their normalization

Let \(P,E\subset\mathbb Z^2\) be finite and let \(h\geq1\) be an integer. A valid reduced card \((P,E,h)\) means the following: at every Maker turn with finite disjoint ownership sets \(M,B\), if \[ P\subseteq M,\qquad B\cap E=\varnothing, \tag{12}\] Maker has already won or can win within \(h\) further actual Maker claims. We do not impose \(P\subseteq E\), nor do we require \(P\) and \(E\) to be disjoint. Additional Maker cells and arbitrary Breaker cells outside \(E\) are allowed. A signed permutation and translation applied to both sets preserves validity and height, by the same transport argument as for full cards.

The normalization \[ (P,E,h)\longmapsto (A,T,h)=(P,P\cup E,h) \tag{13}\] preserves exactly the admissible positions. Indeed, \(P\subseteq M\) and \(M\cap B=\varnothing\) already imply \(B\cap P=\varnothing\); under that assumption, \[B\cap E=\varnothing \quad\Longleftrightarrow\quad B\cap(P\cup E)=\varnothing.\] Conversely, a full card \((A,T,h)\) with \(A\subseteq T\) has the reduced representative \((A,T\setminus A,h)\). Normalizing this representative returns \((A,T,h)\) exactly. Normalizing an arbitrary \((P,E,h)\) and then reducing replaces \(E\) by \(E\setminus P\); this changes no hypothesis on a legal position. Thus disjoint reduced sets are convenient representatives, not an extra assumption in the semantics.

The same argument has a Breaker-turn form. If immediately before a Breaker reply Maker owns \(P\cup\{x\}\) and Breaker avoids \(E\), then after that reply a child applies within at most \(\max_jh_j\) further Maker claims. The attack cell need not have been the latest Maker claim. This follows directly from ownership of \(H\) and the older Breaker avoidance proved above.

Bases, anchors, and the decimal certificate

All attacks in the local coordinates of a \(25\)-card occur at \(o=(0,0)\). Order the target cells as \[(L_0,\ldots,L_5)=((0,0),(1,0),(2,0),(3,0),(3,1),(4,1)).\] Thus \(S=\{L_0,\ldots,L_5\}\). The six base cards are \[ P_i=(S\setminus\{L_i\})-L_i, \qquad E_i=\{o\},\qquad h_i=1, \qquad 0\leq i<6. \tag{16}\] If \(o\) is already Maker’s, the translated target \(S-L_i\) is already complete. Otherwise \(o\) is free and completes it in one move. Their normalized envelopes are exactly \(S-L_i\).

For a reference to card \(j\), order its required set \(P_j\) lexicographically, by the first coordinate and then the second, starting with index zero. Write a placement code \(r\) uniquely as \(r=8k+d\), \(0\leq d<8\), and let \(a_{j,k}\) be the \(k\)th cell in that order. The code is defined only when \(0\leq k<|P_j|\). Set \[ \Phi_{j,r}(v)=R_d(v-a_{j,k}), \tag{17}\] where the signed permutations are given explicitly by

Equivalently, swap first when \(d\) is odd, then negate the first coordinate for the bit of value \(2\), and the second for the bit of value \(4\). In particular codes \(3\) and \(5\) use the swap-first order; they must not be interpreted using the \(21\)-card decoder. Each map in (17) aligns one required child cell with the parent’s attack \(o\). The anchor is taken from \(P_j\), not \(E_j\) or the normalized envelope. A child placement inside a current placement \(F\) is \(F\circ\Phi_{j,r}\).

The complete literal certificate, printed in Appendix 11 and supplied as , has \(2010\) numeric lines defining cards \(6\) through \(2015\) in order. Blank lines have no effect. A marker # n asserts that the next card number is \(n\) and creates no card. There are \(41\) such markers. Every numeric line consists of decimal blocks of exactly three digits. At current card \(i\), read these blocks from left to right; a block with value \(b\) decodes as follows: \[ \begin{array}{c|c|c} \text{condition}&\text{referenced card }j&\text{placement code }r\\ \hline 0\leq b<240&\lfloor b/40\rfloor&b\bmod40\\ 240\leq b<740&i-1-\lfloor(b-240)/100\rfloor&(b-240)\bmod100\\ 740\leq b\leq999&10(b-740)+\lfloor c/100\rfloor&c\bmod100 \end{array} \tag{18}\] The last case consumes the next three-digit block as \(c\) as well. A missing second block is invalid. Leading zeros are part of the three-digit format. Every resulting pair \((j,r)\) must satisfy \(0\leq j<i\) and the anchor range in (17), and each numeric line must contain at least one pair.

For the decoded list \(\mathcal L_i\) of card \(i\), form the placed children \[(\Phi_{j,r}(P_j),\Phi_{j,r}(E_j),h_j),\qquad (j,r)\in\mathcal L_i,\] and apply (14) at \(x=o\) to define \(P_i,E_i,h_i\). Every placed required set contains \(o\), because of its anchor. The resulting \(P_i\) and \(E_i\) are disjoint, and \(o\in E_i\). These properties are consequences of the recurrence; the soundness proof did not assume them. All references are backward, so induction from (16) proves the validity of every card whose line decodes. No game-tree search or additional compatibility test is needed: the union and intersection in the composition formula put all necessary extra ownership into the parent’s required set.

For example, 193233 decodes into \((4,33),(5,33)\). The next line, 165272, decodes at \(i=7\) into \((4,5),(6,32)\). At \(i=2015\), 927400 is an extended term \((1874,0)\), whereas 240 is the relative term \((2014,0)\). Thus all three cases in (18) refer to the same anchor placement rule after decoding.

The first two composite cards

The first two rows exhibit both simultaneous finishes and transfer after a forced block. For card \(6\), the two codes \(33=8\cdot4+1\) use anchors \((1,0)\in P_4\) and \((-1,0)\in P_5\), respectively. Their placed envelopes are the singletons \(\{(0,-1)\}\) and \(\{(0,1)\}\). Their placed required sets are \[\{(-1,t):-4\leq t\leq-1\}\cup\{o\},\qquad \{(-1,t):-3\leq t\leq0\}\cup\{o\}.\] The intersection of the two singleton envelopes is empty. Composition therefore gives exactly \[ P_6=\{(-1,t):-4\leq t\leq0\},\qquad E_6=\{(0,-1),o,(0,1)\},\qquad h_6=2. \tag{19}\] After the attack at \(o\), the two one-hole copies have different holes. If neither is already complete, a single Breaker reply cannot block both. All five cells of the required column are outside \(E_6\); this is an explicit reason the reduced notation must allow \(P_6\not\subseteq E_6\).

For card \(7\), code \(5\) at card \(4\) uses the first lexicographic anchor \((-3,-1)\) and \(R_5(x,y)=(y,-x)\). Its placed required set and hole are \[\{(0,-3),(0,-2),(0,-1),o,(1,-4)\}, \qquad \{(1,-3)\}.\] Code \(32=8\cdot4\) at card \(6\) uses anchor \((-1,0)\) and is translation by \((1,0)\). Its placed required set is \(\{(0,t):-4\leq t\leq0\}\), its envelope is \(\{(1,-1),(1,0),(1,1)\}\), and its attack is \((1,0)\). Again the two child envelopes are disjoint, giving \[ \begin{split} P_7&=\{(0,-4),(0,-3),(0,-2),(0,-1),(1,-4)\},\\ E_7&=\{o,(1,-3),(1,-1),(1,0),(1,1)\},\qquad h_7=3. \end{split} \tag{20}\] After the attack at \(o\), failure to block \((1,-3)\) lets Maker complete the base child on the next move. A block there leaves the translated card \(6\) available, whose next attack is \((1,0)\). If one of these attacks was already owned, the general card semantics either detects an earlier target or charges the required fresh replacement. The ensuing reply is never skipped. Figure 4 displays the two configurations.

The complete finite reconstruction and its endpoint

We now apply the same recurrence to the entire literal, retaining every row. The supplied primary program and independent program reconstruct its finite sets and heights. Their checks include the decimal grammar, every backward reference and anchor, the marker numbers, the required number of rows, and the exact endpoint. Malformed or truncated input is rejected; Appendix 13 gives the verification commands and their scope. Their finite arithmetic supports the set identities below; the reason these sets give a game strategy is Proposition 8 and the induction just proved, independently of either program.

The complete reconstruction has \(2016\) cards and \(5862\) placed child terms. The number of cards of each required-set size is \[ \begin{array}{c|rrrrrrrrrrr} |P_i|&0&1&2&3&4&5&6&7&8&9&10\\ \hline \text{number}&1&5&52&217&448&523&416&219&103&30&2. \end{array} \tag{21}\] The last card can also be inspected through the much smaller terminal table. Its \(28\) children comprise exactly the following five groups in the printed order. Each listed code has anchor index \(k=0\). The last column gives the size of the intersection of all placed reduced envelopes through the end of that row of the table.

The required sets of these five child cards are \[ P_{1874}=P_{1985}=P_{1996}=\{(-1,0)\},\qquad P_{1998}=\{(0,1)\},\qquad P_{2014}=\{(1,0)\}. \tag{22}\] Every placed requirement is therefore \(\{o\}\). The table gives \(U=\{o\}\) and \(I=\varnothing\), hence \(H=\{o\}\) and \[ P_{2015}=\varnothing,\qquad |E_{2015}|=389,\qquad h_{2015}=25. \tag{23}\] The last height is \(1+24\), not a bound obtained by identifying this certificate with either of the other two constructions.

For an explicit description of the final finite region, its section at ordinate \(y\) is empty when \(|y|>11\); otherwise it is the set of integer abscissae in the following table:

Here intervals mean all integer points. The row counts give \(21+2(23+21+23+21+21+19+15+13+13+11+4)=389\).

Why only five first-reply classes need extra cards

The final row can be understood geometrically as a cover of all first Breaker replies. After Maker takes \(o\), each of the eight placements \(\Phi_{2014,d}\), \(0\leq d<8\), has required set \(\{o\}\). Let \(D\) be the intersection of their reduced envelopes. The exact finite calculation is \[ \begin{split} D={}&\{(\pm t,0),(0,\pm t):t=1,2,3\}\\ &\ \cup\{(\pm1,\pm1)\} \cup\{(\pm2,\pm1),(\pm1,\pm2)\}, \end{split} \tag{24}\] with independent signs. It contains \(24\) cells. In particular the sorted absolute coordinates, larger first, have exactly the five values \[(1,0),\quad(1,1),\quad(2,0),\quad(2,1),\quad(3,0).\] The set \(D\) is invariant under all signed permutations: composing any one of those permutations with the eight placements merely permutes them. Equation (24) is a finite set identity, so it covers unbounded first replies as well: for every \(b\notin D\), at least one of the eight envelopes omits \(b\). That placement of card \(2014\) is already available, giving at most \(14\) further claims.

For the five remaining classes, the following placements omit the listed first Breaker cell. All use \(k=0\) and have placed required set \(\{o\}\).

For example, the first placement is \(\Phi_{1874,2}(x,y)=(-x-1,y)\) because its anchor is \((-1,0)\); the fourth is \(\Phi_{1998,2}(x,y)=(-x,y-1)\) because its anchor is \((0,1)\). These formulas give the displayed attacks directly. For an arbitrary reply in one of the five classes, choose a signed permutation \(Q\) taking its representative to that reply and use the placement \(Q\circ\Phi_{j,d}\). It still requires only \(o\), and its envelope omits that reply. Thus the table and the eight placements of card \(2014\) give a direct whole-board opening proof, with largest total \(1+24=25\). The terminal row in Table 2 encodes a finite opening cover of this kind using its specified \(28\) placements.

Two continuations that leave the initial line

We finish by following two actual children of card \(1874\). This makes the composition of coordinate maps visible and shows why an implementation must retain the complete envelopes. Suppose Maker has played \(o\), Breaker has replied \((1,0)\), and Maker uses the first row of Table 3 to attack \((-1,0)\). The current outer placement is \[F(x,y)=\Phi_{1874,2}(x,y)=(-x-1,y), \qquad M=\{o,(-1,0)\},\qquad B=\{(1,0)\}\] before Breaker’s next reply. The two following continuations are present in the literal row for card \(1874\):

For the first, the native required set is \(P_{1716}=\{(-3,-1),(-2,-1)\}\). Since \(8=8\cdot1+0\), the lexicographic anchor is the second point, \((-2,-1)\), and \[\Phi_{1716,8}(x,y)=(x+2,y+1),\qquad (F\circ\Phi_{1716,8})(x,y)=(-x-3,y+1).\] The transformed requirement is precisely \(\{o,(-1,0)\}\). The reduced envelope has \(256\) cells and satisfies the exact check \[ (F\circ\Phi_{1716,8})(E_{1716}) \cap\{(1,0),(-1,-1)\}=\varnothing. \tag{25}\] Thus the old reply as well as the new reply is excluded, and the transformed pivot is \((-3,1)\). It is distinct from all four cells then owned by either player. Card \(1716\) supplies a height-\(23\) continuation after the first two Maker claims, consistent with the total bound \(25\).

For the second, \(P_{1752}=\{(-2,0),(-2,1)\}\) and \(r=3\) selects the first anchor and the swap-first map \(R_3(x,y)=(-y,x)\). Hence \[\Phi_{1752,3}(x,y)=(-y,x+2),\qquad (F\circ\Phi_{1752,3})(x,y)=(y-1,x+2).\] Its requirement is again exactly \(\{o,(-1,0)\}\), while its \(93\)-cell reduced envelope satisfies \[ (F\circ\Phi_{1752,3})(E_{1752}) \cap\{(1,0),(-2,0)\}=\varnothing. \tag{26}\] Its pivot \((-1,2)\) is free, and this child has height \(15\). Equations (25)–(26) use the complete reconstructed envelopes, not just the new pivot or the required pair of Maker cells.

The two replies here are legal examples, not forced Breaker choices. For either example the indicated child is usable; the globally fixed first-surviving-child policy may select an earlier usable child in the same row. Other replies are covered by the full child list and Proposition 8. Neither the game nor this certificate restricts Maker’s holdings to a connected shape: these two attacks deliberately leave the initial horizontal pair.

The letter-and-offset certificate

Write the target points in the fixed order \[s_0=(0,0),\quad s_1=(1,0),\quad s_2=(2,0),\quad s_3=(3,0),\quad s_4=(3,1),\quad s_5=(4,1), \qquad o=(0,0).\] The six initial cards are \[ T_i^{35}=S-s_i,\qquad A_i^{35}=T_i^{35}\setminus\{o\},\qquad h_i^{35}=1 \quad(0\le i\le5). \tag{27}\] They are valid by immediate completion. If the missing point is already Maker-owned, the target has already been obtained.

For \(i=6,\ldots,615\), the literal row consists of \(i\) followed by a nonempty list of placement terms. A term kLuv contains an earlier decimal row index \(k<i\), one letter \(L\), and two individual decimal digits \(u,v\). Its placement is \[ F_{Luv}(x,y)=R_L(x,y)+(u-4,v-4), \tag{28}\] with the eight maps specified by

Thus 614b43 means \((x,y)\mapsto(y,x-1)\), including its translation; it is not one of the decimal orientation codes used in the other two certificates.

If the terms of row \(i\) are \((k_j,L_ju_jv_j)\), put \(C_j=F_{L_ju_jv_j}(A_{k_j}^{35})\) and \(D_j=F_{L_ju_jv_j}(T_{k_j}^{35})\). Define \[ \begin{split} T_i^{35}&=\{o\}\cup\bigcup_j D_j,\\ A_i^{35}&=\left(\bigcup_j C_j\ \cup\ \bigcap_jD_j\right) \setminus\{o\},\\ h_i^{35}&=1+\max_j h_{k_j}^{35}. \end{split} \tag{29}\] Lemma [thm:composition] and induction on \(i\) prove every card defined in this way. The inductive argument is valid for every syntactically correct list of backward references; the particular list determines the useful required sets and envelopes.

For clarity, the complete finite substitution can be performed as follows. Initialize the six triples by (27). Read each remaining row in increasing order, reject an empty list or a reference outside \(0,\ldots,i-1\), decode each affine map by (28), and apply it to both stored sets. Take the union and intersection in (29), store the resulting triple, and proceed to the next row. All coordinates are integers and all sets are finite. At the end of each iteration the stored triples are exactly the triples defined by the displayed equations, which is the loop invariant justifying the reconstruction.

The complete 610-row literal is printed in Appendix 12 and supplied as verification/supporting/prior-35/certificate.txt; it has one row per line, including the final newline. The primary and two independent reconstructions are described in Appendix 13. They use, respectively, integer matrices and ordinary set operations, quarter turns and incidence masks, and signed coordinate lookups with cellwise membership tests. Thus no search procedure or undisclosed strategy tree is needed to recover the certificate.

The first two compositions: five cells in a row

The first two nonbase rows are \[\texttt{6 0a03},\qquad \texttt{7 4a34 6a54}.\] Set \[L_- = \{-4,-3,-2,-1\}\times\{-1\},\qquad L_+ = \{-3,-2,-1,0\}\times\{-1\}.\] Row 6 has \[T_6^{35}=S+(-4,-1)=L_-\cup\{(-1,0),o\},\qquad A_6^{35}=L_-\cup\{(-1,0)\},\qquad h_6^{35}=2.\] The height is the recursively assigned upper bound: after claiming its pivot, Maker has in fact completed this target immediately.

The two placed children in row 7 have \[ \begin{array}{c|c|c} \text{term}&\text{required set}&\text{envelope}\\ \hline \texttt{4a34}&L_-\cup\{o\}&L_-\cup\{(-1,0),o\}\\ \texttt{6a54}&L_+\cup\{o\}&L_+\cup\{o,(1,0)\}. \end{array} \tag{30}\] Their common envelope is \((\{-3,-2,-1\}\times\{-1\})\cup\{o\}\), already contained in the union of their required sets. Consequently \[A_7^{35}=\{-4,-3,-2,-1,0\}\times\{-1\},\qquad T_7^{35}=A_7^{35}\cup\{(-1,0),o,(1,0)\},\qquad h_7^{35}=3.\] After Maker owns the five lower cells and the pivot \(o\), either \((-1,0)\) or \((1,0)\) completes one of the two displayed copies. Both lie in the parent envelope, so neither is occupied by an earlier Breaker stone. If neither target is already complete, Breaker can claim at most one of these two cells. This is the elementary double threat that the longer compositions reuse. Its direct two-claim bound is sharper than the stored height 3; the certificate deliberately uses the uniform recursion (29).

Four conditional outputs

The following finite identities supply the opening. A set in the last column is wholly disjoint from the envelope; it is not asserted to be the entire complement of that envelope.

The complete ordinary opening

Transferring a four-cell attack to a new pair

We now examine the longer tactics inside the certificate. They explain how a small required set can support a continuation even after several forced parries. The conditions always concern the entire envelope; the visible stones alone do not license a card.

Put \(V=\{-1\}\times\{-4,-3,-2,-1\}\). The relevant literal rows and reconstructed outputs are \[\texttt{588 3b33 586a45},\qquad \texttt{589 4b43 588a45},\] \[ \begin{array}{c|c|r|r} i&A_i^{35}&|T_i^{35}|&h_i^{35}\\ \hline 586&\{(0,-2),(0,-1)\}&198&26\\ 588&(V\setminus\{(-1,-1)\})\cup\{(0,-1)\}&202&27\\ 589&V&204&28. \end{array} \tag{34}\] Their envelopes satisfy the more informative identities \[ \begin{split} T_{588}^{35}&=(T_{586}^{35}+(0,1))\cup V,\\ T_{589}^{35}&=(T_{586}^{35}+(0,2)) \cup (\{-1\}\times\{-4,-3,-2,-1,0\})\cup\{(0,-1)\}. \end{split} \tag{35}\] In particular, each smaller continuation envelope is contained in the envelope under which the tactic starts.

For an explicit description of these envelopes, Table 4 gives every vertical fiber of \(T_{586}^{35}\). In this table \([a,b]_{\mathbb Z}\) means every integer from \(a\) to \(b\), and unlisted fibers are empty. Together with (35), it specifies all three complete envelopes, including cells far from the initial column.

Suppose \(V\subseteq M\) and \(B\cap T_{589}^{35}=\varnothing\) at a Maker turn. Claim \(o\) (or make the charged fresh replacement if it is already owned). The set \[Q_1=V\cup\{o,(0,-1)\}\] is the target in the placed base card 4b43. Its only possibly missing Maker cell is \((0,-1)\). If this point is already owned, Maker has won. Otherwise it is free, because it lies in the parent envelope. A Breaker reply other than \((0,-1)\) leaves that immediate completion available, so any defense avoiding this win must claim \((0,-1)\).

The other child 588a45 uses the map \(z\mapsto z+(0,1)\). Its required set is \[(\{-1\}\times\{-3,-2,-1\})\cup\{o\},\] which is contained in the Maker set. Its envelope \(T_{588}^{35}+(0,1)\) is a subset of \(T_{589}^{35}\) and omits \((0,-1)\). All Breaker cells, including that first parry, therefore avoid it. Claim its pivot \((0,1)\), with the same charged-replacement convention if necessary. Now \[Q_2=\{(-1,-3),(-1,-2),(-1,-1),(-1,0),o,(0,1)\}\] is complete except possibly at \((-1,0)\). It is another allowed target: \(Q_1=R_b(S)+(-1,-4)\) and \(Q_2=R_b(S)+(-1,-3)\). Thus, unless Maker has already won or can complete \(Q_2\) on the next move, Breaker must parry at \((-1,0)\).

After these two parries, the continuation 586a45 of the translated row 588 is row 586 translated by \((0,2)\). Its required set is exactly \(\{o,(0,1)\}\), now owned. Its envelope \[D=T_{586}^{35}+(0,2)\] lies in the original envelope and contains neither parry: \((0,-1)\notin D\) and \((-1,0)\notin D\). These omissions follow directly from the fibers \(x=0\) and \(x=-1\) in Table 4. The envelope of the preceding row-588 continuation likewise omits the first parry by (35). Row 586 therefore applies at the next Maker turn, with pivot \((0,2)\) and bound 26. The two earlier claims and their forced replies have transferred the attack from the original column to a new vertical pair, at total cost at most \(1+1+26=28\) Maker claims.

This argument preserves every earlier Breaker restriction: all earlier Breaker cells lie outside the original envelope and hence outside every continuation envelope. Extra Maker cells may complete a target early or occupy one of the prescribed pivots; in the latter case a genuinely fresh replacement uses the same charged turn. No assumption that the displayed stones are the only owned stones is needed.

Opposite-tip continuations from four in a row

Row 612 consists exactly of \[\texttt{612 589b55 589h03}.\] Writing \[W=\{-3,-2,-1,0\}\times\{0\},\qquad G_+(x,y)=(y+1,x+1),\quad G_-(x,y)=(-y-4,-x-1),\] the two placed requirements are both \(W\), and their envelopes obey \[ G_+(T_{589}^{35})\cap G_-(T_{589}^{35})=W. \tag{36}\] Consequently \[A_{612}^{35}=W\setminus\{o\},\qquad T_{612}^{35}=G_+(T_{589}^{35})\cup G_-(T_{589}^{35}),\qquad |T_{612}^{35}|=404,\quad h_{612}^{35}=29.\] After Maker adds the pivot, \(W\) is owned. A legal Breaker reply therefore cannot belong to both child envelopes; choose a child whose envelope it misses. All earlier Breaker cells avoid both envelopes by the parent hypothesis, and the full required column of the selected copy of row 589 is already owned. Its next pivot is either \((1,1)\) or \((-4,-1)\), so the two attacks leave from opposite ends of the four-cell row. The transferred pair in the selected frame is \(G_+(\{o,(0,1)\})\) or \(G_-(\{o,(0,1)\})\), respectively. Identity (36) is what ensures a safe continuation against every reply, including replies far from the displayed four stones.

The overlap identity can also be read directly from Table 4 and (35). The vertical supports of the two placed envelopes are \([-6,12]_{\mathbb Z}\) and \([-12,6]_{\mathbb Z}\), respectively. On their common possible levels \(-6\le y\le6\), the fibers have separated extrema for every \(y\ne0\): the rightmost point of the \(G_-\) fiber is strictly left of the leftmost point of the \(G_+\) fiber. At \(y=0\), the \(G_+\) fiber is \([-3,14]_{\mathbb Z}\) and the \(G_-\) fiber is \([-17,0]_{\mathbb Z}\). Their overlap is \([-3,0]_{\mathbb Z}\). This gives exactly \(W\), and also explains the envelope count \(204+204-4=404\).

The exceptional bent-shape continuation

The near opening reaches the local Breaker-turn position with \(P=\{o,(1,0)\}\) owned and \(q=(1,-1)\) occupied by Breaker. Here the twelve child terms of row 615 are

For each term let \(C_j,D_j\) be its placed requirement and envelope. Every \(C_j\) equals \(P\), all \(D_j\) avoid \(q\), and their full intersection is \(P\). On deleting the second term, the intersection becomes \[ \bigcap_{j:\,\text{term}_j\ne\texttt{614b43}}D_j =P\cup\{(-1,0)\}. \tag{37}\] The next pivots in these eleven children are end extensions \((-1,0)\) or \((2,0)\). Since Breaker cannot claim a point of \(P\), one of them survives every next reply except \((-1,0)\). Against that exceptional reply, the only surviving child is 614b43. Its map and pivot are \[K(x,y)=(y,x-1),\qquad K(o)=(0,-1).\] The pivot is fresh in the near-opening position: it differs from both Maker points and both Breaker points \(q,(-1,0)\).

More explicitly, \[A_{614}^{35}=\{(1,0),(1,1)\},\qquad K(A_{614}^{35})=P,\qquad |T_{614}^{35}|=678,\qquad h_{614}^{35}=33.\] The complete envelope \(K(T_{614}^{35})\) lies in \(T_{615}^{35}\) and avoids both existing Breaker cells. An exact expression for the difference is \[ \begin{split} T_{615}^{35}\setminus K(T_{614}^{35}) =\{&(-15,0),(-15,2),(-14,0),(-14,1),\\ &(-14,2),(-13,-4),(-13,4),(-1,0)\}. \end{split} \tag{38}\] Thus the exceptional reply is excluded by the full continuation envelope, not merely by the three-cell configuration that Maker will obtain.

After Maker claims \((0,-1)\), write \(Q=P\cup\{(0,-1)\}\). The seven children of row 614, composed with \(K\), are listed in Table 5. In the table the term in the second column is expressed directly in the local coordinates of the near opening. For example, \(K\circ F_{b75}(x,y)=(x+1,y+2)=F_{a56}(x,y)\).

Let \(C'_j,D'_j\) be the placed sets of these seven terms. Their reconstructed identities are \[ C'_j=Q\quad\text{for every }j,\qquad \bigcap_{j=1}^7D'_j=Q,\qquad D'_j\subseteq K(T_{614}^{35})\quad\text{for every }j. \tag{39}\] The last inclusion excludes both old Breaker stones from every child envelope. Any legal third Breaker reply lies outside \(Q\), so the intersection identity supplies a child envelope it misses. Its required set is already owned, and its height is at most 32. The selected pivot belongs to that envelope and is outside \(Q\); hence neither an old Breaker cell nor the new reply occupies it. It is therefore fresh in this exact opening position. The full conditional version permits extra Maker ownership and uses a charged replacement if that pivot was owned previously.

The four distinct possible pivots are \((0,1),(0,-2),(2,0),(1,2)\), as shown in Figure 6. They are alternatives selected after the next Breaker reply, rather than a prescribed sequence of four Maker moves. The seven distinct envelopes in (39) determine which alternative is valid; the visible bent shape by itself does not justify any arbitrary choice. The bound after the exceptional second reply is \(1+32=33\) further Maker claims, including the bent-shape pivot, which agrees with the \(2+33=35\) opening calculation.

The finite reconstruction theorem

The finite reconstruction supplement linked from , relative to the article root, has the endpoint OAI.SnakyCertificate.certificate_correct. Its definitions fix the target, six ordered base points, eight letter-order orientations, offset-by-four translation digits, and full-envelope recurrence of Appendix 8. The formal envelope symbol \(H\) denotes \(T_i^{35}\) in that appendix. The theorem has seven clauses:

1. The table has exactly 610 nonbase rows, indexed \(6\) through \(615\), each with a nonempty list of allowed placements referencing earlier rows.

2. There are exactly 1,837 ordered placement terms, counted with multiplicity.

3. Row \(557\) has required set \(\{(-1,0)\}\), envelope size \(118\), height \(19\), and no envelope cell with \(x\leq-3\) and \(y\leq-2\).

4. Row \(595\) has required set \(\{(-1,0)\}\), envelope size \(222\), height \(27\), and no envelope cell with \(x=-2\) and \(y\leq-2\).

5. Row \(603\) has required set \(\{(-1,0)\}\), envelope size \(275\), height \(27\), and no envelope cell with \(x\leq-3\) and \(y=0\).

6. Row \(615\) has required set \(\{(1,0)\}\), envelope size \(686\), height \(34\), and omits \((1,-1)\) from its envelope.

7. Every row \(0\) through \(615\) satisfies \(A_i^{35}\subseteq T_i^{35}\), \((0,0)\in T_i^{35}\setminus A_i^{35}\), and \(h_i^{35}\leq34\).

The last clause makes the required-set containment proper. The literal entries in the Lean source agree with the printed letter-and-offset certificate. This is a finite reconstruction statement, not a game-winning theorem: it does not include the opening, the arbitrary-ownership and Breaker-turn interfaces, policy extraction, or the additional tactical conclusions of Appendix 8. The conventional arguments supply these game-theoretic implications.

The finite Python reconstructions described in this article are separate from Lean kernel checking; they do not themselves establish a Lean theorem or kernel compilation. The certificate copy under contains only the literal certificate data.

Independent reconstructions of all three certificates

The source distribution contains an additional, independently parsed reconstruction for every dialect, together with tests of the finite identities used in the article. From the paper root run

python3 verification/supporting/verify_all.py --output-dir ../all-checks

Choose a new output directory outside the paper directory. The command runs the primary and independent checks for all three literal tables and records their full-card agreement, exact identities, and rejection tests. The support guide gives each program’s standalone command. The \(21\)-move programs under verification/supporting/route21/ additionally check every inline node and local reply class; they are distinct from the short verifier printed above. The \(25\)-move programs under verification/supporting/route25/ use the reduced sets and swap-first anchor maps. The programs under verification/supporting/route35/ check the letter-and-offset table and its conditional and tactical identities. All three literal tables and every checking program are included in the editable source distribution. The directory verification/supporting/prior-35/ contains only a copy of the \(35\)-move literal certificate. The scope of the finite reconstruction supplement is stated in Appendix 9.