What Is Proved, and What Is Only Written

Tier 1 — the 30 kernel-audited results

These are the theorems that shipped with a per-theorem axiom audit attached to a deposit. All 30 were re-confirmed on disk during this build, with zero sorry in code.

Note the overlap is small. Only 5 of these 30 appear in the registry table below — the rest postdate it, or live in files the registry never indexed. The registry is a June inventory of written work; Tier 1 is a later, narrower, harder claim. They are not the same list and should not be added together.

What this page corrects

An earlier version of this page reported 1,170 entries and 1,080 proved at a 92.3% proof rate, with “zero extra axioms” stated corpus-wide. Those figures do not survive audit and have been withdrawn.

The registry counts one row per (theorem, file) pair. Because the same development was copied across repositories, a single result can appear up to eighteen times — stabilityRadius_eq and nextLevel_layer_count_gt each appear eighteen times. The 1,170 rows below resolve to 586 distinct names. Separately, the deduplicated corpus scan finds 253 distinct files out of 408 .lean files authored here.

The “zero extra axioms” claim is true of the 30 Tier 1 results, which were audited individually. It was never established for the corpus as a whole, and stating it that way was an overreach. Scanning the deduplicated corpus with comments stripped finds 62 axiom declarations, 383 sorry tokens, 5 admit and 17 native_decide — none of which are wrong to have while work is in progress, and all of which make a corpus-wide “zero axioms” statement false.

One correction runs the other way. The June registry marked roughly ninety rows as carrying a sorry. Recomputed against today's files, 0 of the registry's live rows still do — those proofs were finished in the intervening weeks and the registry was never updated. The inventory was stale in both directions.

189 rows cite a file that no longer exists and are struck through below. That is the fault named on the front page of Imaginary Origin No. 3 — a citation that rots — recurring at scale in this author's own registry. They are shown rather than deleted so the correction is visible.

Registry — 1,170 (theorem, file) instances