## The counterexample

Domineering is a partizan placement game: Left places vertical dominoes and
Right places horizontal dominoes on a finite region. A long-standing
conjecture attributed to Berlekamp asserted that every finite Domineering
position has temperature at most `2`.

Lech Mazur's manuscript gives an exact counterexample. Lean checks the
board–target game equivalence, the explicit target's thermograph, the complete
30-move rectangle replay, and the resulting existential theorem through the
development's narrow value-and-temperature witness. The stronger witness is
a 28-cell position `B'` reached by an explicit alternating sequence of 30
legal moves from an `11 × 8` rectangle. Its exact game is

> `G(B') = { 17/8 | -2 + * }`,

so, in the nonnegative-temperature convention used in the paper,

> `t(G(B')) = 33/16 = 2.0625 > 2`, with mean `1/16`.

The [Berlekamp collaboration page](/collaboration/berlekamp-domineering-temperature-conjecture/)
retains the broader research frontier and open follow-up tasks.

## What the infographic shows

The infographic displays the actual `11 × 8` replay. Odd-numbered cyan
dominoes are Left's 15 vertical moves; even-numbered coral dominoes are
Right's 15 horizontal moves. The white cells and two gold cells are exactly
the 28 cells left after move 30. Thus the graphic shows the moves as well as
the final position; the coordinate table in the paper and Lean theorem are
the certificates.

## The 26-cell core and the repair

The connected 26-cell core `B` has the same exact value, but it has
checkerboard imbalance `14 − 12 = 2`. A rectangular board has imbalance at
most one, while every played domino removes one cell of each color. Therefore
`B` cannot itself occur as the remainder of play from any rectangle.

The repaired position translates `B` two cells to the right and adds the
single cells `(0,1)` and `(1,4)`. Both are isolated from every other remaining
cell, so neither player can cover either one with a domino. Each is a zero
component, and consequently

> `G(B') = G(B) + 0 + 0 = G(B)`.

The explicit 30-move replay proves the stronger rectangle-reachable statement.

## Lean-checked scope

The frozen Lean source is identified by commit
`9edd1d307a62bcd1b59c4450c8675fcdbb5a3ebe`, Lean `v4.30.0-rc2`, and Mathlib
commit `5450b53e5ddc75d46418fabb605edbf36bd0beb6`. The final declaration is
`Domineering.berlekamp_conjecture_false` in
`Domineering/ReachableCounterexampleValue.lean`.

The machine-readable ProofAtlas evidence record is
`artifact.berlekamp-domineering-temperature-counterexample.reachable.v001`.
It is also included in the public packet as
`formalization/CHECKED_ARTIFACT.json`.

Lean checks:

- the complete 30-move alternating replay from the rectangle;
- the board's exact equivalence to `{17/8 | -2+*}`;
- all 995,069 states of the complete difference-game certificate through a
  proved checker and ordinary kernel reduction;
- the explicit target's thermograph, temperature `33/16`, and mean `1/16`;
  and
- the resulting rectangle-reachable existential statement.

The development contains no `sorry`, custom mathematical axiom, or
native-decision shortcut. Python output and file hashes are not theorem
evidence.

The exact theorem uses the deliberately narrow predicate
`HasValueTemperature`: it exhibits a thermographed representative
game-equivalent to the board. The development proves that equality and the
representative's thermograph, but does not yet include a general theorem that
thermographs are invariant under every game-equivalence presentation. It also
does not formalize the one-cell deletion audit or separately formalize the
checkerboard obstruction for raw `B`.

## Download and reproduce

The [August 14 public artifact bundle](/papers/berlekamp-domineering-temperature-counterexample/BERLEKAMP_DOMINEERING_TEMPERATURE_COUNTEREXAMPLE_PUBLIC_PACKET_2026-08-14.zip)
contains the matching paper PDF and LaTeX source, the complete Lean source and
generated certificate modules, Python verifiers and saved outputs, exact
evidence tables, the final SVG and PNG infographic, toolchain pins, and a
whole-bundle `MANIFEST.sha256`.

From the bundle root:

```bash
sha256sum -c MANIFEST.sha256
./RUN_ALL.sh
cd external_audit_2026-08-12
python3 independent_cgt_audit.py
python3 minimax_cross_check.py
python3 rectangle_reachability.py
```

To check the final Lean module from source, use the pinned toolchain and run
`lake env lean Domineering/ReachableCounterexampleValue.lean` inside
`formalization/`. The full generated certificate is included, but compilation
is a substantial resource job; build products are deliberately omitted.

## Additional exact evidence

The non-Lean routes separately rederive the canonical game and thermograph,
check the raw-option inequalities and their unique equality cases, replay the
rectangle sequence, and prove the value equality again using ordinary
win/loss minimax on a 1,039,152-state difference game.

For every one-cell deletion from the 26-cell core, the exact computed
temperature is below `2`; the maximum is `15/8`, attained at two cells. This
is deletion-local evidence only. It does not prove global size minimality,
uniqueness, or any minimality statement for the 28-cell reachable witness.

## Review and priority boundary

The supplied evidence reports successful replays of the bundled Python routes.
The checked-artifact record retains the successful cached Lean build transcript
from the clean frozen source host, together with the no-sorry result, axiom
profile, source commit, toolchain pin, and dependency-lock digest. ProofAtlas
has matched the selected public files to the supplied manifest, but has not
rerun the substantial Lean build for this page update. These checks were
coordinated in the same author-directed workflow; they are not unrelated
external replication or independent specialist peer review.

ProofAtlas does not award historical priority here. The manuscript reports
that the literature checked through August 12, 2026 contains no earlier
published Domineering position above temperature `2`. A dedicated prior-art
review and a reproduction in an unrelated system remain worthwhile. It also
remains open how high finite Domineering temperatures can be and whether
there is an infinite family above `2`.

Publication here records the exact supplied paper, visual, public bundle, and
scoped Lean evidence. It does not substitute for unrelated reproduction,
specialist peer review, or an independent historical-priority assessment.