On 18 August this desk sent NASA an errata correcting its response to the Moon Base RFI. The errata quoted an offending line — a theorem whose entire content was True — and stated that such statements had been deleted rather than converted to sorry, on the reasoning that a retracted claim is not an open one.
On 21 August the statement was still in the file. A scan written that same morning, for a different purpose, printed it on its first run.
The correction had been made in a previous working session and never committed. The document reported the repair; the repository never received it. Both halves were sincere and the gap between them was invisible to every layer — to the compiler, to the kernel, to continuous integration, and to the person who wrote the errata.
| Failure class | Question it asks | What detects it | Status |
|---|---|---|---|
| MISMATCH | Is this the artifact that was checked? | Content hash | closed |
| STALE | Is this the environment it was checked in? | Environment probe | closed |
| FAIL | Does the check still pass? | Re-run | closed |
| FALSE | Is the statement true at all? | Elaboration — only if a build target reaches the file | closed |
| VACUOUS | Does the statement have content? | Declared-baseline scan | closed 21 Aug |
| UNTRUSTED | Does the proof rest on the kernel? | Axiom allowlist | closed 22 Aug |
| MISATTRIBUTED | Does the statement support the claim made from it? | Nothing, and nothing can | open |
Twelve theorems in this repository are indexed against NASA functional gap codes. All twelve are true, all twelve are proved, and every one reports only the standard axioms. Reading the statements against the codes they answer, five prove something other than what they are filed as.
One asserts that the seed cells of a colony survive n growth steps, and is filed as a proof of reachability — which is the opposite inclusion. One proves that adjacency is symmetric and is filed as proving that neighbours share exactly one interface. One proves n_layers = 6 by unfolding a definition, and is filed under a claim about processed regolith.
No axiom check can see any of this, because the defect is not in the Lean and not in the prose. It is in the join between them, and every layer inspects one side.
The first six classes are mechanical: both sides of each comparison are machine-readable. The seventh is not, and will not become so.
What remains mechanisable is the bookkeeping, not the judgement: require every theorem cited in a claims table to carry an identifier, require every identifier in the prose to resolve to exactly one theorem, fail on either side unmatched. That catches drift. It catches nothing about whether the pairing was ever warranted.
The residue is a signed three-column table — statement as written, what it strictly licenses, what is claimed from it — and a person is the only thing that can produce it.
The vacuity gate. Six statements of the form : True := trivial are declared in a baseline file; an undeclared seventh fails the job. It caught one on its first run — the one the errata had reported deleted.
The axiom gate. One of the twelve rested on native_decide, an axiom emitted when a goal is discharged by compiled code rather than by the kernel, inside a step named Kernel axiom check. Rather than permit the axiom, the proof was rebuilt with decide: the kernel now reduces the goal itself.
The vocabulary gate. A search engine’s generated summary described this corpus as using a “Log-Psi Recurrence Operator” and “Harmonic Resonance Bands (HRB).” Neither term occurs anywhere in it. A 148-term declared baseline now fails on any coined term that appears undeclared.
On the same night, two working sessions with no contact between them diagnosed the same problem in the same file — a 168 KB instruction document, most of it closed history, loaded in full at the start of every session — and both split it, one into CLAUDE-ARCHIVE.md and one into docs/audit-log.md.
Same diagnosis, same remedy, different filename, arrived at independently. The merge that reunited them conflicted on exactly that file and nothing else.
It is a small instance of a large claim this desk has been arguing elsewhere all week: that where a problem admits few solutions, unconnected parties will arrive at the same one, and the arrival is evidence about the problem rather than about the parties.
Why print the defect list rather than the green badge: because seventeen theorems now pass a kernel check that asks for them by name, and that sentence is worth exactly as much as the reader’s ability to see what it does not cover. The run is public and re-runnable. So is the list of what it cannot see.
Toulouse, 1665 — some months before the world was told he was dead.
He was sixty-four, and he had begun, privately, to keep two sets of books. The serial continues; the note on fact & fiction stands, and the false report of Fermat’s death in 1653 — Bernard Medon’s letter, and its retraction a week later — is the documented part.