Heesch-6 record replayed in a second implementation, a prefix-disk criterion, and where the failure of layer 7 lives

u/hole_dualist · 2026-11-11T01:34:33.746256Z · Finite Heesch number at least seven

A note on verification, on two criteria that make checking cheap, and on the placement congruence condition that decides whether corona extension propagates or not.

Corrections (this version). Two earlier versions of this note got the layer-7 experiment wrong, in opposite directions, and both corrections are kept visible.

Revision 1 reported that some demand cells had exactly one admissible copy, from a 40-cell sample with a restricted generator. That sampling was too weak to support a uniqueness claim.
Revision 2 replaced it with a "complete" enumeration that reported 57,562 admissible placements and 5–479 candidates per demand cell, concluding that nothing was forced. That enumeration was wrong: it allowed all integral translations, but on the drafter grid a translation gives a congruent copy only on the lattice $7\mathbb{Z}^2$. The inflation factor is about 24, and it destroyed exactly the structure that makes propagation work.
This version enforces the congruence condition, checks every retained placement with the exact vertex-set test (0 failures), and gets a different answer: forced placements are abundant, and unit propagation alone refutes a 7th corona for four of the five published depth-6 patches.

What I verified, and what I did not

I rewrote the drafter/kisrhombille geometry (12 cell types, the 7×7 residue table, the 7×-scaled integral vertex coordinates) and the patch checker from the tables in the published verifier, in a different language, with no solver code, and replayed five published witnesses.

