Heesch numbers: the potentially non-tiling catalog
Full touching-tile coronas, checked obstructions, and a cold comparison of graph search, learned affine markings, and Glucose. Established space-fillers are excluded from the candidate search; published periodic tilers are tested separately as positive controls.
Three candidates resolved as tilers. The 2-semicross, Letter O, and tuning fork each have a checked periodic construction with two tile copies, proving \(H=\infty\). They are now excluded from the table and further benchmarks. 2-semicross certificate · Letter O certificate · Tuning fork certificate
Classifications and current bounds
Polycubes use integer translations, proper cubic rotations, and complete face/edge/vertex surrounds. The uniform-angle solids have a stronger Euclidean obstruction. The two names for the nonacube cross are consolidated. Mixtures are not tested as if they were single polyhedra.
| Tile · click to inspect | Heesch result | Evidence and limitations |
|---|
Inspect the catalog geometry
Six bent arms: no first lattice corona
The 25-cube reconstruction of Sridhar Ramesh’s six-arm illustration has checked lattice Heesch number \(H=0\). Glucose excluded a first corona in 17.34 seconds, and DRAT-trim verified the proof. A separate enumeration checked all 4,396 eligible neighboring placements. This additional source example is separate from the catalog counts above. Rotate the exact prototype and inspect the evidence. Compare alternative bends.
Ring octocube: exactly one lattice corona
Checked result: \(H=1\). The planar \(3\times3\) ring with its center missing admits a complete first corona of 27 surrounding tiles. No second corona exists, so it cannot tile the cubic lattice. This additional source example is separate from the 19 catalog candidates counted above.
Glucose found the first corona in approximately 0.0006 seconds and excluded the second in 1.29 seconds, with proof recording enabled. These are individual search times, not comparative benchmarks. The exclusion ranges over every first corona, not just the displayed witness data. DRAT-trim verified the proof in approximately 0.95 seconds.
Independent cube-vertex checks validate the positive witness. A separate rectangular translation scan reproduces all 386 possible root neighbors and all 4,364 candidates needed for two coronas. The original nonacube encoder and the catalog encoder give identical clauses for this tile. The result permits integer translations and all cubic-lattice orientations; it does not address arbitrary rotations or noninteger placements.
Literature correction: Papoutsis’s empty result for entry 834 means his periodic search found no motif. The same discussion already reports the ring as non-tiling, including a later box-covering obstruction. Calling its general tiling status unresolved was misleading. This computation independently establishes the stated lattice corona count; it is not a claim of a new non-tiling discovery.
First-corona coordinates · Verification receipt · Second-corona formula · UNSAT proof · Methods and reproduction
Validation against published periodic tilings
These two tiles have published twelve-copy periodic motifs, so \(H=\infty\) and two coronas must exist. The original nonacube encoder is reused with only the prototype orientations replaced. Its clauses match the later catalog encoder exactly. The motif is withheld from each blind search.
Outcome: all 24 known complete patches were accepted, and all 48 incomplete fixed patches were rejected. The five blind solver attempts remained undecided at their limits; none found a two-corona patch. This is a successful known-witness check, not a successful blind reproduction. Validation summary
| Known tiler | Blind Glucose search | Blind CaDiCaL search | Known two-corona patches accepted | Tiles in extracted patches including root | Evidence |
|---|
Separate witness tests reconstruct the infinite periodic tiling by exact residue lookup, extract coronas around every motif tile, then fix every placement variable and check every SAT clause. Removing a first-layer tile or a second-layer tile must reject the now-incomplete fixed patch. These are model validation tests, not blind search successes. Cutoffs remain unknown. Runs may overlap with validation work; their times are not comparative benchmarks.
Agreement on these examples tests whether the encoding accepts real coronas and enforces both coverage layers. It does not by itself prove the nonacube reduction correct for every possible configuration. Methods and commands · All root-position checks
Finite cases: time and visited search size
Every row below is the same geometric target in all three lanes. Each lane starts cold, and the table shows medians of three sequential runs. Learning and geometric compilation are included. Proof recording is disabled in all timed runs and verified separately. Glucose uses its normal CDCL search; the marked lane uses a specialized frontier graph scheduler.
| Target | Unmarked graph | Learned affine GCTS | Glucose sequential-counter CNF | Graph dead leaves unmarked to marked | Glucose conflicts / decisions |
|---|
Glucose conflicts are not ordinary tree leaves: backjumps, learned clauses and restarts change the search structure. Graph counts are terminal branches actually visited, not inferred sizes of pruned subtrees. A contradiction during Glucose formula loading can precede its search counters. Python graph engines versus native Glucose is an implementation comparison, not an asymptotic complexity claim.
Scheduling scope: both graph lanes use explicit corona generations and scan globally at node entry and after forced moves. Between failed siblings they continue at the chosen point; they do not perform the reference scheduler’s full rescan until the next child. The methods document records this conformance gap.
What the markings learn
At a dead frontier point, the learner finds selected tiles that block every possible geometric covering tile. It removes distant tiles while that certificate survives. Conditional second-layer obligations retain an activating tile in the learned core.
Each core receives a private affine channel at the fixed root anchor:
\[\sum_{i=1}^{k}z_i=1,\qquad\text{role }i:\ z_i=0.\]All roles conflict; every proper subset of that channel admits a coordinate-vector witness. Anchor positions identify the intended placements. Incremental counters eliminate the last missing role through the candidate graph.
Every learned exclusion is checked geometrically. These are context-preserving redundant constraints, not restrictions inferred merely from successful training examples. The implementation still uses many private channels and does not claim a compact, symmetry-complete decoration.
What a corona means here
A first corona fills the full voxel halo of the root. A second must also surround every selected root neighbor. The first layer varies throughout the search; failure to extend one chosen patch would not prove an upper bound.
Outermost tiles need no additional surround, and overlap is forbidden everywhere. This convention distinguishes the new Heesch results from older finite distance-window experiments.
The tetrahedron, octahedron and cuboctahedron have a separate exact edge-angle obstruction: at a generic root-edge point a complete surround would require
\[n\alpha+m\pi=2\pi.\]Their uniform dihedral angles admit no such nonnegative sector counts with an edge sector present. The check uses exact rational arithmetic and does not assume face-to-face contacts.
What is still unresolved?
The table exposes every unresolved value and its available lower bound. The regular truncated tetrahedron has multiple dihedral angles, so the uniform-angle argument is inconclusive. Chair44 needs a faithful full-boundary corona reduction; its point-window results are not silently converted into Heesch bounds.
Unresolved two-corona searches were first given a short Glucose budget, then selected cases received longer searches or a graph-search pass. Budgets, partial search counts and witnesses are preserved in the data. The tuning fork was subsequently resolved by a periodic certificate. Unknown outcomes for the remaining candidates remain unknown.