WP-91 · A Theorem Twenty-Seven Characters Long

Cloning sluing/neuro on macOS produced a warning about colliding paths. Following it led to two tracked files whose names differ only in case, then to the theorem they both contain, then to the published registry entry for that theorem. The registry says collatz_converges is proved. The proof is hasStructuredCycle_collatz X — twenty-seven characters invoking an axiom declared eleven lines above it, whose statement is the Collatz conjecture. The file's own comment says so.

DEFECT published claim, reproducible MEASURED produced by the instrument READ read from source, quoted OPEN not settled here

§1

The pair, and which is canonical READ

Three tracked names, two contents:

path	bytes	axioms	theorems	documented
DiscreteDM3.lean	2,732	4	4	no header, no comments on the axioms
discreteDm3.lean	6,511	4	4	module header naming the axioms as the conjecture
discretedm3.lean	6,511	4	4	byte-identical to the above

APFS is case-insensitive, so a macOS checkout holds one of these and reports the survivor as modified against the index entry for its sibling. Committing that apparent modification overwrites one tracked file with another's content. That is the hazard; it is not the finding.

The canonical file is discreteDm3.lean

Not because it is larger, and not on any sorry count — neither file contains a sorry. Both declare four axioms and four theorems, and the mathematics is the same. The difference is entirely in what each one tells the reader.

discreteDm3.lean carries a module header stating that its three analytic axioms are the Collatz conjecture, marks hasStructuredCycle_collatz as "the Collatz conjecture itself", annotates collatz_converges as "as strong as the axiom it rests on", and proves the even branch of M_collatz_iff_E_collatz before isolating the odd branch as a named private axiom with its reason.

DiscreteDM3.lean is the same file with the header deleted, the annotations deleted, and M_collatz_iff_E_collatz demoted from a partially proved theorem to a bare axiom. It is a caveat-stripping regression, and it is the copy the published registry links to.

§2

What the registry says DEFECT

Read from the tracked pages on 2026-09-01:

AXLE/theorem-registry.html <div class="thm" data-st="proved"><span class="b b-proved">✓</span>collatz_converges</div>

geometry/neuro/SBM/1080.html <tr data-tier="free" … ><span class="badge bf" title="Sorry-free in source — proof written, no unproved step">S</span> … collatz_converges … DiscreteDM3.lean ↗

Against the source:

axiom hasStructuredCycle_collatz : ∀ X, ∃ n, collatzStep_dm3^[n] X = attractor theorem collatz_converges (X : CollatzState) (_hX : isSimplyConnected X) : ∃ n : ℕ, collatzStep_dm3^[n] X = attractor := hasStructuredCycle_collatz X

The badge tooltip — "proof written, no unproved step" — is false for this entry. The unproved step is the axiom, and the tiering treats an axiom as not-a-step. Both statements are individually defensible and their conjunction publishes the Collatz conjecture as a machine-verified theorem. This is the failure mode the corpus already names in CLAUDE.md: sorry-free is not proved.

And it is counted twice

MEASURED AXLE/directory.html carries collatz_converges at entry 357 (from DiscreteDM3.lean) and again at entry 773 (from lean/discreteDm3.lean); 1080.html lists it at 356 and 773. The case-collision is therefore not only a git hazard — it inflates a published declaration count by duplicating the same theorem under two spellings. The same applies to entropy_monotone and M_collatz_iff_E_collatz.

§3

Neither file compiles MEASURED

Both import Mathlib.Init.Function. Checked against the v4.32.0 build at geometry/.lake/packages/mathlib on 2026-09-01:

import	present in the v4.32.0 build
Mathlib.Init.Function	ABSENT
Mathlib.Data.Nat.Basic	present
Mathlib.Data.Nat.Factorization.Basic	present

So the "sorry-free in source" badge was determined by parsing the text, not by building it. tools/axiom_gate.py — the real gate, which asks the kernel via #print axioms — cannot see either file, because a file that does not elaborate has no axioms to report. The declarations least able to be checked are the ones the gate is structurally blind to, and they are scored by the instrument that cannot tell an axiom from a proof.

§4

How much of the corpus is like this MEASURED

Measured 2026-09-01 by tools/axiom_dependence.py over the roots declared in tools/corpus_roots.txt, 10 of 11 readable (io-clone was not reachable), 264 tracked .lean files:

figure	count
axiom declarations	61
theorems / lemmas whose body names a locally declared axiom	27
…of which the body is a pass-through (≤ 80 non-space chars)	10

