A single “theorems proved” figure would be easier to read and would not be true. These are four distinct claims of decreasing strength, and only the last one is proved in the sense a referee means. Each is regenerable from the command below.
Every theorem / lemma in a git-tracked .lean file across ten
repositories — 259 files. example is anonymous and not counted; comments and
docstrings are stripped before matching, so a theorem named in prose is prose.
40 groups of version-suffixed siblings (AXLE.lean, AXLE_v5_1.lean,
AXLE_v6.lean, AXLE_V8.lean…) collapse to one. The 778-declaration gap is
unreconciled duplication in the repositories — open housekeeping, not lost work.
Every figure below is read against this denominator.
The proof body contains no sorry. This is not the same as proved.
theorem X : True := by trivial is sorry-free and vacuous. 180 grouped
declarations (269 raw) are admitted and are disclosed, never dropped.
Elaborated through Lean’s kernel with a per-declaration #print axioms
reporting exactly [propext, Classical.choice, Quot.sound] — no
sorryAx, no native_decide. This is the only tier that means
verified. Source:
AXLE Theorem Registry,
rebuilt 15 August 2026.
axiom is an assumption, not a
proof; these are counted separately and belong to no tier. The “zero extra axioms” claim
is true of the 30 kernel-audited results, which were probed individually. It has never been
established for the corpus as a whole, and this page does not assert it.
tools/theorem_census.py — scope: git-tracked
.lean only, one checkout per distinct git remote. A copy of the tool and its root
list ships beside this page; the canonical home is
TOTOGT/geometry at
tools/theorem_census.py.
git clone https://github.com/TOTOGT/geometry
cd geometry
python3 tools/theorem_census.py --selftest
python3 tools/theorem_census.py --corpus --tracked
Per-repository declarations written (raw), summing to 2,667:
- F1 Sub-halo density exponent β ∈ [1.4,1.6] vs. CDM β ≈ 1.0 — high-res core imaging
- F2 Convergence peak at r ≈ ε₀·rₙ — JWST Cycle 3 lensing maps
- F3 Core density ρ ∝ M¹⁄³ — archival multi-cluster data
- F4 Magnification excess (1+z)⁰⋅³ — JWST high-z clusters
- F5 χ²/n improvement over CDM with zero free parameters — already demonstrated
- F6 Broken power-law kink at r~0.01R₂₀₀ — JWST NIRCam 3–10 kpc
Pablo Nogueira Grossi · G6 LLC
Newark, NJ · ORCID 0009-0000-6496-2186 · g6llc@proton.me
The dm³ framework is a science of generative transitions — threshold-crossings that cannot be undone. The same four-operator contact-geometric sequence describes helium ignition in stars, autophagy in cells, sub-halo lensing anomalies in galaxy clusters, and the growth phases of a lunar colony.