The same hexagonal tiling carries six separate pieces of work in this series. A lunar habitat answering a NASA gap ledger. A compressed-earth-block house buildable on a lot in Newark. A load-sharing argument about walls. A magnetic-symmetry census. The descending chirp of a staircase at Chichén Itzá. And a conjecture about why any of that should be true at once.
A geometry that turns up in six places is not evidence. It is a temptation, and the failure it invites is specific: proving something about the tiling and then citing it about whatever else the tiling resembles. This paper is the ledger of what actually crosses.
| Where | What it is |
|---|---|
| Ch 16 | The crystalline lattice — the geometry itself |
| Ch 17 | Magnetic lattice — Shubnikov census, helimagnet periodicity |
| Ch 18 | Seismic lattice — load share, crack tortuosity, detuning |
| Ch 19 | Acoustic lattice — the staircase chirp |
| The Stone Fold | Seismic geometry in ancient architecture |
| G6 Crystal | Arquitetura e conjectura — the unifying claim |
| NASA Architecture | The Moon Base gap ledger, by functional gap code |
| G6 Earth House | CEB housing: build a stable home from the dirt on land you own |
| Biosynthetic Building | The course that teaches the build |
These are theorems about the tiling. They hold in vacuum, in Newark soil and at Chichén Itzá, because none of them mentions a material, a gravity or an atmosphere. They are the only results that may be cited anywhere in the list above without further argument.
| Theorem | What it says | Rests on |
|---|---|---|
| FN_H_101L_isoperimetric | The hexagon encloses a given area with the least perimeter among regular tilings — 3.7224 against 4.0000 and 4.5590 per unit area | permitted three |
| FN_L_101L_hex_interfaces | Six mating interfaces per cell, all distinct; any two neighbours mate on exactly one | permitted three |
| hex_load_share_min | Each contact face carries 1/6 of an applied load — the minimum among regular tilings | permitted three |
| no_straight_continuation | Three edges at 120° per vertex, so no edge path has two consecutive collinear edges: a crack must turn at every junction | propext alone |
The last one closed on 2026-09-14 and is the cleanest result in the group: it needs neither choice nor quotients. It is also the one with the most direct build consequence, and the consequence is not part of the theorem — that a turning crack costs more energy than a straight one is the engineer's inference, drawn outside the kernel and stated as such.
These carry a hypothesis across with them. The theorem is true wherever the hypothesis holds and says nothing where it does not, which is the honest way for physics to enter a proof assistant.
| Theorem | The hypothesis it carries | Travels? |
|---|---|---|
| detune_bounds_amplification | hA: amplification does not grow as the structure is detuned further from the ground's dominant period | ✓ wherever a response spectrum is monotone |
| full_diffraction_spectrum | An optical-grating model of the staircase (Declercq et al.) | ∼ once the model is fixed |
| hexagrid_collapse_superior | A finite-element model of progressive collapse | ∼ once the model is fixed |
| heliSpin_incommensurate_aperiodic | Irrationality of q/2π | open — the one remaining sorry |
Until 2026-09-14 the detuning theorem concluded 0 < |T − T_g| ∨ T = T_g — true of any two real numbers, needing none of its hypotheses, silent about any building. It could have been closed in one line at any point, and that close would have produced precisely the artefact the RFI errata documents: no sorry, permitted axioms, nothing said. Restated with hA explicit, it became a theorem worth closing, and then closed.
Two claims in the acoustic chapter were declared as theorems for a year and were never propositions. Whether the Maya designed the descending chirp is a question about people in the past. Whether the chirp is the resplendent quetzal's call is settled by recordings and listeners. Both are now prose in the file; keeping them declared put two permanent non-obligations into a register of dischargeable ones.
The scope warning at the head of SeismicLattice.lean is the most important sentence in this cluster, and it is there because the mistake is easy and would be invisible once made:
These theorems are about the hexagonal tiling — the unit is a hexagonal cell with six edge-neighbours, so each contact face carries 1/6 of a load. They are not about the honeycomb lattice of graphene, whose unit is a vertex with three nearest neighbours at 120°, and which is not a Bravais lattice at all. The two are duals. Both carry D₆ symmetry; only the tiling carries hex_load_share_min. Do not cite these facts in support of a graphene claim.
That is what a transfer ledger is for. D₆ symmetry is shared, and sharing a symmetry group is the weakest possible reason to think two results are the same result.
The Moon Base and the Newark house are the same geometry on different ground, and the trip between them is where the ledger earns its keep. The same mathematics. Different ground.
| Moon Base | Earth House | Survives the trip? |
|---|---|---|
| Hexagonal module, isoperimetric optimum | Hexagonal CEB module | ✓ geometry, unchanged |
| Six mating interfaces, standardised | Six block faces, one press | ✓ unchanged |
| Crack must turn at every junction | Same, in compressed earth | ✓ a tiling fact |
| Pressure vessel against vacuum | — | × no vacuum; the requirement does not exist |
| ISRU: build from local regolith | Know what you have before you press it — soil testing | ∼ same principle, different instrument |
| Seismic detuning (no ground motion on the Moon of this kind) | Detuning against a real quake spectrum | ∼ matters more here than there |
| Power generation | Grid, or not | × open in both; the RFI response was withdrawn |
Two rows in that table run the other way, which is the reason to write it down. Seismic detuning is close to irrelevant on the Moon and load-bearing in Newark; the pressure vessel is the whole problem on the Moon and absent on Earth. A framework that only ever exported from the glamorous case to the ordinary one would have missed both.
No building has been built and no hardware flown. Everything above is geometry, plus named models, plus one house design and a course that teaches it. Nothing here is a structural engineering certification and none of it substitutes for a licensed engineer or a local building code.
A closed theorem is not a closed gap. The NASA ledger stands at two of eight rows fully closed, and the work of 2026-09-14 did not move it — because the open rows are open for physical reasons, not for want of proof effort. Any reading of this paper that converts proofs into readiness is a misreading.
The unifying conjecture is a conjecture. That one tiling should serve load, symmetry and sound is stated in G6 Crystal as a claim to be argued, not a result. This paper only audits what transfers given the geometry; it does not establish why the geometry recurs.
Sharing a symmetry group proves nothing. Stated again because it is the failure this ledger exists to prevent.
Companion pages: NASA Architecture · WP-115 on why a kernel cannot see the difference between these categories · docs/verification-checklist.md for the method.
sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.