A lunar habitat whose every structural dimension follows from two invariants — and whose every gap-closure claim is bound to a named theorem that a build must accept before the claim may stand.
| Solicitation | Notice ID 80JSC026MoonBase_RFI |
|---|---|
| Requirements source | NASA Moon Base User’s Guide, NP-2026-04-6806-HQ, April 2026 — functional gap codes FN-xxx-L |
| Response | submitted 14 April 2026 · corrected 21 May 2026 · errata 21 August 2026 |
| Deposit | doi:10.5281/zenodo.19162012 (concept DOI — the deposited text still carries the §4 section withdrawn on 2026-08-21) |
| Respondent | G6 LLC · Pablo Nogueira Grossi · Newark NJ · EIN 33-2880433 · SAM.gov registered · ORCID 0009-0000-6496-2186 |
Among regular tilings, the hexagon encloses a given area with the least perimeter: 3.7224 against 4.0000 for the square and 4.5590 for the triangle, per unit area. On a surface where every square metre of pressure wall is mass delivered from Earth, that ratio is the whole argument. It is also the one claim here that is both machine-checked (FN_H_101L_isoperimetric) and checkable by hand.
The criterion the response asked NASA to apply is stated in the ledger itself: a sorry is an open gap; closing a sorry closes a NASA functional gap. The table below is generated from that file's own status marks, not from the submission.
A thirteenth declaration, nasa_gap_closure_summary, collects the closures so that the table's status is decided by whether that theorem compiles.
The twelve gap theorems are probed by name in .github/workflows/verify-proofs.yml and judged by tools/axiom_gate.py, which fails the job on sorryAx or on a missing declaration. The file sits inside the Orthogenesis default build target, so lake build compiles it; before 21 August 2026 it was in no target at all and had never been compiled by anything.
| File | Decls | Admitted | Gate |
|---|---|---|---|
| NASAGaps.lean | 12 | 0 | probed by name in CI, per theorem |
| G6Crystal.lean | 33 | 0 | kernel-audited |
| AcousticLattice.lean | 11 | 3 declared | OK — no sorryAx, permitted axioms only |
| MagneticLattice.lean | 20 | 1 (M2) | PASS-AS-DECLARED |
| SeismicLattice.lean | 17 | 1 (Q2) | PASS-AS-DECLARED |
| DM3Bridge.lean | 14 | 0 | no gate report on disk |
| ToyModel.lean | 14 | 0 | no gate report on disk |
| Coverage.lean | 6 | 0 | in the Orthogenesis target; compiles. No gate report yet |
The rows to read are the last three. Compiles and kernel-audited are different things: a file inside the build target is known to elaborate, but without a #print axioms report nothing has checked what its theorems rest on. Three files are in that state. They are listed rather than omitted, because the omission is what would mislead.
Corrected 2026-09-14: this table previously recorded Coverage.lean as outside every build target, following docs/lean-4.32.0-ledger.md and the errata of 2026-09-11. It has since been added to Orthogenesis.lean and builds with the target (job 8684 of the 2026-09-13 lake build). The claim was stale in the pessimistic direction, which is the safer way to be wrong and still wrong.
An internal audit on 20–21 August 2026 found that three claims in §5 of the May submission were not supported by the artifacts they cited, and that the verification metric the submission proposed to NASA did not measure what it was said to measure. None of the errors were found by a reviewer.
Units. The supporting theorem compared a dimensionless count of limit cycles against a number of hertz. The comparison is a true statement about two real numbers and an empty one about the world — and the Lean kernel does not carry units, so it certified something not physically well-formed.
Wrong mode. The frequency was taken from the lossless idealisation, which places the fundamental at 10.59 Hz rather than the observed 7.83 Hz.
Back-fitted constant. The multiplier that reached the target figure was the factor required to reach it, not a rotation number derived from anything.
No cavity. Schumann resonance is a property of the Earth–ionosphere cavity. The Moon has none. In the environment the response was written for, the coupling is not mistuned — it is absent.
There was indeed no sorry in the file. There were also three items its own header called open obligations. Both were true at once, because the obligations were written as theorems concluding True. Such a statement compiles, contains no sorry, and passes #print axioms on the standard three — it is indistinguishable from a real theorem to every automated check, including this repository’s. The criterion the submission asked NASA to apply could not see it.
The corrections reduce the claimed scope. No correction expands it. What survives is stated as plainly: the hexagonal isoperimetric optimum, the dimensional derivation from the dm³ invariants, phase payload monotonicity and the hex-grid colony results are non-vacuous and unchanged. The withdrawal costs the physical justification of the aspect ratio, not the geometric one.
The response to finding a vacuous theorem was not to delete the category but to make it declarable. Orthogenesis/Architecture/KNOWN_PLACEHOLDERS.txt is append-only and lists every statement whose conclusion is True, so that CI can tell a known vacuity from a new one. The rule is one line: declared-open is acceptable; undeclared-open fails the build. Six entries are active.
A retired entry is commented out with the date and reason, never deleted — because a bare list loses its own history the moment an entry goes, and would say six while carrying no trace that it once said seven.
Nothing on this page needs to be taken on trust, and the fastest way to judge it is to run the same checks the repository runs. No account, no credentials.
# the twelve gap theorems, and what each rests on grep -n "^theorem" Orthogenesis/Architecture/NASAGaps.lean # every declaration in the repo, what it rests on, and what has no gate python3 tools/toolchain_ledger.py --write && head -12 docs/lean-4.32.0-ledger.md # the declared-vacuity register: declared-open is fine, undeclared-open fails CI cat Orthogenesis/Architecture/KNOWN_PLACEHOLDERS.txt # the kernel check itself, on one file (needs Lean + a built Mathlib) bash tools/leancheck.sh --audit Orthogenesis/Architecture/SeismicLattice.lean
The audit reports this page cites are committed under tools/verify-audit/<date>/, one per file, with the axiom list for every declaration. They are the evidence, not a summary of it.
| If you are checking the mathematics | |
|---|---|
| Ch 16 · The Crystalline Lattice | The geometry the rest depends on |
| Ch 18 · Seismic Lattice | Load share, crack tortuosity, detuning — the structural face |
| Ch 17 · Magnetic Lattice | Shubnikov census; one open obligation, named |
| Ch 19 · Acoustic Lattice | Where two claims were found not to be propositions at all |
| Orthogenesis · Geometry | The layer underneath: hex grid, cell, colony, growth, hexagonal form, discrete Gauss–Bonnet. Fifteen declarations, no sorry, and no mention of a material anywhere |
| Lean v4.32.0 ledger | Every tracked declaration, what it rests on, what has no gate |
| If you are checking whether it builds anything | |
| G6 Earth House | The same geometry as compressed-earth-block housing — the terrestrial case, costed |
| Biosynthetic Building | The course that teaches the build |
| The Stone Fold | Seismic geometry in ancient architecture — the precedents |
| G6 Crystal | The unifying conjecture, cited as a conjecture |
| If you are checking the method | |
| WP-119 · Which Theorem Travels | Which of these results may be cited on the Moon, in Newark, at Chichén Itzá — and which may not |
| WP-73 · The Stamp and the Triple | Why a verification claim needs artifact, toolchain and library together |
| WP-115 · The Fold in Formal Verification | The class of failure a kernel is built not to see |
| The verification checklist | Twelve steps, four stages, with a status column saying what is not yet implemented |
| The audit log | Every defect found in this corpus, dated and classed. Including the ones on this page |
| The response documents | |
| Errata, 21 August 2026 | The three withdrawn claims in full, with the identifier corrections |
| Zenodo community | Deposits with DOIs — concept DOI 10.5281/zenodo.19162012 |
| github.com/TOTOGT/geometry | The corpus, its tools, and the CI that judges it |
| Master index | Every page, with its scope stated in the footer |
Corrections are published in place rather than withdrawn silently, and the register of defects is public and dated. The errata above was produced by an internal audit, not by a reviewer; the stale row corrected on this page today was found the same way. That is the standard being offered — not that nothing here is wrong, but that what is wrong is findable, by you, without asking.
No flight hardware exists. No physical test has been performed. Nothing here is a NASA endorsement, a contract, or a statement by NASA; the gap codes are cited from a public guide and the responses are G6 LLC’s own. Six of the eight gap rows are partial or open and are marked so; two are closed. The geometric results are machine-checked; the engineering claims that would turn a geometry into a habitat are not, and are not asserted.