A first corona exists.
The displayed packing was found using Z3 and is replayed with integer arithmetic. The verifier checks the shape of every copy, all overlaps, and the complete boundary surround. This establishes \(H_{\mathrm{lat},26}\geq1\).
VERIFIED LATTICE RESULT 24 SEPTEMBER 2026
Nine cubes.
Exactly one corona.
The planar cross can be completely surrounded once. A checked impossibility proof rules out every second corona—and therefore every tiling of the integer cubic lattice.
\(H_{\mathrm{lat},26}(P)=1\)Integer translations · cubic rotations · face, edge and vertex contacts
The complete first corona
EXACT WITNESSLoading the verified surround…
Central cross Surrounding copies
Drag to rotate · scroll to zoom · click a tile to inspect
Transparent colors reveal the central tile. Coordinates are the verified packing; the outer tiles need not be surrounded.
TWO COMPLEMENTARY CERTIFICATES
Why the answer is exactly one
No second corona exists.
A finite formula covers all possible first coronas and their possible surrounds. A modified Glucose 3.0 SAT solver produced the published UNSAT proof, which is checked independently. A larger corona or infinite lattice tiling would supply a second corona, so both are excluded.
Solver credit. Glucose, developed by Gilles Audemard and Laurent Simon, supplied the crucial proof-producing SAT engine. Glucose 3.0 is based on MiniSat 2.2. Our computation uses a Glucose hybrid with modifications to learned constraints and their geometric propagation. The solver modifications and reproduction instructions are published. DRAT-trim and cake_lpr independently check the resulting certificate; verification does not require rerunning Glucose.
8,140placement variables
569,020exact constraints
2proof-checking stages
0extra geometric exclusions
The exact scope. Copies use integer translations and proper cubic rotations; reflections add no orientations for this tile. A corona includes face, edge and vertex contacts, with no topological-ball condition. This result does not decide tilings using arbitrary off-grid Euclidean placements.
REPRODUCE IT ON YOUR MACHINE
The proof travels with the result.
Download the self-contained package, or give its verification instructions to your AI. Checking the existing Glucose-generated certificate needs no SAT solver or research app.
Open the AI-readable verification instructions ↗AFTER EXTRACTING THE ARCHIVE
cd polycube-certificates
python3 verify.pyThe command regenerates the formula, audits the candidate universe, replays the first corona, checks the DRUP proof with DRAT-trim, then checks the generated LRAT proof with the formally verified cake_lpr checker.
Python 3.9+ and a C99 compiler · x86-64 or ARM64 · about 3 GB free disk and several GB available RAM. Offline after download.
Complete local verification passedApproximately two minutes on macOS ARM64 · all eight regression tests passed. Linux CI is configured in the package but has not run.
Checksums and raw artifacts
The archive SHA-256 is:
c1d36e7bad4d2f20194e83c6eb61c061ad81c0f0a009ee9ab7b26cf90b865fa4The archive includes pinned checker sources, the deterministic encoder, geometric audit, formula, proof, positive witness, and recorded logs. The mathematical reduction is documented; it is not itself formalized in a proof assistant.
CONNECTION TO THE ORIGINAL QUESTION
One catalogue candidate, now certified.
This is entry 25373 in Georgios Papoutsis’s nonacube catalogue. His 2021 Stack Exchange answer carefully distinguished a search that found no tiling from a proof of impossibility. This certificate supplies the latter for this particular tile under the stated lattice model.
It does not certify the entire catalogue or establish a smallest non-space-filling polycube theorem.