WP73 · The Stamp and the Triple · Verification Claims That Outlive Their Evidence

1 · A header that was true, and then was not

On 20 July 2026 a file entered this repository containing five theorems about a six-site D₆-equivariant ring, and a header asserting that all five had been kernel-verified: 0 sorry, and #print axioms reporting only propext, Classical.choice and Quot.sound for each. No sorryAx. One commit, one day, claim and code together.

On 21 August 2026 the file was run for the first time in a month. Three of the five theorems depended on sorryAx. They were admitted, not proved.

The obvious reading — that the header was written without running anything — is wrong, and the way it is wrong is the subject of this paper. The machine that produced the file still carries a Lean tree pinned to v4.14.0, the toolchain the header names, with a built Mathlib in it. Running the preserved 20 July copy there separates the causes cleanly:

theorem	20 July, v4.14.0	21 Aug, v4.33.0-rc1	class
`angCoupling_not_commute` `rot_commutes_coupling`	proved	proved	stable
`gate_commutes_onsite` `hex_rotation_invariant`	proved	`sorryAx`	decayed
`hex_coupling_uniform`	`sorryAx`	`sorryAx`	misfiled

The two that decayed were genuinely proved in July. Between v4.14.0 and v4.33.0-rc1, Mathlib reorganised its import graph and stopped supplying Fintype (Fin 6) transitively through Mathlib.Data.Real.Basic. Without that instance fin_cases cannot perform the case split; Lean logs the failure and its error recovery admits the open goal. Nobody edited the file. Nobody made a mistake. A true claim became a false one while the object it described sat unchanged on disk.

The third has a different history, and it is legible in two timestamps sixty seconds apart:

22:28 sibling copy written. Contains the ring call that closes c + c = 2 * c.
Header reads: KERNEL-VERIFIED: <pending — run and record>
22:29 repository copy written. The ring is gone.
Header reads: KERNEL-VERIFIED 2026-07-20 … No sorryAx

In one minute, a rewrite dropped a tactic and promoted a disclaimer into a claim. The fix and the assertion that the fix had worked ended up in different files. Neither file is dishonest. The copy that could justify the claim declines to make it; the copy that makes it cannot justify it.

Definition

Claim–artifact separation. A verification claim and the object it verifies come to reside in different places, such that no reader — human or automated — can detect the separation from either place alone.

2 · The triple

The defect that permits all of this is stateable in one line. A verification claim names an artifact. But what was verified is a triple:

V = ( artifact , toolchain , library )

File headers record the artifact. Lock files record the library, elsewhere, unlinked to any claim. Toolchain pins record the toolchain, elsewhere again. No convention in common use binds the three to the assertion that depends on all of them. The consequence is that a claim can survive intact while any of its three arguments is replaced — and it will read exactly as it did when it was true.

This is not a Lean problem. It is the general shape of software provenance: a green badge, a signed attestation, a verified field in a manifest, a comment saying checked. Each names what was checked and omits what it was checked against.

3 · Three classes, and why they must be distinguished

Once the triple is written down, the failures separate. They demand different responses, and conflating them produces the wrong action every time.

	what changed	who erred	correct response
MISMATCH	the artifact is not the one that was checked	nobody lied; a copy, a handoff or a transcription separated claim from code	find the sibling; reconcile; never trust either copy until re-run
STALE	toolchain or library moved	nobody at all	re-run and re-stamp; the claim may well still hold
FAIL	the check itself now reports a forbidden result	a real regression	fix the artifact

Treat a STALE as a FAIL and you go looking for a bug in a file that has none. Treat a MISMATCH as a FAIL and you repair the copy in front of you while the correct version sits unused one directory away — which is precisely what happened here in July. Treat any of them as a passing check and you get a month of silence.

4 · Why no layer objected

The header stood for a month inside a repository with continuous integration, a formal kernel, and a version-control history. Each layer was working. None of them was pointed at the claim.

The file sat at the repository root. The Lake configuration declared one build target, lean_lib Orthogenesis, which did not include it. lake build therefore never compiled it — not once, in a month, on any push.
The CI job contained a step named “Real axiom check through the Lean kernel.” It was a real kernel invocation. It probed six definitions — hexNeighbors, hexToVec2, Cell.center, Cell.radius, Colony.insert, Colony.expand — and no theorems. Definitions cannot depend on sorryAx. The step could not fail.
The repository held no built Mathlib, so the file could not have been compiled there even by hand. The header named a different tree as the site of verification, and that tree was outside version control.
Three copies of the file existed on one disk, in three directories, two of them untracked. They were not identical.

The general shape

