\documentclass[11pt,reqno]{amsart} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage{microtype} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{booktabs} \usepackage{array} \usepackage{enumitem} \usepackage{xcolor} \usepackage{float} \usepackage{hyperref} \usepackage{xurl} \usepackage{listings} \usepackage[nameinlink,noabbrev]{cleveref} \usepackage[a4paper,margin=1.10in]{geometry} \usepackage{tikz} \usetikzlibrary{arrows.meta,calc,positioning} \definecolor{paBlue}{HTML}{176B87} \definecolor{paCyan}{HTML}{1AA6B7} \definecolor{paCoral}{HTML}{E65F5C} \definecolor{paGold}{HTML}{E4A33A} \definecolor{paInk}{HTML}{172A3A} \definecolor{paIvory}{HTML}{F7F1E5} \definecolor{paGrid}{HTML}{73808A} \hypersetup{ colorlinks=true, linkcolor=paBlue, citecolor=paBlue, urlcolor=paBlue, pdftitle={An Exact Counterexample to Berlekamp's Temperature-2 Conjecture for Domineering}, pdfauthor={Lech Mazur}, pdfsubject={A Domineering temperature counterexample with Lean-checked value, target-thermograph, and reachability certificates}, pdfkeywords={Domineering, combinatorial game theory, temperature, thermograph, Berlekamp conjecture, Lean}, pdfdisplaydoctitle=true, pdflang=en } \setlist{nosep,leftmargin=*} \allowdisplaybreaks \emergencystretch=2em \raggedbottom \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \numberwithin{equation}{section} \newcommand{\G}{\mathcal G} \newcommand{\BP}{\operatorname{BP}} \newcommand{\temp}{\operatorname{t}} \newcommand{\mean}{\operatorname{m}} \newcommand{\LS}{\operatorname{LS}} \newcommand{\RS}{\operatorname{RS}} \newcommand{\cell}[2]{(#1,#2)} \title[Temperature $33/16$ in Domineering] {An Exact Counterexample to Berlekamp's\\ Temperature-$2$ Conjecture for Domineering} \author{Lech Mazur} \email{2022melodies@gmail.com} \date{August 14, 2026} \subjclass[2020]{Primary 91A46; Secondary 68W30} \keywords{Domineering, combinatorial game theory, temperature, thermograph, partizan game, exact computation, Lean, Berlekamp conjecture} \begin{document} \begin{abstract} Domineering is the partizan placement game in which Left places vertical dominoes and Right places horizontal dominoes. A long-standing conjecture attributed to Berlekamp asserted that every finite Domineering position has temperature at most $2$. We give a $28$-cell position $B'$ reached by an explicit $30$-move alternating sequence from an $11\times8$ rectangle, with \[ \G(B')=\left\{\frac{17}{8}\,\middle|\,-2+*\right\}. \] In the nonnegative-temperature convention used here, both options have temperature $0$, with thermograph masts $17/8$ and $-2$. Hence its thermograph has \[ \temp(\G(B'))=\frac{33}{16}>2, \qquad \mean(\G(B'))=\frac1{16}. \] The value calculation factors through a connected $26$-cell core $B$ with the same game value. The actual witness $B'$ is a translate of that core together with two isolated one-cell zero components. A checkerboard argument shows that $B$ alone is not a rectangle remainder, so it is used only as the compact computational core; $B'$ is the counterexample asserted by the main theorem. Lean verifies the complete board--target game equivalence, the explicit target's thermograph, and the $30$-move rectangle replay. Its final existential statement uses the narrow \texttt{HasValueTemperature} formulation described below; a proved checker validates all $995{,}069$ difference-game certificate states using ordinary kernel reduction. \end{abstract} \maketitle \begin{center} \fcolorbox{blue!45!black}{blue!4}{% \begin{minipage}{0.91\textwidth}\small \textbf{Generative-AI disclosure.} Generative AI played a substantial role in the discovery and derivation of the mathematics in this paper, not merely in editing its presentation. Lech Mazur served as curator and prompter, designed the orchestration and verification workflow, selected and reconciled the outputs, and takes responsibility for the manuscript and its claims. The model used was OpenAI GPT-5.6 Pro. It contributed to mathematical exploration, exact computation, adversarial auditing, and exposition. The work was developed as part of \href{https://proofatlas.ai/}{ProofAtlas.ai}, a project for organizing mathematical claims and their evidence. The board--target equality, target thermograph, and rectangle replay are formalized in Lean at frozen commit \texttt{9edd1d307a62bcd1b59c4450c8675fcdbb5a3ebe}: a proved checker validates the complete difference-game certificate, while Lean separately checks the board semantics, target thermograph, and rectangle replay. Algorithmically independent programs and the Lean development were produced in the author-led audit workflow and do not replace unrelated specialist review. Responsibility for any remaining errors lies with the human author. \end{minipage}} \end{center} \section{Introduction and main results} \label{sec:introduction} Domineering is played on a finite collection of grid cells. Left may cover two vertically adjacent empty cells with a domino, Right may cover two horizontally adjacent empty cells, dominoes may not overlap, and the first player unable to move loses. The game is generally credited to G\"oran Andersson around 1973; Martin Gardner presented it as \emph{crosscram} in 1974 \cite{Gardner1974}. It became a foundational example of a partizan game in the treatments of Conway and of Berlekamp, Conway, and Guy \mbox{\cite{Conway1976,BCG1982}}. Temperature measures urgency rather than winning probability or game length. In a disjunctive sum, the hottest component is often, but not always, the best place to move \mbox{\cite{BCG1982,HuntemannMaciosowski2026}}. Berlekamp's study of Blockbusting and Domineering developed heating and generalized overheating methods \cite{Berlekamp1988}. The conjecture conventionally bearing his name is \begin{equation} \temp(\G(P))\leq 2 \qquad\text{for every finite Domineering position }P. \label{eq:conjecture} \end{equation} The precise origin of the attribution is historically uncertain; the recent literature uses the name \lq\lq Berlekamp's conjecture\rq\rq\ while recording that caveat \cite{HuntemannMaciosowski2026}. For years the evidence reached the proposed boundary but did not cross it. Drummond-Cole exhibited a temperature-$2$ position in 2004 \cite{DrummondCole2004}. Subsequent large searches found many new temperatures and further boundary examples but none above $2$ \cite{ShankarSridharan2005,UiterwijkBarton2015,HuntemannMaciosowski2026}. We first isolate the compact connected core on which the exact value calculation is performed. The subsequent theorem gives the actual rectangle-reachable counterexample. For these statements, let $B$ denote the $26$-cell region defined explicitly in \cref{eq:board,fig:board}. \begin{proposition}[Exact connected value core] \label{prop:core} The region $B\subset\mathbb Z^2$ is connected, has $14$ legal Left moves and $14$ legal Right moves, and \begin{equation} \G(B)=\left\{\frac{17}{8}\,\middle|\,-2+*\right\}. \label{eq:mainvalue} \end{equation} Consequently \begin{equation} \temp(\G(B))=\frac{33}{16}>2, \qquad \mean(\G(B))=\frac1{16}. \label{eq:maintemp} \end{equation} \end{proposition} Some authors allow an arbitrary finite region as a position, while a stricter reading requires the empty cells to be reachable from a rectangular starting board. The connected board $B$ satisfies the former convention but, by a coloring obstruction, not the latter. The following main result covers both conventions. \begin{theorem}[Rectangle-reachable counterexample] \label{thm:main} Inside the rectangle $\{0,\ldots,10\}\times\{0,\ldots,7\}$, set \begin{equation} B'=\{(x+2,y):(x,y)\in B\}\cup\{(0,1),(1,4)\}. \label{eq:reachableboard} \end{equation} Then $B'$ is the exact remainder after an alternating sequence of $30$ legal moves, beginning with Left, on the full $11\times8$ rectangle. Moreover \[ \G(B')=\G(B)=\left\{\frac{17}{8}\,\middle|\,-2+*\right\}, \qquad \temp(\G(B'))=\frac{33}{16}>2, \qquad \mean(\G(B'))=\frac1{16}. \] Consequently \eqref{eq:conjecture} is false and $\BP(\mathrm{Domineering})\geq 33/16$. \end{theorem} The complete numbered replay is displayed in \cref{fig:reachable} and listed coordinate-by-coordinate in \cref{tab:sequence}. Here the boiling point is the supremum of the temperatures of all finite positions; the theorem gives a lower bound, not a determination of that supremum. The role of $B$ is computational: the two isolated cells in $B'$ have no moves and do not alter the game value. To our knowledge, after checking the published literature through August 12, 2026, this is the first reported Domineering temperature above $2$. That is a qualified priority statement, not a claim that no earlier unpublished example exists. \section{Short-game values, stops, and cooling} \label{sec:background} We use the standard theory of finite partizan games \cite{Conway1976,BCG1982,Siegel2013}. A short game is written \[ G=\{G^L\mid G^R\}, \] where $G^L$ and $G^R$ range over the followers available respectively to Left and Right. The zero game has no options, and $*=\{0\mid0\}$. The Domineering value of a disjoint union is the disjunctive sum of the values of its components. For a finite region $P$, $\G(P)$ denotes the value of the game whose Left options are $\G(P\setminus v)$ for legal vertical dominoes $v$ and whose Right options are $\G(P\setminus h)$ for legal horizontal dominoes $h$, with $\G(\varnothing)=0$. The left and right stops are defined recursively by \begin{align*} \LS(G)&=G &&\text{if $G$ is a number}, &\LS(G)&=\max_{G^L}\RS(G^L) &&\text{otherwise},\\ \RS(G)&=G &&\text{if $G$ is a number}, &\RS(G)&=\min_{G^R}\LS(G^R) &&\text{otherwise}. \end{align*} We use the nonnegative-temperature convention: numbers and number-plus- infinitesimals have temperature $0$. For a number $x$, put $x_s=x$. For a nonnumber, preliminary cooling charges a tax $s$ to either player who moves: it subtracts $s$ after a Left move and adds $s$ after a Right move, \begin{equation} \widetilde G_s= \left\{(G^L)_s-s\,\middle|\,(G^R)_s+s\right\}. \label{eq:cooling} \end{equation} Call $G$ \emph{numberish} when $\LS(G)=\RS(G)$; equivalently, $G$ differs from a number only infinitesimally. The temperature $\temp(G)$ is the least $s\geq0$ at which the preliminary cooled game is numberish; cooling thereafter freezes the game to that common stop. The frozen number is the mean $\mean(G)$. Equivalent formulations use the intersection of the thermograph's left and right walls \cite{Siegel2013,HuntemannNowakowskiSantos2021}. For the elementary switch $\{a\mid b\}$ with numeric options $a>b$, the walls are $a-s$ and $b+s$, so \begin{equation} \temp(\{a\mid b\})=\frac{a-b}{2}, \qquad \mean(\{a\mid b\})=\frac{a+b}{2}. \label{eq:switch} \end{equation} The right option in \eqref{eq:mainvalue} is not a number but the infinitesimal perturbation $-2+*$. It nevertheless has temperature $0$ and mast $-2$, so the same two-wall calculation applies. \section{The connected value core} \label{sec:board} Coordinates are Cartesian: $(x,y)$ denotes the unit grid cell with lower-left corner $(x,y)$. Define \begin{align} B=\{&\cell00,\cell01,\cell02, \cell12,\cell15,\cell17, \cell22,\cell25,\cell26,\cell27,\notag\\ &\cell32,\cell33,\cell34,\cell35,\cell36, \cell44,\cell45,\cell46,\notag\\ &\cell52,\cell53,\cell54, \cell62,\cell72, \cell80,\cell81,\cell82\}. \label{eq:board} \end{align} Let \begin{equation} C=(3,5),\qquad U=(3,6),\qquad W=(4,5). \label{eq:crossingcells} \end{equation} The vertical move $C$--$U$ and the horizontal move $C$--$W$ cross at $C$. They are the unique moves attaining the two canonical options. Adjacency inspection shows that $B$ is connected. Enumerating adjacent cell pairs gives $14$ vertical and $14$ horizontal placements. Those elementary geometric statements are also asserted before the value calculation begins. \begin{figure}[H] \centering \begin{tikzpicture}[scale=0.42,line join=round] \foreach \x/\y in { 0/0,0/1,0/2, 1/2,1/5,1/7, 2/2,2/5,2/6,2/7, 3/2,3/3,3/4,3/5,3/6, 4/4,4/5,4/6, 5/2,5/3,5/4, 6/2,7/2, 8/0,8/1,8/2} {\filldraw[fill=paIvory,draw=paGrid,line width=.55pt] (\x,\y) rectangle ++(1,1);} \filldraw[fill=paGold!32,draw=paGrid,line width=.55pt] (3,5) rectangle ++(1,1); \filldraw[fill=paCyan!22,draw=paGrid,line width=.55pt] (3,6) rectangle ++(1,1); \filldraw[fill=paCoral!20,draw=paGrid,line width=.55pt] (4,5) rectangle ++(1,1); \draw[paCyan,line width=3.0pt,rounded corners=2pt] (3.15,5.08) rectangle (3.85,6.92); \draw[paCoral,line width=3.0pt,rounded corners=2pt] (3.08,5.15) rectangle (4.92,5.85); \node[font=\sffamily\bfseries\small,text=paInk,fill=paGold!70, circle,inner sep=1.2pt] at (3.5,5.5) {C}; \node[font=\sffamily\bfseries\small,text=paInk] at (3.5,6.5) {U}; \node[font=\sffamily\bfseries\small,text=paInk] at (4.5,5.5) {W}; \draw[-{Stealth[length=2.2mm]},paCyan,line width=1.15pt] (3.5,8.12) -- (3.5,6.94); \node[anchor=south,align=center,font=\sffamily\small,text=paCyan] at (3.5,8.16) {Left's unique canonical move}; \draw[-{Stealth[length=2.2mm]},paCoral,line width=1.15pt] (6.34,5.62) -- (4.88,5.55); \node[anchor=west,align=left,font=\sffamily\small,text=paCoral] at (6.38,5.72) {Right's unique\\canonical move}; \foreach \x in {0,...,8} \node[font=\scriptsize,text=paGrid] at (\x+.5,-.28) {\x}; \foreach \y in {0,...,7} \node[font=\scriptsize,text=paGrid] at (-.28,\y+.5) {\y}; \end{tikzpicture} \caption{The exact $26$-cell value core $B$ from \cref{eq:board}; it is not itself rectangle-reachable. Cyan marks Left's move $C$--$U$, coral marks Right's move $C$--$W$, and gold marks their shared cell $C$. The verifier uses the coordinate list, not the image.} \label{fig:board} \end{figure} \section{Exact value certificate} \label{sec:certificate} For a legal move $m$, write $B-m$ for the cells remaining after its two cells are covered. The central certificate is the following exact finite statement. \begin{proposition}[Raw-option certificate] \label{prop:options} The crossing followers satisfy \begin{equation} \G(B-(C\text{--}U))=\frac{17}{8}, \qquad \G(B-(C\text{--}W))=-2+*. \label{eq:followers} \end{equation} For every legal vertical move $v$, \begin{equation} \G(B-v)\leq\frac{17}{8}, \label{eq:leftbound} \end{equation} with equality only for $v=C$--$U$. For every legal horizontal move $h$, \begin{equation} -2+*\leq\G(B-h), \label{eq:rightbound} \end{equation} with equality only for $h=C$--$W$. \end{proposition} The order in \cref{eq:leftbound,eq:rightbound} is Conway's partial order on short games, not a comparison of numerical approximations. Thus the other $13$ Left options and other $13$ Right options are dominated; the marked options themselves attain equality and are retained. After the move $C$--$U$, the board separates into components of sizes $19$ and $5$, with respective values $17/8$ and $0$. After $C$--$W$, it separates into components of sizes $17$ and $7$, with respective values $0$ and $-2+*$. The component sums give \eqref{eq:followers}. Each component value, and each comparison against every raw follower, is computed from the same recursive game definition rather than inferred from the drawing. \begin{proof}[Proof of \cref{prop:options}] Index the $26$ cells and represent every subposition by its $26$-bit mask. For a mask $S$, the verifier evaluates the well-founded recursion \begin{align*} \mathcal L_S&=\{F(S\setminus v):v\text{ is a legal vertical domino in }S\},\\ \mathcal R_S&=\{F(S\setminus h):h\text{ is a legal horizontal domino in }S\},\\ F(S)&=\{\mathcal L_S\mid\mathcal R_S\}. \end{align*} Each child has two fewer cells, so memoization merely shares repeated subtrees and does not change the definition. Game comparison uses the standard recursive criterion \[ X\leq Y \quad\Longleftrightarrow\quad \bigl(\nexists X^L:\;Y\leq X^L\bigr) \ \text{and}\ \bigl(\nexists Y^R:\;Y^R\leq X\bigr), \] with equality defined by the two opposite comparisons. The target games $17/8$, $*$, $-2+*$, and $\{17/8\mid-2+*\}$ are constructed exactly in the same short-game representation. The verifier first asserts the coordinate count, connectedness, and the $14+14$ legal-move count. It then evaluates $F(B)$, the two marked followers, and every one of the $28$ raw followers. The assertions are exactly \cref{eq:followers,eq:leftbound,eq:rightbound}, including uniqueness of equality. The calculation uses integer masks and rational numerators and denominators only. The independently structured checks summarized in \cref{sec:verification} reproduce the same comparisons and component values. \end{proof} \begin{proof}[Proof of \cref{prop:core}] The coordinate assertions and legal-move counts are direct. By \cref{prop:options}, removing dominated options from the raw game tree leaves exactly \[ \G(B)=\left\{\frac{17}{8}\,\middle|\,-2+*\right\}, \] which the canonical-form checker also confirms is canonical. The left option is the number $17/8$, while the right option is numberish with temperature $0$ and mean $-2$. For nonnegative cooling taxes their relevant thermograph masts are therefore $17/8$ and $-2$. Under cooling by $s$, the two walls are \[ \frac{17}{8}-s \qquad\text{and}\qquad -2+s. \] They meet when \[ \frac{17}{8}-s=-2+s, \] namely at $s=33/16$, at height $1/16$. This proves \eqref{eq:maintemp}. \end{proof} \begin{figure}[!htbp] \centering \begin{tikzpicture}[x=4.25cm,y=1.30cm,>=Stealth] \draw[->,line width=.7pt,text=paInk] (-.03,-2.28) -- (2.34,-2.28) node[below right,font=\small] {cooling tax $s$}; \draw[->,line width=.7pt,text=paInk] (0,-2.35) -- (0,2.46) node[above,font=\small] {stop}; \foreach \y/\lab in {-2/{-2},0/{0},2.125/{17/8}} {\draw[paGrid] (-.015,\y) -- (.015,\y); \node[anchor=east,font=\scriptsize] at (-.025,\y) {$\lab$};} \draw[densely dashed,paGrid] (2,-2.28) -- (2,.125); \draw[densely dashed,paGold!85!black] (2.0625,-2.28) -- (2.0625,.0625); \draw[paCyan,line width=2.3pt] (0,2.125) -- (2.0625,.0625); \draw[paCoral,line width=2.3pt] (0,-2) -- (2.0625,.0625); \draw[paGold!85!black,line width=2.3pt] (2.0625,.0625) -- (2.30,.0625); \fill[paGold!90!black] (2.0625,.0625) circle (.025); \node[font=\scriptsize,text=paCyan,anchor=south west] at (.18,1.95) {$17/8-s$}; \node[font=\scriptsize,text=paCoral,anchor=north west] at (.18,-1.78) {$-2+s$}; \node[font=\scriptsize,anchor=north east,text=paGrid] at (1.995,-2.34) {$2$}; \node[font=\scriptsize,anchor=north west,text=paGold!65!black] at (2.070,-2.34) {$33/16$}; \node[font=\scriptsize,anchor=south west,text=paGold!60!black] at (2.08,.10) {mean $1/16$}; \end{tikzpicture} \caption{The exact thermograph of $\{17/8\mid-2+*\}$. The infinitesimal $*$ distinguishes the exact right option from the number $-2$, but the right option's thermograph has the same mast $-2$; the infinitesimal therefore does not alter the two outer walls or the temperature. The plot is drawn with cooling tax on the horizontal axis and stop value on the vertical axis, transposed from the conventional thermograph orientation. The walls meet at $s=33/16$, strictly to the right of the conjectured ceiling $2$.} \label{fig:thermograph} \end{figure} \section{The rectangle-reachable realization} \label{sec:reachability} \begin{proof}[Proof of \cref{thm:main}] Color a cell $(x,y)$ black when $x+y$ is even and white otherwise. Every domino covers one cell of each color. The board $B$ has $14$ cells of one color and $12$ of the other, while a rectangle has color imbalance $0$ or $1$ in absolute value. Therefore the complement of $B$ in any containing rectangle cannot be tiled by played dominoes. In particular, $B$ itself is not a remainder reachable from a rectangular start. The construction in \cref{thm:main} is value-neutral. Translation preserves adjacency and game value. Translate $B$ two units to the right and adjoin the isolated cells $(0,1)$ and $(1,4)$. Each single cell has game value $0$, and the three components are mutually nonadjacent. Hence \begin{equation} \G(B')=\G(B)+0+0=\G(B). \label{eq:reachablevalue} \end{equation} The sequence in \cref{tab:sequence} covers the other $60$ cells by $15$ vertical and $15$ horizontal dominoes. Direct replay verifies at every step that the specified domino lies within the rectangle, occupies two adjacent uncovered cells, and has the required orientation. Its final uncovered set is exactly $B'$, proving rectangle reachability. Equation \eqref{eq:reachablevalue} and the value and thermograph calculation in \cref{prop:core} give the asserted game, temperature, and mean. The boiling-point conclusion follows from its definition as a supremum over finite positions. \end{proof} \begin{figure}[!htbp] \centering \begin{tikzpicture}[scale=.64,line join=round] \foreach \x in {1,...,10} \draw[paGrid!18] (\x,0)--(\x,8); \foreach \y in {1,...,7} \draw[paGrid!18] (0,\y)--(11,\y); % The complete alternating play. Odd moves are Left/vertical; % even moves are Right/horizontal. \foreach \n/\x/\y in { 1/0/2,3/0/4,5/0/6,7/1/1,9/1/5, 11/2/4,13/3/0,15/3/3,17/4/0,19/4/3, 21/5/0,23/6/0,25/6/2,27/7/0,29/8/3} {\filldraw[fill=paCyan!48,draw=paCyan,line width=.9pt, rounded corners=1.4pt] (\x+.06,\y+.06) rectangle (\x+.94,\y+1.94); \node[font=\sffamily\bfseries\scriptsize,text=paInk] at (\x+.5,\y+1) {\n};} \foreach \n/\x/\y in { 2/0/0,4/1/3,6/1/7,8/2/6,10/5/7, 12/7/5,14/7/6,16/7/7,18/8/0,20/8/1, 22/9/3,24/9/4,26/9/5,28/9/6,30/9/7} {\filldraw[fill=paCoral!43,draw=paCoral,line width=.9pt, rounded corners=1.4pt] (\x+.06,\y+.06) rectangle (\x+1.94,\y+.94); \node[font=\sffamily\bfseries\scriptsize,text=paInk] at (\x+1,\y+.5) {\n};} % The cells left after move 30. \foreach \x/\y in { 2/0,2/1,2/2, 3/2,3/5,3/7, 4/2,4/5,4/6,4/7, 5/2,5/3,5/4,5/5,5/6, 6/4,6/5,6/6, 7/2,7/3,7/4, 8/2,9/2, 10/0,10/1,10/2} {\filldraw[fill=paIvory,draw=paGrid,line width=.55pt] (\x,\y) rectangle ++(1,1);} \foreach \x/\y in {0/1,1/4} {\filldraw[fill=paGold!35,draw=paGold!75!black,line width=1pt] (\x,\y) rectangle ++(1,1); \node[font=\bfseries\small,text=paGold!55!black] at (\x+.5,\y+.5) {0};} \draw[paGrid!70,line width=.85pt] (0,0) rectangle (11,8); \foreach \x in {0,...,10} \node[font=\tiny,text=paGrid] at (\x+.5,-.22) {\x}; \foreach \y in {0,...,7} \node[font=\tiny,text=paGrid] at (-.22,\y+.5) {\y}; \end{tikzpicture} \caption{The complete rectangle replay. Every colored domino is an actual move, numbered in play order: odd cyan dominoes are Left/vertical moves and even coral dominoes are Right/horizontal moves. The white and gold cells are the exact $28$-cell remainder $B'$ after move $30$; the two gold singletons have game value $0$. The coordinate list in \cref{tab:sequence}, not this rendering, is the formal certificate.} \label{fig:reachable} \end{figure} \section{Exact computation and independent checks} \label{sec:verification} The finite certificate is supported by five routes. \begin{enumerate} \item The primary standalone verifier constructs the raw short-game DAG, performs exact Conway-order comparison, and checks the full value, all $28$ raw-option comparisons and their equality cases, the two marked follower totals, both component-size lists, the temperature, and the mean. It visits $17{,}673$ board masks and interns $15{,}774$ raw game forms. \item An archived earlier engine provides a separately structured replay of the value and thermograph certificates using its own canonicalization and thermograph routines. \item A newly written canonical-game checker uses domination and reversible-option bypass together with an exact piecewise-linear thermograph engine. It confirms the geometry, symmetries, option uniqueness, four component values, stops, mean, and temperature. This run visits $47{,}419$ masks and interns $11{,}061$ game forms. \item A zero-thermography cross-check proves the value claims by ordinary win/loss minimax on difference games. In particular it verifies that $B+\{2+*\mid-17/8\}$ is a second-player win, which is equivalent to \eqref{eq:mainvalue}, since a short game equals $0$ exactly when it is a second-player win. This route uses neither game-order comparison, canonicalization, nor thermographs and records $1{,}039{,}152$ cached states. \item A Lean development defines the finite normal-play Domineering model, derives both players' move masks from the coordinate boards, and proves a sound checker for balanced difference-game certificates. Ordinary kernel reduction validates all $995{,}069$ certificate states, arranged in $128$ balanced subtrees and $32$ proof modules. Lean then proves the complete game equivalence with the explicit target, the target walls' first intersection at $33/16$ and mean $1/16$, the $30$-move rectangle replay, and the final rectangle-reachable existential theorem in the \texttt{HasValueTemperature} formulation explained below. Python output and hashes are not theorem evidence in this route \cite{MazurFormalization2026}. The recorded dependency audit reports only \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}; the checked development uses no \texttt{sorry}, custom mathematical axiom, or native-decision shortcut. \end{enumerate} The minimax checker and Lean development are structurally separate from the discovery engines. All routes were nevertheless coordinated in the same author-directed audit workflow. The Python checks ran in the same local environment, while the retained Lean kernel build ran on the clean frozen source host. Their agreement is strong algorithmic evidence but is not the same as unrelated external replication. The rectangle-reachability script is a separate exact replay of the sequence in \cref{tab:sequence}. The Lean theorem uses the deliberately narrow predicate \texttt{HasValueTemperature}: it exhibits an explicit thermographed representative game-equivalent to the Domineering board. The development proves that exact equivalence and that representative's exact thermograph; it does not yet prove a general theorem that thermographs are invariant under every game-equivalence presentation. It also does not separately formalize the checkerboard unreachability of the value core $B$. All scripts use only Python's standard library. The final manuscript replays were run under Python 3.13.13. In the table below the first two files are relative to the artifact bundle root, and the last three are relative to \texttt{external\_audit\_2026-08-12/}. Their SHA-256 digests are: \begin{center} \small \begin{tabular}{@{}>{\ttfamily}p{.43\textwidth}>{\ttfamily\scriptsize}p{.49\textwidth}@{}} \toprule file & SHA-256 \\ \midrule \normalfont\texttt{verify\_counterexample\_v11.py} & 6a6aaa8e0fa54e3c3cd3e57aad375a52\newline bf3a86f4872f5fbcb00eb0df6411e2a6 \\ \normalfont\texttt{counterexample\_certificate\_v11.json} & 977be959a474b80e407bb894057c36d8\newline c84132bb7ba0047442a77b64259071df \\ \normalfont\texttt{independent\_cgt\_audit.py} & 39833ddc79c93ad4b345c44e3bca16d4\newline f5f711c507153cd16db9d4ec572a6e6a \\ \normalfont\texttt{minimax\_cross\_check.py} & 65e8758c9608af4f172fa3c5a64499f9\newline eca3e147c94aada9e391e913e2188f35 \\ \normalfont\texttt{rectangle\_reachability.py} & 2bbdf2cbbb4c77347a5a3b8b80bb7014\newline a441449823bf27b9f8a2d63b86b0e31e \\ \bottomrule \end{tabular} \end{center} The digests identify the audited files; they do not by themselves establish correctness. Exact saved outputs accompany the programs. From the artifact bundle root, the principal routes are reproduced with \begin{lstlisting}[basicstyle=\ttfamily\scriptsize,frame=single] ./RUN_ALL.sh cd external_audit_2026-08-12 python3 independent_cgt_audit.py python3 minimax_cross_check.py python3 rectangle_reachability.py \end{lstlisting} The frozen Lean sources are identified by commit \nolinkurl{9edd1d307a62bcd1b59c4450c8675fcdbb5a3ebe}, with the final declaration \nolinkurl{Domineering.berlekamp_conjecture_false} in \nolinkurl{Domineering/ReachableCounterexampleValue.lean} \cite{MazurFormalization2026}. The complete public bundle---including the Python certificates, saved outputs, matching manuscript source, Lean project, generated certificate modules, toolchain pin, and Mathlib manifest, but excluding build products---is available from the \href{https://proofatlas.ai/papers/berlekamp-domineering-temperature-counterexample-formalized/BERLEKAMP_DOMINEERING_TEMPERATURE_COUNTEREXAMPLE_PUBLIC_PACKET_2026-08-14.zip}{ProofAtlas artifact download}. \section{Historical context and consequences} \label{sec:history} Drummond-Cole's 2004 example has value $\{2+*\mid-2+*\}$ and temperature $2$, establishing that the proposed bound could not be lowered \cite{DrummondCole2004}. Shankar and Sridharan then searched more than ten billion positions fitting in $5\times6$, $4\times8$, $3\times10$, and $2\times16$ boards. They reported $219$ new temperatures, $26$ above $3/2$, and none above $2$ \cite{ShankarSridharan2005}. Uiterwijk and Barton computed exact canonical values for all connected positions through $15$ cells, finding one temperature-$2$ position and none hotter \cite{UiterwijkBarton2015}. General methods based on thermographic confusion intervals later gave uniform bounds for restricted Domineering families but did not prove the universal bound $2$ \cite{HuntemannNowakowskiSantos2021}. Most recently, Huntemann and Maciosowski exhaustively searched arbitrary subgrids on $5\times5$ and $5\times6$ boards, searched $6\times6$ positions with at most $20$ empty cells, and used a genetic search on $7\times7$. They also proved an infinite temperature-$2$ family and reported no position above $2$ \cite{HuntemannMaciosowski2026}. Their arbitrary-subgrid convention includes regions not reachable from rectangle play, such as the value core used here. That $26$-cell core has a $9\times8$ bounding box, outside the exhaustive regimes just listed. The counterexample changes the central question from proving a ceiling of $2$ to determining, or bounding, the true boiling point. It also raises structural questions: whether the crossing-option mechanism here extends to an infinite hotter family, whether temperatures substantially above $33/16$ occur, and what the smallest connected or rectangle-reachable example is. The present computation establishes none of those stronger claims. \appendix \section{An explicit rectangle-play certificate} \label{app:sequence} \Cref{tab:sequence} lists the complete alternating play from the full $11\times8$ board. A notation $(x,y)$--$(x',y')$ means the domino covering those two cells. Each row gives one Left move followed by one Right move. \begin{table}[H] \centering \scriptsize \begin{tabular}{@{}c@{\quad}ll@{\hspace{1.8em}}c@{\quad}ll@{}} \toprule round & Left: V & Right: H & round & Left: V & Right: H \\ \midrule 1 & $(0,2)$--$(0,3)$ & $(0,0)$--$(1,0)$ & 9 & $(4,0)$--$(4,1)$ & $(8,0)$--$(9,0)$ \\ 2 & $(0,4)$--$(0,5)$ & $(1,3)$--$(2,3)$ & 10 & $(4,3)$--$(4,4)$ & $(8,1)$--$(9,1)$ \\ 3 & $(0,6)$--$(0,7)$ & $(1,7)$--$(2,7)$ & 11 & $(5,0)$--$(5,1)$ & $(9,3)$--$(10,3)$ \\ 4 & $(1,1)$--$(1,2)$ & $(2,6)$--$(3,6)$ & 12 & $(6,0)$--$(6,1)$ & $(9,4)$--$(10,4)$ \\ 5 & $(1,5)$--$(1,6)$ & $(5,7)$--$(6,7)$ & 13 & $(6,2)$--$(6,3)$ & $(9,5)$--$(10,5)$ \\ 6 & $(2,4)$--$(2,5)$ & $(7,5)$--$(8,5)$ & 14 & $(7,0)$--$(7,1)$ & $(9,6)$--$(10,6)$ \\ 7 & $(3,0)$--$(3,1)$ & $(7,6)$--$(8,6)$ & 15 & $(8,3)$--$(8,4)$ & $(9,7)$--$(10,7)$ \\ 8 & $(3,3)$--$(3,4)$ & $(7,7)$--$(8,7)$ & & & \\ \bottomrule \end{tabular} \caption{A $30$-ply legal sequence whose uncovered cells are exactly $B'$. Left moves first and the orientations alternate.} \label{tab:sequence} \end{table} \clearpage \section{Scope, artifacts, and project context} \label{app:scope} The certificates concern the exact coordinate sets, not rendered images; the TikZ diagrams are illustrative. The companion bundle contains the primary verifier and output, the JSON certificate, archived replays, both algorithmically independent audits and outputs, and the reachability checker. The companion Lean source fixes the game model, proved certificate checker, complete generated certificate, target thermograph, and final theorem at the commit cited above. The public \href{https://www.proofatlas.ai/collaboration/berlekamp-domineering-temperature-conjecture/} {ProofAtlas.ai collaboration record} collects the problem context and evidence status, and the \href{https://proofatlas.ai/papers/berlekamp-domineering-temperature-counterexample-formalized/BERLEKAMP_DOMINEERING_TEMPERATURE_COUNTEREXAMPLE_PUBLIC_PACKET_2026-08-14.zip}{downloadable companion bundle} supplies the exact source named in the verification section. A ProofAtlas listing is a route to evidence and provenance, not a claim of journal acceptance or independent replication. \section*{Acknowledgments} The author thanks the developers of Lean and Mathlib, the developers of the combinatorial-game systems, and the authors of the primary sources used here. Algorithmically independent audits supplied complementary checks of the finite computation. \begingroup \small \raggedright \setlength{\itemsep}{0pt} \setlength{\parsep}{0pt} \begin{thebibliography}{99} \bibitem{BCG1982} E.~R. Berlekamp, J.~H. Conway, and R.~K. Guy, \emph{Winning Ways for Your Mathematical Plays}, vol.~1, Academic Press, London, 1982. \bibitem{Berlekamp1988} E.~R. Berlekamp, Blockbusting and Domineering, \emph{J. Combin. Theory Ser. A} \textbf{49} (1988), no.~1, 67--116, \href{https://doi.org/10.1016/0097-3165(88)90028-3}{doi:10.1016/0097-3165(88)90028-3}. \bibitem{Conway1976} J.~H. Conway, \emph{On Numbers and Games}, Academic Press, London, 1976. \bibitem{DrummondCole2004} G.~C. Drummond-Cole, Temperature two in Domineering, unpublished note, 2004, \url{https://drummondcole.com/gabriel/academic/2star.pdf}. \bibitem{Gardner1974} M.~Gardner, Mathematical games: Cram, crosscram and quadraphage: new games having elusive winning strategies, \emph{Scientific American} \textbf{230} (1974), no.~2, 106--108, \href{https://doi.org/10.1038/scientificamerican0274-106}{doi:10.1038/scientificamerican0274-106}. \bibitem{HuntemannMaciosowski2026} S.~Huntemann and T.~Maciosowski, High temperature Domineering positions, \emph{Integers} \textbf{26} (2026), Paper G1, \href{https://doi.org/10.5281/zenodo.18154236}{doi:10.5281/zenodo.18154236}. \bibitem{HuntemannNowakowskiSantos2021} S.~Huntemann, R.~J. Nowakowski, and C.~P. dos Santos, Bounding game temperature using confusion intervals, \emph{Theoret. Comput. Sci.} \textbf{855} (2021), 43--60, \href{https://doi.org/10.1016/j.tcs.2020.11.015}{doi:10.1016/j.tcs.2020.11.015}. \bibitem{MazurFormalization2026} L.~Mazur, Lean formalization of the Domineering temperature counterexample, frozen source commit \nolinkurl{9edd1d307a62bcd1b59c4450c8675fcdbb5a3ebe}, Lean \texttt{v4.30.0-rc2}, Mathlib commit \nolinkurl{5450b53e5ddc75d46418fabb605edbf36bd0beb6}, companion artifact, 2026, \href{https://proofatlas.ai/papers/berlekamp-domineering-temperature-counterexample-formalized/BERLEKAMP_DOMINEERING_TEMPERATURE_COUNTEREXAMPLE_PUBLIC_PACKET_2026-08-14.zip}{ProofAtlas public artifact bundle}. \bibitem{ShankarSridharan2005} A.~Shankar and M.~Sridharan, New temperatures in Domineering, \emph{Integers} \textbf{5} (2005), Paper G04, \href{https://doi.org/10.5281/zenodo.7727185}{doi:10.5281/zenodo.7727185}. \bibitem{Siegel2013} A.~N. Siegel, \emph{Combinatorial Game Theory}, Graduate Studies in Mathematics, vol.~146, American Mathematical Society, Providence, RI, 2013. \bibitem{UiterwijkBarton2015} J.~W.~H.~M. Uiterwijk and M.~Barton, New results for Domineering from combinatorial game theory endgame databases, \emph{Theoret. Comput. Sci.} \textbf{592} (2015), 72--86, \href{https://doi.org/10.1016/j.tcs.2015.05.017}{doi:10.1016/j.tcs.2015.05.017}. \end{thebibliography} \endgroup \end{document}