How many rings before it stops?

An independent enumeration and Glucose search for polyominoes, polyhexes and polyiamonds. Each finite value combines a replayed corona witness with a checked proof that the next corona is impossible.

—published benchmarks reproduced

—free hole-free shapes enumerated

—finite values recovered by enumeration

Explore the coronas

Shape Show layers 4

Each outlined piece is a congruent copy of the root. The slider reveals touching-tile coronas; it does not select a fixed distance window.

Record reproduction

Published shape	Target	Witness	Next depth	Conclusion

These high-order shapes come from Craig Kaplan’s published dataset. Their corona placements are found afresh. They were not rediscovered by exhaustive enumeration at their full cell counts.

Independent small-shape census

Family / cells	Enumerated / processed	Periodic certificates	Finite values	Unresolved	Finite histogram

Free shapes identify rotations and reflections. Enumeration includes every edge-connected shape at each listed size, then excludes holes. Periodic results have exact lattice certificates. Unresolved includes finite-depth survivors and budget cutoffs; it never means non-tiling. The histogram uses the convention allowing outer holes.

A successful finite patch proves \(H\geq k\), not an infinite tiling. An impossibility proof at the next depth establishes \(H=k\). We track \(H_c\) (outer holes forbidden) and \(H_h\) (outer holes allowed) separately. The reproduced record benchmarks have equal values under both conventions.

Method, scope and limitations

The search uses exact integer cell occupancy, all lattice rotations and reflections, complete point–placement incidence, and full vertex-contact surrounds. All choices of the inner coronas are reconsidered at each depth. SAT witnesses are checked by independent vertex-sector counts; upper-bound proofs are checked with DRAT-trim. This is a specialized CDCL experiment, not the reference GCTS generation scheduler.

Blind hole-free searches add explicit enclosure cuts when necessary. No published corona or learned marking is supplied to the solver. Small periodic searches use at most two copies in a period cell; failure in that family is inconclusive. Runs may overlap and their times are diagnostic, not comparative benchmarks.

The broader polygon record \(H=6\), from Bojan Bašić, lies outside these three regular-grid polyform families and is not reproduced here. This experiment establishes lattice results; it does not independently exclude off-grid Euclidean placements.

Full method and reproduction commands