Every layer here checks well-formedness, and well-formedness is exactly what a false claim can afford. A build succeeds or fails; it cannot report that the file it never compiled was the important one. A kernel accepts a proof; it cannot report that the declaration it was handed is a definition. A badge turns green; it certifies that the configured steps ran, not that the configured steps were the right ones. And a comment asserting verification is, to every automated reader, indistinguishable from a comment asserting anything else.

5 · The cost structure

Naming the costs is what makes them targetable, and the distribution is counter-intuitive.

cost	magnitude here	reducible?
writing the claim	one line, seconds	no — and this is the root asymmetry
the defect itself	two lines: one `import`, one `ring`	already negligible; not worth optimising
detection	unbounded — nothing initiated it; it happened by chance a month later	yes, qualitatively: to one CI cycle
localisation	six filesystem sweeps, a `git log`, three runs, one wrong hypothesis	yes — named declarations in the output
adjudication	two days; required preserved specimens, an obsolete toolchain, and someone doubting the auditor	replaced, not accelerated, by the three exit codes
contamination	the claim reached three files, a manuscript and a commit message	only via detection latency

Repair was free. Detection was unbounded. And contamination is not an independent cost but a multiplier on latency: every day a false claim stands is another artifact that inherits it. A claim caught within one CI cycle cannot reach a paper. That reorders the priorities completely — the target is latency, because latency is what converts a two-line defect into a corpus-wide one.

Counter-move that costs

Consolidation has a negative term. Reducing to a single copy lowers drift cost and raises adjudication cost: the verdict above was settled by a specimen that had been moved to a deletion folder that same morning, read by a stale multi-gigabyte build of an obsolete toolchain. Delete either and the question does not become harder — it becomes permanently unanswerable. The resolution is to separate the roles: one source copy, n archived specimens, and the old toolchains retained as instruments rather than reclaimed as clutter.

6 · The instrument

verify-stamp binds the triple to the claim and reports which of the three has come apart. Its design follows from the failure it was built for.

The stamp lives inside the artifact, not in a sidecar file. A sidecar can be separated from what it describes, which is the failure being caught. The content hash covers the file with the stamp block removed, so the stamp can be rewritten without invalidating itself.
The comment prefix is inferred from whatever precedes the marker on its line, so the format works unmodified for --, #, //, %.
The environment is probed, not asserted. Each env-probe is a command whose output is recorded at stamping time and recomputed at check time. Drift is detected by comparison, not by trusting a written-down version string.
Stamping runs the check first and refuses to write a stamp over a failing result. A stamp cannot be issued for something that has not just passed.

Exit codes

0 OK       hash, environment and re-run all agree
10 MISMATCH content hash differs from the stamp
11 STALE      hash matches, environment moved
12 FAIL       re-ran; forbidden token present or declaration absent
13 ERROR      no stamp, malformed stamp, missing file, probe failed

The codes begin at ten deliberately, and the reason is a defect this tool found in itself. In the first test run, MISMATCH was 2 — the same code a Python interpreter returns for a file it cannot open. A broken invocation exited 2 and was scored by the tool's own test suite as a genuine MISMATCH: a green assertion, for the wrong reason, in a suite written to catch exactly that. A checker whose failure is indistinguishable from the failure it reports is the defect it exists to catch. The codes moved out of the range that shells and interpreters already occupy.

A fourth defect appeared the first time the instrument ran against real theorems, and it is the strangest of the four. #print axioms has two output forms: 'foo' depends on axioms: […], and — when a theorem rests on nothing whatever — 'foo' does not depend on any axioms. The check counted occurrences of the first string. Three of the twelve theorems it was asked about are axiom-free, so it counted nine and failed the job.

A checker that cannot see success

The three results it discarded were the three best results in the file — proofs resting on no axiom at all, not even propext. The other defects in this instrument corrupted an artifact or mislabelled a failure. This one is quieter and worse in a particular way: it was blind to the strongest possible outcome, and it reported that blindness as the file's fault. A verification tool has two ways to be wrong, and the literature attends almost entirely to the first: it can accept what it should reject, or it can fail to recognise what it should accept. The second produces no false assurance, so nothing downstream complains — it produces abandoned results.

A second defect was found by turning the instrument on itself. The source defined its delimiters literally — BEGIN = "…-BEGIN" — so when the tool stamped its own file it matched those two constant definitions as the stamp block and deleted them from the body it wrote back. The write reported success, with a hash and a timestamp. The file could then no longer import itself, and its test suite fell from twenty passes to two. The delimiters are now assembled from parts so they never appear literally, and any detected block whose lines do not all look like stamp lines is an ERROR rather than a licence to remove them.

Worse than what it detects

That failure is more serious than any in the taxonomy above. MISMATCH, STALE and FAIL all describe a claim that has come loose from a surviving artifact. Here the instrument destroyed part of the artifact and certified the result. A verification tool is a privileged writer, and privileged writers fail in ways their subjects cannot. It was found only by applying the instrument to itself, which is now a standing test rather than an experiment.