The ten pass-throughs, shortest first:

chars	declaration	rests on	file
25	entropy_monotone	meanContraction_collatz	AXLE/discreteDm3.lean
25	entropy_monotone	meanContraction_collatz	AXLE/discretedm3.lean
27	collatz_converges	hasStructuredCycle_collatz	AXLE/discreteDm3.lean
27	collatz_converges	hasStructuredCycle_collatz	AXLE/discretedm3.lean
47	critDim_3	nBonacciRingSize_3	GTCT/dm3CriticalityPrinciple_extended.lean
47	critDim_4	nBonacciRingSize_4	GTCT/dm3CriticalityPrinciple_extended.lean
64	entropic_cost_minimal_at_rank3	nBonacciRingSize	GTCT/dm3CriticalityPrinciple_extended.lean
67	igcp_3	dm3_criticality_principle	AXLE/CatGT/Criticality_Principle.lean
69	tribonacci_3_critical	dm3_criticality_principle_instance	GTCT/dm3CriticalityPrinciple_extended.lean
77	super	dm3_criticality_principle	AXLE/CatGT/Criticality_Principle.lean

The seventeen longer ones are questions, not defects — a long body naming an axiom may contain real work, and several plainly do. They are listed in the tool's output and should be read once each, not swept.

The instrument cannot see the file the registry links to

Run on macOS, the scan finds discreteDm3.lean and discretedm3.lean but not DiscreteDM3.lean, because the case-collision means only one is in the working tree. The registry's link points at the one the scan cannot open. Any count of this population taken on a Mac is short by the hidden siblings; see Finding 3 in docs/leanscan-2026-09-01.md.

§5

What is not claimed

No accusation of fabrication. discreteDm3.lean states its axioms and their status plainly, in its own header, in more detail than most files in the corpus. The defect is that the registry's tiering discards that honesty on the way to a badge, and that a second copy of the file deleted it at source.
Axiomatising the conjecture is a legitimate move. Stating "if Collatz holds in this form, the dm³ closure gives convergence" is a real thing to formalise. What cannot follow is a registry row reading ✓ proved.
The 61 / 27 / 10 figures are source-level. They come from a regex scan, not from the kernel. They cannot see axioms imported from other modules and do not resolve namespaces. The authoritative instrument is #print axioms, which is blind to every file that does not elaborate — which is why this tool exists alongside it, not instead of it. OPEN
No corpus-wide recount is published here. Changing the tier of these entries changes totals on several pages; under the house rule that is a census re-run and a diff, not an edit. OPEN

§6

Repairs, in order

Retier the registry. "Sorry-free in source" needs a fourth state for rests on a local axiom. Ten declarations are pass-throughs today; the tooltip "proof written, no unproved step" must not apply to them. This is the change that touches published counts.
Retire DiscreteDM3.lean in favour of discreteDm3.lean, and delete discretedm3.lean as a byte-identical third spelling. The retired copy goes to docs/ml-evidence/ — it is the evidence that the caveats were removed somewhere between the two, which is a finding about machine-assisted production and not junk.
Repoint the registry link from DiscreteDM3.lean to the canonical file, and collapse the duplicate entries (356/357 and 773).
Fix or retire the imports. Mathlib.Init.Function no longer exists; until it is dropped, neither file can be gated and no badge on either is evidence of anything a machine checked.
Add the case-collision check to CI. One line — compare git ls-files against its case-folded set — would have caught this before it reached a published count. OPEN

Falsifiers

§1 fails if the two files differ in some way this page missed — both are short and are quoted from directly. §2 fails if the registry markup has changed since 2026-09-01; the two lines are quoted verbatim and are greppable. §3 fails if Mathlib.Init.Function is present under some other path in the build. §4 fails if the scan's regex misattributes a body; the ten flagged rows are short enough to read in full, which is the point of sorting by length.

References

tools/axiom_dependence.py — the instrument. Source scan; run 2026-09-01.
tools/axiom_gate.py — the kernel gate, via #print axioms. Authoritative where a file elaborates.
docs/leanscan-2026-09-01.md, Finding 3 — the case-collision and what it does to any count taken on macOS.
tools/corpus_roots.txt — the declared root set these figures are taken over.
WP-80 · The Theorem and the Reader — the position that a count of declarations must exclude the author and the production pipeline. This page is an instance: the badge counted a reader who was never there.