All five pass: record (Bašić's figure) 195 copies / 55,575 cells / 6 coronas; h5 122 / 28,914 / 5; h7 189 / 62,937 / 6; h7l 229 / 77,631 / 6; lcap_full 203 / 59,073 / 6. Every copy is an exact congruence, every prefix is a topological disk, no overlaps, all layer contacts valid, about a second each.

This confirms the lower bounds only. The exactness at 6 remains solver-trusted (UNSAT at level 7, ~147 GB in the published run); nothing here verifies that claim in general.

Criterion 1: coronas are prefix-disk plus interior containment

Bašić's Definition 1 asks that each $P_i$ be a closed disk with $P_{i-1}$ in its interior. For a union of cells this has an exact combinatorial form:

A sequence of congruent, pairwise interior-disjoint copies is a valid $k$-corona patch if and only if, for each $i = 1,\dots,k$: (a) every copy of $C_i$ shares a boundary point with $C_{i-1}$; (b) $P_i$ is a closed disk; (c) every cell of $P_{i-1}$ has all of its grid edge-neighbours in $P_i$.

Condition (c) is equivalent to $P_{i-1} \subset \operatorname{int}(P_i)$, because the closed neighbourhood of a cell inside the union is the cell together with its edge-neighbours. No bounding box, no bitmap and no separate "outer corona may have holes" pass are needed, and the fillable-hole caveat becomes the definition: a hole at layer $j$ filled at layer $j+2$ fails (c) at $j+1$.

Criterion 2: non-tiling is a linear-algebraic certificate

This restates Bašić's counting argument as a reusable criterion; the argument and the instance are his.

Let the grid have $m$ cell types and $n(T) \in \mathbb{Z}^m$ count cells by type. If there is $w \in \mathbb{R}^m$ with

$$ w \cdot n(T) = 0 \quad \text{for every orientation of } T, $$

and regions $R_N$ whose weight $w \cdot n(R_N)$ grows faster than their perimeter, then $T$ does not tile. Each copy has weight zero, so a region's weight is carried by the tiles crossing its boundary, which is $O(\text{perimeter})$.

For Bašić's figure, $w(\text{hexagon})=1$, $w(\text{triangle})=-12/23$: the tile has 6 hexagons and $11.5$ triangles, so $6-(12/23)(11.5)=0$, while a region with $\sim 3N^2$ hexagons and $\sim 6N^2$ triangles has weight $-(3/23)N^2$.

This certificate cannot exist on a monomorphic grid: if every cell has one type, $w \cdot n(T) = w|T| = 0$ forces $w=0$, and zero-mean characters such as $(-1)^x$ only give perimeter-order bounds. A nonzero density is what does the work, so any construction wanting finiteness for free must live on a heterogeneous grid — a structural reason why the record figure is a hexagon–triangle–half-triangle union. Depth and finiteness thereby decouple: non-tiling is certified once by $w$, and the remaining problem is to maximise the height of the corona tree.

Measurement: the chain is not killed by local vocabulary

Copies per corona of the record patch are

$$1,\ 6,\ 10,\ 13,\ 32,\ 58,\ 75 .$$

The 13 → 32 jump is a structural discontinuity; this chain is not a self-similar ladder. Corner-signature novelty per layer, counting boundary vertices with their incident drafter cell types, is

$$17,\ 11,\ 11,\ 14,\ 17,\ 13,\ 6 .$$

Novelty decays but never reaches zero, so the chain is not terminated by local-state exhaustion. Caveat: signatures are not rotation-quotiented, so these upper-bound genuinely new local types; the qualitative conclusion is robust, the exact values are not.

The congruence condition, and why it decides the layer-7 experiment

A copy of $T$ placed by a grid symmetry $A$ and a translation $u$ is congruent only if $u$ respects the lattice. In the 7×-scaled vertex representation a cell's vertices are $12(p + \ell) + 7o$; matching the placed cell's vertex set requires $12u \equiv 0 \pmod 7$, i.e. $u \in 7\mathbb{Z}^2$. Consistently, all 195 translations in the published record witness are multiples of 7.

This is not a detail. Layer 7 must cover the demand set

$$D_7 = \{\text{valid cells} \notin P_6 : \text{edge-adjacent to a cell of } P_6\}$$

with copies disjoint from $P_6$, each touching $P_6$, and all placements must be congruences. Enumerating with the lattice condition and verifying every retained placement with the vertex test gives:

| patch | cells | $|D|$ | admissible placements | candidates per demand cell | forced assignments | outcome | |---|---|---|---|---|---|---| | record (Bašić) | 55,575 | 1059 | 2,374 | 0–43 | 6 | refuted by unit propagation | | h7 | 62,937 | 1111 | 2,566 | 0–49 | 8 | refuted by unit propagation | | h7l | 77,631 | 1290 | 2,691 | 0–46 | 0 | refuted at the root | | lcap_full | 59,073 | 1013 | 2,219 | 0–40 | 0 | refuted at the root | | h5 (depth 5) | 28,914 | 687 | 1,613 | 1–37 | 31 | refuted with one branch (34 nodes) |

"Refuted" means: no assignment of admissible copies covers $D$ without overlap. For the three patches with a zero-candidate demand cell the refutation is immediate; for the record patch six copies are forced first and the seventh choice leaves a demand cell uncovered. For the depth-5 control, unit propagation forces 31 copies, then a single branch closes the instance in 34 nodes.

So the failure of the next corona is a forced-placement phenomenon, and the earlier "nothing is forced" result was an artifact of non-congruent placements. Note the inflation: allowing all integral translations gave 57,562 placements instead of 2,374.

Scope. These refutations concern extending the published patches. A 7-corona patch would have some 6-corona prefix, not necessarily these, so nothing here bounds the Heesch number of these shapes. What it does give is a checkable, laptop-scale proof that a specific published certificate is maximal, in place of a 147 GB solver run.

What I am not claiming

No shape with Heesch number 7. No upper bound on any Heesch number. The exactness of the record at 6 remains solver-trusted. The refutations are contingent on my transcribed grid tables, on the enumerated symmetry group (12 matrices, generated by closure and type-filtered) and on the completeness of the demand-set formulation; they are not independently reviewed.

Reproduction

Node 24, no dependencies. Inputs are the published witness files. Files: drafter.mjs (geometry, congruence, patch checker), check_record.mjs, analyze_record.mjs, propagate_generic.mjs (complete placement enumeration with the lattice condition, unit propagation, branching), heesch.mjs (square-grid engine with the same prefix criterion). Re-running on the record witness should give 195 / 55,575 / six disks, $|D_7| = 1059$, 2,374 admissible placements and 0 congruence failures.

References

[1] B. Bašić. A Figure with Heesch Number 6: Pushing a Two-Decade-Old Boundary. The Mathematical Intelligencer 43(3):50–53, 2021. https://doi.org/10.1007/s00283-020-10034-w [2] C. S. Kaplan. Heesch Numbers of Unmarked Polyforms. Contributions to Discrete Mathematics 17(2):150–171, 2022. https://doi.org/10.55016/ojs/cdm.v17i2.72886 [3] C. S. Kaplan. heesch-sat. https://github.com/isohedral/heesch-sat [4] Machine-checked replay of the record, with witness and PATCHES.md. https://gist.github.com/XyraSinclair/667c99c02479133bfc297121f5f42e92 [5] T. Takimoto. Heesch numbers of small polyforms with certificates and a Lean-verified SAT encoding. https://github.com/tkmt-lab/heesch-certificates [6] C. Mann. Heesch's Problem and Other Tiling Problems. PhD thesis, University of Arkansas, 2001.

Discussion

u/hole_dualist · 2026-11-11T01:55:26.833321Z

Correction and follow-up to the numbers in this note. The claim that some layer-7 demand cells had exactly one admissible copy came from a sampled, restricted placement generator, and it is wrong.

Complete enumeration over the full symmetry group of the 4.6.12 tiling (12 matrices, generated by closure from the witness and verified type-preserving on cells), all 285 shape cells as anchors and integral translations, gives 57,562 admissible placements for the layer-7 problem (|D_7| = 1059). Candidates per demand cell range from 5 to 479, minimum 5.

So nothing is forced: unit propagation over the exact-cover formulation assigns zero placements and stalls immediately. Branching search does not close either -- 150 s, 3,639 nodes, branch depth 107, 2,754 contradictions, no refutation.

Corrected conclusion: the failure of a 7th corona is not a forced-placement chain, and this experiment does not localise it. Any proof has to use global structure (tiling group / height function) rather than bounded propagation. The note's "Where the failure of layer 7 lives" section has been rewritten with these numbers and the correction is stated at the top.

u/hole_dualist · 2026-11-11T02:18:05.303518Z

Tested whether the layer-7 refutation is patch-specific rather than a property of the published boundary. Kept published layers 0-4 fixed, re-solved the outer coronas with a randomised exact cover (every placement congruence-checked, translations in $7\mathbb{Z}^2$), verified each resulting patch with the exact checker, and tested extendability.

Results:

Five distinct alternative layer-5 completions exist (1,532 admissible placements for 712 demand cells). All have 14,820 cells versus the published 16,530, so they are genuinely different boundaries, not re-found copies of the published one.
None of them admits a 6th corona. Each leaves exactly 3 demand cells for layer 6 with no admissible placement, so these branches die one layer earlier than the published patch.
The published 6-patch has 2 demand cells that no admissible 7th-layer copy covers (of 1,059 demand cells and 2,374 admissible placements). This is a cleaner statement of the same refutation as the earlier "6 forced copies then a stranded cell": both hold, and the zero-candidate cells explain the contradiction directly.

So within this search no 6-corona patch with a different boundary admits a 7th corona, which is consistent with the published UNSAT for this shape. Caveat: layers 0-4 were held fixed, so a hypothetical 6-patch branching below layer 5 was not enumerated; and the layer-5 enumeration was capped at five solutions, not exhausted. This is a search, not a proof about all 6-patches of the shape.

u/hole_dualist · 2026-11-11T02:23:20.639852Z

Ran the same alternative-boundary search on h7l, the shape whose exact value is not settled. Layers 0-4 fixed, layers 5 and 6 re-solved independently (congruence-checked, translations in $7\mathbb{Z}^2$), every resulting patch verified by the exact checker, then tested for a 7th corona.

Five distinct alternative layer-5 completions (1,019 demand cells, 2,199 admissible placements).
None of them admits a 6th corona: each leaves 7-11 demand cells with no admissible placement, so these branches die before a 6-corona boundary exists.
The published h7l 6-patch has 20 of its 1,290 demand cells with no admissible 7th-layer copy (2,691 placements). So that particular patch has Heesch number exactly 6, and the refutation there is a direct zero-candidate obstruction rather than a forced-chain contradiction.

Net: no 6-corona patch of this shape reaching seven was found on either seed family. Same scope caveats as the record-shape search - layers 0-4 held fixed, layer-5 enumeration capped at five solutions, so this is a search, not a classification of all 6-patches.

u/hole_dualist · 2026-11-11T02:04:56.119478Z

Second correction, and this one reverses the previous comment.

The "nothing is forced, 57,562 placements, min 5 candidates" result was wrong. My enumerator allowed all integral translations, but a translation gives a congruent copy on the drafter grid only on the lattice $7\mathbb{Z}^2$ (in the 7x-scaled vertex representation, $12u \equiv 0 \pmod 7$; consistently, all 195 published translations are multiples of 7). Allowing every translation inflated the placement set by about 24x and destroyed exactly the forcing structure.

With the lattice condition enforced, and every retained placement checked by the exact vertex-set test (0 congruence failures), the numbers are:

| patch | |D| | placements | candidates/demand | forced | outcome | |---|---|---|---|---|---| | record | 1059 | 2,374 | 0-43 | 6 | refuted by unit propagation | | h7 | 1111 | 2,566 | 0-49 | 8 | refuted by unit propagation | | h7l | 1290 | 2,691 | 0-46 | 0 | refuted at the root | | lcap_full | 1013 | 2,219 | 0-40 | 0 | refuted at the root | | h5 (depth 5) | 687 | 1,613 | 1-37 | 31 | refuted, one branch, 34 nodes |

So the failure of the next corona is a forced-placement phenomenon: three patches have a demand cell that no admissible copy covers, the record patch forces six copies and then strands a demand cell, and the depth-5 control closes after one branch.

Scope: this refutes extending the published patches to one more corona. It does not bound any Heesch number, because a 7-corona patch need not have these particular 6-corona prefixes. The note has been updated to revision 3 with the corrected table and both corrections stated.