What a build target surfaced

Between 21 August and the following day, twelve theorems that had sat in this repository for a month were compiled for the first time, because a single line was added to a Lake configuration. Making them compile took six repair commits and turned up four distinct defects, none of which any of the three classes above describes:

a lemma admitted — hexRing_card, its successor case sorry, with coord_coverage a bare call to it;
a lemma misapplied — stage_bound, given one argument fewer than it quantifies over;
a lemma named but never supplied — hexNeighbors_nodup, cited by a theorem and defined nowhere;
a theorem false as stated — no_coord_collision, which could not be proved because it was not true.

The last is the one worth pausing on. MISMATCH, STALE and FAIL all concern a claim coming loose from a surviving artifact. This is a claim that was never true, sitting in a repository, indistinguishable from its neighbours, and undiscoverable until something attempted to check it. No stamp detects it. No axiom probe detects it. Only elaboration does, and elaboration only happens to files a build target reaches.

7 · What the instrument does not do

It does not decide whether the recorded command is the right command, or whether the declarations named are the interesting ones. A stamp that faithfully re-runs a check of the wrong thing will pass forever, and will pass with a hash, a timestamp and an environment fingerprint attached — which is a more convincing false assurance than a bare comment ever was. That risk is real and it is created by this tool.

The July CI step is the cautionary instance: a genuine kernel invocation, correctly executed, reporting truthfully about six declarations nobody cared about. No stamp would have helped, because the step was not wrong — it was aimed elsewhere.

Irreducible

Someone has to doubt the auditor. No mechanism produces that, and the failure it prevents is the worst available, because a wrong correction arrives carrying more authority than the error it replaces. In the audit reported here the decisive intervention was not a tool. It was the author reading the auditor's conclusions and saying that half of them were not true — which was correct, and which no exit code would have produced.

8 · Beyond the triple: two classes the stamp cannot reach

The classes above concern a claim coming loose from an artifact. Three further classes concern the artifact itself, and they were found by running the hardened job against a body of theorems rather than against one file. The first was described at the end of §6: a theorem false as stated, which only elaboration detects. Two more complete the ladder, and they are of opposite character — one is trivially mechanisable and had simply not been mechanised; the other cannot be mechanised at all.

VACUOUS. A theorem whose conclusion is True compiles cleanly, contains no sorry, and reports [propext, Classical.choice, Quot.sound] exactly as a real theorem does. #print axioms is the wrong instrument by construction: it asks what a proof rests on, and a trivially true statement rests on nothing. The check passes, truthfully, and certifies nothing. Six such statements are live in Orthogenesis/Architecture/; a seventh, hexagrid_collapse_resistance_superior, was reported deleted in an errata issued to a federal agency and was still in the file three days later. It is now gated: a scan compares the vacuous statements present against a declared baseline, and an undeclared one fails the job. That scan caught the seventh on its first run.

MISATTRIBUTED. A theorem that is true, proved, and credited with a claim it does not support. The twelve NASA gap-closure theorems are each indexed against a functional gap code; reading the statements against the codes, five of the twelve prove something other than what they are filed as.

theorem	what the statement proves	what it is filed as
`FN_A_104L_reachability`	`C₀.cells ⊆ (expandN n C₀).cells` — the seed cells survive n steps	“every cell in `expandN n C₀` is reachable from C₀ in exactly n steps” — the converse inclusion
`FN_L_101L_unique_interface`	adjacency is symmetric	“any two neighbouring cells share exactly one interface face”
`FN_U_103L_six_layers`	`n_layers = 6`, by `decide` on a literal	“each completed layer contains sufficient processed regolith to seed one additional module”
`FN_U_103L_expand_models_ISRU`	monotonicity, true of `expand` by construction	“one expand = one ISRU cycle”
`FN_T_202L_payload_ratio`	a ratio equal to 15 in ℕ, so any true ratio in [15, 16) satisfies it	confirmation that g² ≈ 14.98

Every one is true. Every one is proved. Each reports the standard three axioms. None supports the sentence recorded against it, and one of them is re-exported into the summary theorem that constitutes the machine-readable gap table.

The ceiling

MISMATCH, STALE and FAIL are mechanical: both sides of each comparison are machine-readable. VACUOUS is partly mechanical — the elaborated type is a formal object, so a checker can reject True and self-implication. MISATTRIBUTED is the first class in which one side of the comparison is a natural-language sentence. Deciding it means deciding whether a Lean proposition entails an English claim, which is not a decision procedure and will not become one. This is the ceiling of the verification stack and is worth stating as a ceiling: the stack can certify that a proof supports a statement, and can never certify that a statement supports a claim. Everything above that line is review, and review is done by a person or not at all.

