| File | Decls | What it establishes |
|---|---|---|
| HexGrid.lean | 2 | Axial coordinates, and that every cell has exactly six neighbours, all distinct |
| Cell.lean | 0 | The unit: a coordinate and a stage. Definitions only |
| Colony.lean | 4 | A set of cells and its expand; reachability is monotone — the basis of the NASA autonomy row |
| Growth.lean | 1 | Stage-gating: a cell at stage n cannot appear before stage n−1 exists |
| HexForm.lean | 5 | The hexagon itself — the isoperimetric optimum the habitation row rests on |
| GaussBonnet.lean | 3 | Discrete Gauss–Bonnet on the tiling: curvature is bookkeeping, and it closes |
Not one of these files mentions a material, a gravity, an atmosphere or a load. That is not modesty — it is the reason the results hold equally in vacuum, in Newark soil and at Chichén Itzá. Everything above this layer carries a hypothesis; everything in it carries none.
Which theorem may be cited where, and which may not, is set out in WP-119 · Which Theorem Travels. The short version: the tiling and the graphene honeycomb are duals, both carry D₆ symmetry, and only the tiling carries the load-sharing result. Sharing a symmetry group is the weakest possible reason to think two results are one result.
All six are imported by Orthogenesis.lean and build with the target, so they are known to elaborate. None currently carries a #print axioms report, so nothing has checked what their theorems rest on. That is a real gap, it is listed as declared, no gate in the ledger, and it is stated here rather than left for a reader to discover.
| NASA Architecture | The Moon Base gap ledger — thirteen NASA functional gap codes, twelve theorems |
| Ch 18 · Seismic | Load share, crack tortuosity, detuning |
| Ch 19 · Acoustic | The staircase chirp |
| G6 Earth House | The same geometry as compressed-earth-block housing |