ersatztv/docs/decisions/records/testing/mutation-claims-are-executed.md

key, title, status, since, supersedes, superseded-by, rule, signals, mechanics

key	title	status	since	supersedes	superseded-by	rule	signals	mechanics
testing.mutation-claims-are-executed	2026-08-22 — a MUTATION grade is EXECUTED every run, from a declared clause, or it is not that grade (#790)	active	2026-08-22	none	none	A `MUTATION` row in `docs/guard-inventory.md` is not a statement that someone once witnessed a red. It carries a DECLARED clause mutation in `scripts/tests/mutation_manifest.py`, and `scripts/tests/test_mutation_harness.py` applies that mutation to an isolated copy of the repository on every run and requires the row's OWN named test to go red. The manifest and the MUTATION rows are compared for SET EQUALITY in both directions, so a row cannot claim the grade without a mutation and a mutation cannot outlive the grade it justifies. EXIT STATUS IS NOT THE VERDICT: each entry also declares the DIAGNOSTIC its red must carry, matched against pytest's exception output alone, because pytest reports a crashing test exactly as it reports a detecting one and a red for an unrelated reason is evidence about nothing. WHERE THE GUARD IS ITSELF A TEST, `target` may differ from `guard` and the exact-once check applies to the declared TARGET. Two shapes are admissible and the choice is not free. Where the guard's assertion IS the check — a completeness comparison against a Markdown inventory — the mutation goes into the guarded ARTIFACT, per `testing.guard-ships-with-mutation-proof`'s checker-guard exception, because mutating such a checker's own POPULATION demonstrates a false POSITIVE while proving nothing about the detection the row claims. Where the guard is a test module wrapping a separately mutable DETECTOR or helper, the clause may be in that detector, since disarming it is a real clause disarm and the module's own assertion is what notices. THE MUTATION IS DECLARED, NEVER INFERRED: a harness that guessed which clause of a 90-line hook is the guard would manufacture the confident-but-empty coverage this exists to prevent, which is why `testing.guard-ships-with-mutation-proof` rejected a generic runner. Where a proof test already names its clause in source, the manifest reuses THAT string, so a retarget in either place is caught by the other. COARSENESS IS RECORDED, NOT HIDDEN: each entry is graded `CLAUSE` or `DETECTOR`, and a `DETECTOR` entry — one whose detector accumulates faults from independent arms, so disarming any single arm leaves its proof test green — must CARRY the finer mutation that survived, which is re-run every time and required to keep surviving. Guards that are not graded `MUTATION` each carry a STATED reason in that same manifest, keyed on the guard and compared for SET EQUALITY against the inventory's `GUARD` rows in both directions — so a new guard cannot arrive without someone writing what a proof would need, and a reason cannot outlive the row it is about. Keying the reason on the row's GRADE instead is tautological (a new guard inherits one and nobody looks at it) and a pinned COUNT moves only on net change; both were tried and are rejected. The sandbox is a real git repository built from `git ls-files` with working-tree content, never a filesystem walk. THE POPULATION IS EVERY DECLARED MUTATION-OUTCOME CLAIM, NOT ONLY THE INVENTORY'S ROWS (ersatztv#881): a sentence asserting that a specific mutation reddens, or does not redden, a named test is the same kind of claim wherever it is written — a code comment, a test docstring, a decision record — and is either a `CLAIMS` entry in `scripts/tests/mutation_manifest.py` that executes every run, or it is not written. A claim entry is keyed on the PROSE rather than on a guard: it carries the tracked `site` and the verbatim `quote`, both checked every run, so a reworded sentence reports as a RETARGET instead of drifting away from the entry that justifies it. THE QUOTE SPANS THE MUTATION AND THE OUTCOME IT ASSERTS: the outcome half is the checkable part, so a quote stopping at the mutation binds the uncontroversial words and leaves the assertion, and the test it names, outside the binding entirely. It declares `RED` or `GREEN`, and GREEN is the half no `MUTATION` row can express — a claim that a mutation is NOT noticed is read by THREE separate clauses, because each alone certifies a run that proves nothing: the run exited 0, something actually PASSED, and the named proof was shown to REACH the mutated clause. THE TWO DIRECTIONS ARE NOT SYMMETRIC, WHICH IS WHY THE THIRD CLAUSE EXISTS ON ONLY ONE OF THEM. A RED claim checks its own relevance for free — a proof that never executes the mutated file stays green and is refused in the same words as a clause that has stopped being load-bearing — while a GREEN claim gets precisely the green it asserts from a proof that reads a different file entirely, so exit status and a passing test TOGETHER still certify a run that never executed the clause. A GREEN entry therefore also declares a SECOND mutation of the SAME clause, required to REDDEN the same proof and carrying its own declared diagnostic, executed through the same red-reading path the inventory rows use; only once that passes is the green evidence about this clause at all. It is worth what the `DETECTOR` survivor was worth: re-run, and required to KEEP surviving. THE REFERENT IS DECLARED, NEVER INFERRED, exactly as the clause is: a checker hunting for sentences that merely SOUND like mutation claims would be a string predicate over prose, which this repo refuses to make load-bearing, so what is enforced is a claim that named its own referent, and the direction that cannot be mechanised — prose that declares nothing — is stated rather than papered over. TWO NEIGHBOURING PROPOSALS ARE SETTLED HERE. A QUOTATION of another file is a claim about that file: adopted, and the `quote` field IS the check, wherever the referent is declared; a general quotation-checker is rejected for the same reason inference is, since a quotation whose referent is unnamed has nothing to resolve. ANCHORING PROSE TO A STATE THE COMMIT ITSELF MOVES ('the last edit to that path', 'the only X that'): rejected as a detector and kept as a phrasing rule. The rejection is measured, and the scan is PINNED IN THE BODY rather than summarised as a figure here, for the same reason the population scan is — a count quoted without the predicate that produced it is the defect this record is about. What it shows is that the shape is indistinguishable BY PATTERN from ordinary rationale ('X is the only thing that can Y'), which this rule carves out, so a detector would fire mostly on prose it must not flag, and an advisory check that does that stops being read. Anchor to a date or a sha under `docs.no-session-narrative`'s dated-measurement clause; inside this rule's own population the anchor is the manifest entry, which is re-executed and therefore cannot go stale.	mutation harness · declared clause not inferred · MUTATION row is executed · set equality manifest vs inventory · CLAUSE vs DETECTOR granularity · surviving finer mutation is re-run · pytest exit code 1 is the only red that counts · every other exit status is rejected · positive control before any mutation · sandbox from git ls-files · paths: `scripts/tests/test_mutation_harness.py`, `scripts/tests/mutation_manifest.py`, `scripts/tests/mutation_harness_lib.py`, `docs/guard-inventory.md` · prose claim bound to its declared site and verbatim quote · GREEN direction executes a claim that a mutation is NOT noticed · a GREEN entry declares a reach mutation proving its proof touches the clause · quotation of another file is a claim about that file · state anchors rejected as a detector, kept as a phrasing rule · issues: #790, #775, #774, #778, #806, #812, #881	The harness builds ONE sandbox per session — tracked files only, from `git ls-files -s`, in an environment with every `GIT_*` variable stripped so an exported `GIT_DIR`/`GIT_COMMON_DIR`/`GIT_CONFIG_*` cannot point its `init`/`add`/`commit` at the real repository — and resets it between mutations with `git reset --hard` TO A BASELINE COMMIT RECORDED OUTSIDE THE REPOSITORY, plus `git clean -qffdx`. Both halves matter: bare `git reset --hard` resets to whatever HEAD is, so a proof test that COMMITS inside the sandbox moves HEAD onto a commit carrying the mutant and every later reset restores it faithfully; and a baseline held as a REF inside the sandbox is one more thing a proof can move. `core.hooksPath`, `commit.gpgsign` and `core.worktree` are pinned on every git invocation for the same reason. The `-ff` removes a nested repository a proof may have left. It runs the full set of named proof tests UNMUTATED first, inside the fixture rather than as a separate test so ordering is a dependency and not a convention. Only pytest exit code 1 counts as red; every other status is rejected. That is what closes the two ways a proof ref goes stale, and they are measured rather than assumed: with an explicit `file.py::function` node id a missing file and a missing function both exit 4, while 5 needs a collection that succeeded and selected nothing. The sandbox skips the `ErsatzTV-macOS` gitlink and recreates the `.claude/skills/jellyfin` symlink as a symlink. `CLAIMS` reuses the same sandbox, the same reset and the same clause application (`_mutate_and_run`, split out so the two directions cannot come to disagree about what a red is worth), and its proof refs join the positive control for the reason the row proofs do, which holds in BOTH directions: over a proof that was ALREADY red, a RED claim is satisfied by redness its own mutation did not cause, and a GREEN claim is REFUSED for a reason that has nothing to do with its mutation — reported as a wrong sentence when what is wrong is the proof. What that control cannot do is see ONE ref that collects nothing — its assertions are over the aggregate of every ref, so the other refs supply the word `passed` — nor ONE ref that collects plenty and touches nothing the claim mutates, which is the larger of the two, since such a proof is green before and after and a GREEN claim would read as verified. Both discriminations are per-claim, in the GREEN direction's own vacuity and relevance gates. THE RELEVANCE GATE RUNS LAST BECAUSE IT IS THE EXPENSIVE ONE: it is the only one of the three that costs a second full run of the proof, under the reach mutation with a sandbox reset between, so an entry the status or the vacuity gate has already refused never pays for it. What keeps the three gates worth three is that each carries its own disarm proof, rather than the position it sits in. The sandbox is reset between a claim's two proof runs, for the reason it is reset between mutations. Each claim's `site` is tested for membership of the git INDEX, not `is_file`, so a claim pointing at an untracked file fails here instead of passing on one machine. Cost, re-measured 2026-09-05 WITH the relevance gate, on an M-series Mac with `-p no:randomly`, whole file, three baseline/branch pairs run back to back: the `CLAIMS` half adds 31.7-43.6%, which is the span of the three pairs and not a rounding of it — 43.6% (46.8s -> 67.2s), 34.1% (50.1s -> 67.2s) and 31.7% (48.9s -> 64.4s), under varying concurrent load. The figure this replaces, 12.7-16.6% measured 2026-09-04, was taken before the GREEN direction had a relevance gate and is retired rather than adjusted: the gate runs a GREEN entry's proof a SECOND time under the reach mutation, with a sandbox reset between, and its three disarm proofs each drive further inner pytest runs. A measurement is a property of the population that produced it, so growing the population invalidates it — re-measure, never scale. Quote the PERCENTAGE rather than the seconds - the absolute figures moved 30% with machine load in one session, and the earlier ~14s here covered fewer entries. The ~4min `script-tests` suite it was measured against is PRE-#870 and no longer holds: that change made `count_pr_mutations` read to its 20-page cap, and `test_pr_changed_files.py` went from 202s to 474s locally (286 -> 294 tests, same machine, `-p no:randomly`, 528383cf3 vs the #870 branch), so the job is roughly double. Re-measure on a runner before quoting a job figure.

What #775 left open, in its own words: "nothing checks that a row claiming MUTATION is telling the truth." It said so deliberately — the bookkeeping half (population, set equality, proof refs resolving to a real def) was mechanised, and the judgement half was left with review. Both cold reviews of #774/#775 came back to the same place: the witnessing had happened once, by hand, and hand-run evidence decays the moment someone edits the guard. Two false MUTATION grades were caught by reading in the first draft, and a third round would likely have found more.

Why a generic runner was rejected, and what changed. #775 rejected a mutation runner for shell hooks on the grounds that it "would have to know which clause of a 90-line hook is the guard". That objection is correct and is not answered by better inference — it is answered by not inferring. The clause is declared, one entry per row, and for most rows the declaration already existed: the proof tests name their own clauses in source (= "efbbbf" ]; then, UNSET_CLAUSE, if [ "$RC" -eq 0 ]; then). Reusing those strings rather than inventing parallel ones is what makes the two halves catch each other's drift.

What a green harness proves, and what it does not. It proves the proof ref names a test that still exists and still collects; that the declared clause still occurs, exactly once, in the entry's declared target, which is not always the guard's own file; and — via the positive control — that every named proof test is GREEN on the unmutated sandbox, so "the mutation was noticed" cannot be confused with "the test was already red". The proofs that carry a disarm of their own run it during that control; the two that are plain production set-equality checks have none, and the harness supplies theirs. It does not prove the declared clause is the only thing the guard hangs on. For three entries (measured 2026-08-22: the BOM guard, build_decisions_catalog.py and prove-fix.sh) the redness arrives through the proof test's own "this clause has moved, RETARGET it" assertion rather than through changed behaviour. That is the intended reading rather than a hole: those tests perform their behavioural disarm themselves on every green run; what they could not do was notice their own clause reference going stale. Every other entry reddens behaviourally, and each one's declared diagnostic says which.

The DETECTOR grade is the honest half, and it exists because measuring found a case. #775's record concedes that neutering pin_population_faults wholesale is "coarser than disarming one clause at a time — coarse enough that a single surviving clause would not be noticed". Running the finer mutations settled which guards actually admit clause-level proof: all but one did at the time, including pin_population_faults, where disarming the against-the-registry comparison alone reddens the proof because a job that loses its container: block leaves the two derived sets equal — and since ersatztv#891 regraded the exception, all of them do. That one did not, and its history is the worked example. instrumentation_faults accumulated from independent arms a stripped hook trips several of at once, so disarming any single arm left the proof test green — measured, by running if not _SOURCES_SINK.search(text): → if False: and watching it pass. The surviving mutation was carried as data and re-run every suite, required to keep surviving.

It stopped being able to, and that is the mechanism working rather than failing. ersatztv#891 replaced the lexical rule over the hook preamble with byte-identity, a clause that decides alone; the entry was regraded to CLAUSE and the survivor dropped. Note the direction: the contract says a survivor that STARTS REDDENING forces a regrade, and this survivor could no longer redden at all — byte-identity necessarily matches the line it tested. A widened clause can retire its own evidence, and a canary whose precondition the fix removes does not fail, it becomes a tautology that reads exactly like a passing proof. So re-derive every proof calibrated against a clause you widen. A grade that cannot decay quietly is the point — including decaying into vacuity.

Three shapes that were tried and rejected, because each looks like verification and is not. Emptying a checker's own population reddens its proof with an IndexError — a crash, not a detection, and any breakage of the derivation satisfies it equally. Shrinking the guard-inventory checker's hook glob reddens its proof by making every real row report as PHANTOM: a false positive, which says nothing about the missing-row detection the row claims. And planting a phantom row in docs/remote-state-inventory.md reddens a proof test that builds a phantom of its own and asserts the difference is exactly one entry — so the declared diagnostic appears through fixture contamination, in the opposite direction from the one the row claims. All three are replaced by artifact-level mutations that reach the guard's production assertion — a deleted inventory row, a renamed one — and expect is what makes the difference visible instead of arguable.

Stating the other guards, and the two cheaper shapes that do not work. Keying the reason on the row's grade is tautological: a new guard graded NONE inherits a sentence automatically and nobody ever looks at that particular guard. Pinning the count of undeclared guards is no better, because it moves only on net change — one guard arriving as another is promoted leaves it unchanged. What ships is a per-guard mapping compared for set equality against the inventory's GUARD rows. That is a hand-maintained table, which is normally the duplication family to avoid (#774's wrong summary counts, #788's verdict vocabulary) — but bidirectional set equality is what makes docs/guard-inventory.md itself safe, and it is what turns "state the ones you cannot declare" into something a new guard cannot slip past. Set equality ALONE is not sufficient and the gap is demonstrable: every comparison here reduces rows through a set or a dict, so a DUPLICATED row is invisible to all of them and a table contradicting itself reports full coverage. Duplicate rejection is a separate, explicit check, and copying the set-equality design without it recreates the hole.

Two words that are not interchangeable. A NONE row means the row nominates no proof; it does not mean the guard is untested. scripts/ci-prove-ban-detects.sh is graded NONE and is driven end to end by test_ci_release_path_scan_job.py, and eight hooks are driven through their deciding path by test_hook_fire_log.py — whose matrix asserts instrumentation TRANSPARENCY, that the wrapped and unwrapped runs agree, never that the decision is right or that a particular clause produced it. A statement that reads "no test drives this" over those guards sends the next session's proof work in the wrong direction, so each entry says which of the two is actually missing.

The population this rule enforces was its first site, and that is what ersatztv#812 fell through. At efadbec29 the manifest's own docstring scoped it to one entry per MUTATION-graded row of docs/guard-inventory.md and nothing else, so a mutation-outcome claim written anywhere else was outside the rule by construction. The anchor is a sha rather than a state, deliberately: this change rewrites that docstring, so an anchor to what the file currently says would be false on arrival. How much else there is, is measured rather than taken from the four defects that prompted this — and the WAY it has to be measured is itself the argument. The scan is a mechanical OVER-APPROXIMATION, and it is pinned VERBATIM rather than described, because a count quoted without the predicate that produced it is the defect this record is about — a number nothing binds to its referent:

git grep -PIc '(?i)\b(disarm|mutat|neuter|delet|remov|replac|flip|strip)\w*\b.{0,80}\b(green|red|redden|pass|fail)\w*\b|\b(green|red|redden|pass|fail)\w*\b.{0,80}\b(disarm|mutat|neuter|delet|remov|replac|flip|strip)\w*\b' efadbec29 -- scripts .claude .gitea docs/decisions web/src ':(exclude)scripts/tests/fixtures' | awk -F: '{f++; n+=$NF} END {print f" files, "n" lines"}'

Run on 2026-09-05 it prints 104 files, 311 lines, against the 27 MUTATION-graded rows the rule reached at that same sha. The sha is baked into the command deliberately: this change adds entries whose own prose the pattern matches — so does this very paragraph, the pinned command included — and the count therefore moves under the commit that records it. A figure quoted for the branch head would decay the moment anything else lands, which is the anchoring failure this rule ends. The hits sit in code comments, in test docstrings, in decision-record bodies and in the manifest's own why fields. Narrow the outcome half to green alone — the same command with both \b(green|red|redden|pass|fail)\w*\b groups replaced by \bgreen\b — and it prints 39 files, 69 lines, the sub-shape whose asserted outcome is that a mutation is NOT noticed — which no MUTATION row can express at all. So the harness had to grow a GREEN direction before the rule could be satisfied for the claims that are of that shape: "declare it or do not write it" is not a rule you can follow when the thing you want to declare is inexpressible. BOTH FIGURES ARE CANDIDATE COUNTS, NOT POPULATIONS, and reading either as a backlog of real claims overstates it: most of the lines are machinery prose or error text — green in the corpus is as often a CI job's colour as a mutation's outcome — and no predicate separates them from real claims, which is exactly why the referent is declared and not detected.

Proposal 3 is a phrasing rule and not a check, and the same kind of scan is what settles that. The shapes it names — "the last edit to that path", "the only X that" — anchor a sentence to a state a later commit can move without touching the words. Over the same corpus at the same sha:

git grep -PIc '(?i)\bthe (only|last) \w+ (that|which|to)\b' efadbec29 -- scripts .claude .gitea docs/decisions web/src ':(exclude)scripts/tests/fixtures' | awk -F: '{f++; n+=$NF} END {print f" files, "n" lines"}'

Run on 2026-09-05 it prints 32 files, 58 lines, and reading all 58 is what decides it, because they are not one kind of sentence. MOST are rationale — which single thing can produce some effect, and why — the class this rule carves out. A FEW are state anchors of exactly the kind proposal 3 is about: at that sha scripts/lib/h10-reviewers.sh and scripts/lib/review-verdict-vocabulary.sh each open a comment with "The ONLY assignment to 1 in this file". And SOME are mutation-outcome claims, reached by accident of a pattern aimed at something else — the mutation table in docs/decisions/records/ffmpeg/watermark-resolution-unified.md, the sentence at web/src/screens/AutoTuneScreen.test.tsx line 174 about what a revert to the old flex row can redden, and test_a_verdict_BEYOND_A_SHORT_PAGE_is_still_found in scripts/tests/test_pr_changed_files.py, whose docstring says an implementation stopping at the first short page would leave every other test in the file passing. HOW MANY OF THAT THIRD KIND THERE ARE IS NOT STATED, and the omission is the point rather than a gap: which side of the line a sentence falls on is a judgement, not a predicate — the AutoTuneScreen line names no test, the test_pr_changed_files.py one names a test SET — so a count here would be a figure the next reader re-derives differently and "corrects", which is the failure this record is about. Three kinds under one pattern is the finding, not a footnote to it: nothing in the string separates them, because the difference is whether the sentence EXPLAINS, ANCHORS or ASSERTS — the same undecidable-by-string-predicate boundary that keeps the referent declared rather than detected. A detector here would fire mostly on prose it must not flag, which is how an advisory check stops being read; the withdrawn test_review_verdict_vocabulary_parity.py is this repo's own case for not building one. The pattern is deliberately wider than the two example phrases: one narrow enough to match only them would report a small figure and establish nothing about the shape.

Extended in place, not given a sibling record — and the choice is the finding. A sibling would have been the cheaper edit and would have recreated the exact defect: a second record scoped to a second site class, with the third site class outside both, which is how #773, #784 and #743 each happened. The rule's subject has not changed — a mutation-outcome claim is executed or it is not written — only its population has, and a record's identity is its rule. A reader resolving testing.mutation-claims-are-executed by key must not have to know a second key exists to get the whole of it. The counter-argument considered was length: this record is already far past the 60-line prose ceiling. That is a formatting pressure, and answering it by forking a key would buy a shorter file with a wider hole.

The seed set found a shipped claim already false, which is the calibration. scripts/post-review-verdict.sh asserted that the array-TYPE test in its read-back was unwitnessable, on the grounds that the absent-entry check below it caught every case on its own — lines 316-317 at efadbec29, which this change replaces. The wording is paraphrased and the source pinned by sha, not quoted, and the reason is the replacement itself: that sentence is not in the tree any more — measured 2026-09-05, git ls-files piped through a fixed-string search for it returns no file — so a verbatim quotation here would resolve to nothing, which is #812's second defect exactly. What disarming that test actually produces is deliberately NOT restated here: it is declared in the CLAIMS entry for scripts/post-review-verdict.sh and re-executed on every run. A dated witnessing written into a decision record is the exact form the rewritten comment beside it rejects, and a second copy of the outcome here would be free to drift from the entry that executes it while both read as checked. Note what the shape costs to detect: the sentence lives in a shell script, its referent is a Python test in another directory, and nothing connected them — so either could be edited without the other showing any sign. Only the SENTENCE was wrong: the test has asserted the shape diagnostic since 5d955000f (#889), and what this change adds beside the rewritten comment is the binding — a RED entry naming both, re-executed every run, which is the state that now decays loudly.

Proposal 4 is not adopted, and the reason is the issue's own argument. Its fourth proposal — prose written to answer a review finding gets the scrutiny a code fix gets — is an exhortation, and the issue makes the case against relying on one better than a summary could: the four defects were written while answering a review finding, "the moment of least slack", which is exactly when a rule you have to remember does not fire. Adding it here would put a review-behaviour clause inside a record whose subject is what executes, and it would be read at the same moment #609's already-recorded advice was not. What replaces it for the shape #812's defects actually took is the mechanism: a mutation-outcome claim written under review pressure is re-executed on the next run whether anyone re-read it or not. For prose that is NOT of that shape, the scrutiny proposal 4 asks for stays where review responsibilities live — docs/defect-shapes-773.md §4 — rather than being restated here.

What this does not reach, stated so it is not read as more. The direction that is mechanised is a declared claim keeps its meaning: the quote must still be there, the mutation must still produce the declared outcome. The direction that is not is every claim is declared — prose that asserts a mutation outcome and declares nothing stays invisible, because finding it means recognising a sentence by its shape, and docs/defect-shapes-773.md §4 names that class — overclaim and stale claim, which no check can tell from a supported sentence — as a review responsibility. That gloss is a paraphrase and §4 is the pinned source. The withdrawn test_review_verdict_vocabulary_parity.py is the empirical case for not trying. So the candidates counted above are a place to look and not a hole this rule closes — nor a backlog, since nobody has established how many of them are claims at all; each real one needs a judgement about whether it is still executable, and declaring them in bulk would manufacture exactly the unverified coverage the rule exists to refuse.

And what the relevance gate leaves, which is narrower than what it closes. The gate proves the named proof EXECUTES the mutated clause and that what the clause computes changes what that proof observes — measured, by a second mutation of the same clause that is declared and required to redden it. What it does not prove is that the proof exercises the particular INPUT the claimed-inert change is about. In the shipped GREEN entry the reach mutation drops the b/ stripping every scanned diff header goes through, while the change claimed inert removes the /dev/null arm, which only a DELETED file reaches — so in general a green of this shape leaves "no test feeds that input" and "the arm changes nothing" indistinguishable. For this entry it is settled by reading the proof: test_a_DELETED_doc_is_not_reported_as_added_content deletes a tracked doc, and a deletion diff under the flags run_diff pins carries a +++ /dev/null header (probed 2026-09-05). That is the shape of what remains — a question about one clause and one proof, answerable by looking — where a green from a proof that touches the file not at all is a green about nothing and is indistinguishable from a verified claim by any amount of reading.