What is mechanisable is the bookkeeping, not the judgement. Require every theorem cited in a claims table to carry a machine-readable claim identifier; require every identifier in the prose to resolve to exactly one theorem; fail on either side unmatched. That catches drift — a renamed theorem, a gap code whose theorem was deleted, a theorem quietly repointed at a second gap — and catches nothing about whether the pairing was ever warranted. The residual judgement has one honest form, a three-column table: statement as written, what it strictly licenses, what is claimed from it. The gap between the second column and the third is the audit.

UNTRUSTED. The opposite case — mechanisable, and simply not mechanised. One of the twelve, FN_H_102L_phase02_cluster, depends on colony_depth1_cells._native.native_decide.ax_1_1: an axiom emitted when a goal is discharged by compiled code rather than by the kernel. The gate is a grep for sorryAx and cannot see it, so a step named “Kernel axiom check” reports success on a theorem the kernel did not check. Enumerating the forbidden axioms is the wrong shape; enumerating the permitted three is two lines and closes the class for good, including against whatever axiom nobody has thought of yet.

	question asked	detected by
MISMATCH	is this the artifact that was checked?	hash
STALE	is this the environment it was checked in?	probe
FAIL	does the check still pass?	re-run
FALSE	is the statement true at all?	elaboration — and only if a build target reaches the file
VACUOUS	does the statement have content?	a declared-baseline scan; fully only on the elaborated type
UNTRUSTED	does the proof rest on the kernel?	an axiom allowlist
MISATTRIBUTED	does the statement support the claim made from it?	nothing, and nothing can

9 · Provenance of this paper

This chapter was produced across sessions of an automated assistant that does not retain memory between them, which is the same condition that produced the July defect. Its own errors are recorded here for the same reason the July ones are.

An earlier draft of the companion manuscript asserted “five results are proved without sorry” in its abstract. That sentence was copied from the file header, without running anything. The false claim moved from a comment into a manuscript in a single step — the ordinary mechanism, operating inside a paper about the mechanism.
On finding three theorems admitted, the auditor concluded the header had been false when written and stated so in a source retraction and a draft. That conclusion was reached by searching one directory — chosen because the header itself named it — and treating the absence of evidence as evidence. It was wrong for two of the three theorems. It was corrected only because the author disputed it.
The tool's test suite returned a false pass on its first run, and the tool corrupted its own source on first self-application while reporting success — both in §6. Four defects were found in the instrument during the writing of the paper that specifies it — the fourth, in §6, being an inability to recognise an axiom-free proof as a success. All four are recorded in its README rather than quietly repaired.
The Status block below originally closed its open item by citing run #235. GitHub records run #235 as failed. The sentence describes kernel steps inside that run and reports them as though they were the run — a true statement about a part, offered as a statement about the whole, in the Status block of a paper about exactly that substitution. It was caught on 22 August 2026 by checking the run rather than the sentence, and the citation now names run #238, which is green.
The earliest audit in this series, logged in April 2026, records a cosmetic overlay applied to the wrong page of a PDF — index 105 rather than 99 — caught by visual inspection and reversed. That is a MISMATCH in a medium with no kernel, no CI and no hashes, and it suggests the class is not an artefact of formal methods but a property of any workflow in which claims and objects are handled separately.

Status

The five theorems in SaturnHexagon.lean report [propext, Classical.choice, Quot.sound] and no sorryAx under leanprover/lean4:v4.33.0-rc1, run 21 August 2026 on the author's machine.

An earlier version of this paragraph recorded, as an open item, that the result had not been reproduced under v4.32.0 — the version this repository pins and its CI uses. That item is closed. Run #238 of verify-proofs.yml on branch verify-hardening, commit 8855044, compiled the library on a public runner under v4.32.0 and asked the kernel about seventeen theorems by name: the five above, and the twelve NASA gap-closure theorems in Orthogenesis/Architecture/NASAGaps.lean. No occurrence of sorryAx in any of them, and the vacuity baseline matches the file. The run is green as a whole, which is the property being claimed; an earlier version of this sentence cited run #235, which is not (see §9).

What that green does not establish is §8: eleven of the twelve rest on the kernel and one does not, and five of the twelve are filed under claims their statements do not support. Both are open. A green run is a statement about provenance, never about content.

The gap table those twelve constitute was described, in an errata issued three days earlier, as one that “should be regarded as unverified until a clean build is reported.” It is reported. What changed is not the theorems, most of which were sound; it is that the claim now stands downstream of a machine anyone can re-run, rather than upstream of a comment. That is the entire distance this paper is about, and it is one line of Lake configuration wide.