26 Axiom Inventory

Re-audited 2026-08-30 directly against the source tree (grep -rn "^axiom " GppVerify/) rather than carried forward from an earlier snapshot. There is now exactly 1 custom axiom in the repo, down from 13.

What changed. Twelve of the thirteen were not mathematical gaps at all. Eleven declared physical observables (\(c_{2D}\), \(c_{4D}^{\mathrm{Weyl}}\), \(n_{\mathrm{gen}}\), \(\kappa _0\), \(\Omega _{DM}\), the shadow-breaking scale) or cited external physics results (link6_from_physics, boyle_turok_2021); a twelfth (hurwitz_division_algebra_dimensions) was consumed by no theorem at all. A global axiom is the wrong mechanism for a physics input: it silently propagates into the axiom trace of every downstream result, whether or not the reader is looking. All eleven are now carried as explicit hypotheses on the theorems that use them, so the conditionality is visible in each statement and the theorems audit clean; the unused one was retired outright, its statement kept as a hypothesis-shaped Prop. No mathematical content was weakened, added, or removed — the deduction \(c_{2D}=0 \Rightarrow n_{\mathrm{gen}}=3\) was always conditional on its physics inputs, and now says so in its own type.

26.1 Physics Inputs (now hypotheses, not axioms)

These name a physical observable, or a cited external physics result. None is a mathematical gap, and none is an axiom any more: each is a universally quantified variable or an explicit hypothesis on the theorems that consume it.

1. \(c_{2D}\), \(c_{4D}^{\mathrm{Weyl}}\), \(n_{\mathrm{gen}}\), \(\kappa _0\) — the 2D celestial-OPE central charge, the 4D graviton-self-energy Weyl anomaly coefficient, the number of fermion generations, and the canonical-OPE normalisation. CelestialHolography/Link6.lean

2. link6_from_physics — \(c_{2D} = \kappa _0 \cdot c_{4D}^{\mathrm{Weyl}}\) (thm:link6), now the named hypothesis link6. Its intended route is four QFT inputs (Weinberg soft theorem, Cachazo–Strominger celestial OPE, Capper–Duff one-loop anomaly, Adler–Bardeen non-renormalization), each parked in the file as a True-stub with a doc comment naming the input; thm:link6 is not derived from those stubs, since a vacuous statement derives nothing.

3. boyle_turok_2021 — \(c_{4D}^{\mathrm{Weyl}}=0 \Rightarrow n_{\mathrm{gen}}=3\) (Boyle–Turok 2021), an uncited external analysis; now the named hypothesis boyle_turok. Link6.lean

4. \(\Omega _{DM}\) — observed dark matter abundance (Planck 2018: \(\Omega _{DM}h^2 \approx 0.12\)); its \((0,1)\) range is the hypothesis omega_observed. StandardModel/DMAbundance.lean

5. The former shadow_breaking_scale / shadow_breaking_scale_pos axioms were deleted rather than converted: no statement anywhere consumed them.

26.2 Mathlib-Gap Axioms

There are none. As of 2026-08-31 this repository contains zero custom axioms.

The last one, exp_growth_not_tempered — \(e^{au}\) (\(a\neq 0\)) is not a tempered distribution — is now proved: RiemannHypothesis/ExpNotTempered.lean. Its only dependencies are propext, Classical.choice and Quot.sound, the three axioms of Lean itself.

The argument: fix a bump \(b\), smooth and supported in the unit ball, and set

so that \(a\, t_n = |a|\, n\) whichever sign \(a\) has. Two facts then collide. First \(\psi _n \to 0\) in \(\mathcal{S}(\mathbb {R},\mathbb {C})\): shifting the bump costs only polynomial growth in each Schwartz seminorm, \((|t_n|+1)^k\), while the scalar decays exponentially — so continuity of \(T\) forces \(T\psi _n \to T0 = 0\). Second, \(T\psi _n\) does not depend on \(n\) at all: translating the bump multiplies the weighted integral by exactly \(e^{a t_n} = e^{|a|n}\), which is what the scalar was chosen to cancel, leaving \(T\psi _n = \int e^{av}b(v)\, dv\) for every \(n\). A constant sequence converging to \(0\) is \(0\), contradicting the positivity of that integral.

This was not possible before the Mathlib 4.33 upgrade. HasCompactSupport.toSchwartzMap is the entry point for every construction in that file and does not exist in Mathlib 4.19.0 — the Schwartz space was available with no way to build a concrete nonzero element of it, which is precisely what this argument needs. The upgrade (2026-08-31) was undertaken partly on the expectation that it would unblock this axiom, and it did.

Retired here: hurwitz_division_algebra_dimensions (Hurwitz’s theorem: the only normed division algebras over \(\mathbb {R}\) are \(\mathbb {R},\mathbb {C},\mathbb {H},\mathbb {O}\), dimensions \(1,2,4,8\)) was retired 2026-08-30. It was applied by zero theorems, and the finite dimension-counting content this repo actually uses is proved without it. Its statement survives as GppSM.HurwitzDimensionHypothesis. Note that Mathlib’s NormedDivisionRing is associative, so the octonions do not inhabit it and the reachable content of that statement is really the Frobenius classification \(\{ 1,2,4\} \) — a mismatch to fix before anyone proves or applies it. StandardModel/ThreeGenerations.lean

26.3 Retired Axioms

Two axioms that appeared in earlier snapshots of this inventory no longer exist in the tree — genuinely eliminated, not renamed:

1. arithmetic_admissibility and its riemann_hypothesis alias — retired 2026-07-17 (commit da2eaf4). It restated RH verbatim as an axiom; superseded by the genuine conditional GppWeilCriterion.rh_of_weil_pairedForm_nonneg (see Theorem 5.5), which derives RH from a stated positivity hypothesis rather than assuming it.

2. schwartz_integral_clm_exists — retired 2026-08-14, now proved via Mathlib’s SchwartzMap.integralCLM.

26.4 The True-Stub Convention (not axioms, not sorries)

Open results are parked as theorem foo : True := trivial (or \(\forall \) (_ : True), True) — the repo’s deliberate convention, carrying a doc comment that names the precise upstream gap, rather than smuggling the claim in as an axiom or leaving a live sorry. There are currently 156 such stubs.

That number was wrong until 2026-08-31, and the way it was wrong is worth recording. This blueprint published 141; the gate reported 142; the tree held 150 — and on 2026-09-01 a third pass found two more, for 152. The gate matched line by line — it remembered the last theorem line, then looked for : True := trivial on a later one — so it could not see a stub written as

theorem shadow_discontinuity :
-- Disc(celestial amplitude) = shadow transform jump = loop integrand
True := trivial

because the line carrying True := trivial has no colon in front of True; the colon is two lines up, behind a comment. Eight stubs sat in that blind spot and all eight were unprefixed — shadow_discontinuity, born_rule_from_haar, K_compact, K_trace_class, plancherel_atom_one, meyer_spectral_weil, adelic_l2_regularization, digamma_series_form. The gate printed “All True-stubs correctly prefixed” on every build while carrying exactly the names it exists to catch. They are now renamed open_…, and the gate reads whole declarations with comments stripped rather than lines, so a stub can no longer hide behind a comment inside its own statement. The gate also now checks this very sentence against the tree, so the published count cannot drift again.

A second hiding place, found 2026-09-01: the reflexivity tautology. Everything above hunts for the conclusion True. That is not the only way to assert nothing. A declaration whose conclusion is X = X for syntactically identical X is equally empty, is discharged by rfl, reports the same spotless axiom bill — and, not being True, walked past every version of the gate. Eleven were in the tree, none prefixed, several carrying the name of a substantive claim:

theorem three_generations : (3 : \(\mathbb {N}\)) = 3 := rfl
lemma test_function_fe_symmetric (h) (rho) : h rho = h rho := rfl
theorem mirror_baryon_lower_bound : (1 : \(\mathbb {N}\)) \(\le \) 1 := le_refl 1
theorem dim_sun (n) (_ : 1 \(\le \) n) : n^2 - 1 = n^2 - 1 := rfl

test_function_fe_symmetric sat under a section header reading “algebraic spectral facts (proved clean)” and was #checked in its file’s summary. three_generations — the framework’s headline Standard-Model prediction, and the \lean{} target of Theorem 13.2 — said “OPEN PROBLEM” in capitals in its own docstring while being proved by reflexivity on a numeral. mirror_baryon_lower_bound is the sharpest case: it began as an axiom and a June 2026 session recorded it as closed by restating it as 1 \(\le \) 1, which is strictly less honest than the axiom it replaced, since an axiom at least appears in #print axioms.

Five of the eleven had real content available and now state it (the shadow map’s involution \(2-(2-\Delta )=\Delta \); sesquilinearity’s conjugate-linear half; the functional-equation partner map’s involutivity and its fixed-point characterisation of the critical line; the Gr(2,4) point count’s middle coefficient; and \(\dim SU(n)\) in the one form that consumes its own hypothesis, \((n^2-1)+1 = n^2\), false at \(n = 0\)). The other six became open_ stubs and are included in the count above — which is why it rose to 156 while a stub was simultaneously closed by proof. The gate now rejects any declaration whose two sides are character-for-character identical, so this class cannot recur either.

It took a third pass to get right. On 2026-09-01 two further unprefixed stubs surfaced: thm_universal_shadow_product (\(\forall \) (_ : \(\mathbb {C}\)), True := fun _ => trivial) and scaling_eigenspace_ode. Both were invisible because the gate still keyed on the binder being literally True and the proof being literally the token trivial. Neither is what makes a declaration vacuous — the conclusion is. The pattern now matches a True conclusion under any binders with any by/fun/intro boilerplate, and is built as a union with the previous pattern: an intermediate "cleaner" rewrite silently dropped four stubs written as by intro _ then trivial on the next line, so widening is now done additively by construction. Five shapes are negative-tested.

One stub was then closed by proof rather than by counting. open_prop_ratio_identity recorded its own gap as “follows from open_thm_shadow_euler by division (unconditional)” — that is, the only missing ingredient was the universal shadow product, and the step from it to the ratio identity is arithmetic. That step is now proved as , with the product supplied as an explicit hypothesis rather than assumed globally, together with for the \(SU(3)\) specialisation at the coupling \(a = 1/4\) that shadow_coupling_su3 already proves correct.

This is the same move that retired twelve physics axioms in Link6/DMAbundance: a claim parked as a vacuous True becomes a real theorem whose input is visible in its own signature. The hypothesis function is deliberately arbitrary — nothing presumes it is the Hadamard product, only that \(\xi \) normalised at \(1/2\) agrees with it. Establishing that remains open.

The file header of ShadowEulerIdentity.lean also described three of these stubs as axioms. They are not. An axiom asserts its statement and downstream results may depend on it; a True-stub asserts nothing and nothing can depend on it. Calling a stub an axiom overstates it in both directions at once. Corrected.

Every stub name now begins with open_, and CI enforces it (scripts/check_stub_naming.py, wired into build.yml as a failing gate). This closes a real hazard rather than a cosmetic one. A stub is inert and cannot corrupt a proof, but it reports “does not depend on any axioms” — the cleanest possible bill of health — while asserting nothing. Until 2026-08-30 the tree therefore contained, among others,

Millennium-Prize-scale problems and major open results wearing the names of the theorems they are not, in a repository advertising zero sorries and zero axioms. None was referenced by any real content, so nothing unsound was ever derived from them — but a reader grepping the source could reasonably have concluded otherwise. The renaming makes the hazard structurally impossible: open_yang_mills_mass_gap cannot be misread, and the gate rejects any future stub that omits the prefix.

This remains the single most important caveat for reading this repo: a file containing only stubs reports zero sorries and zero axioms while asserting nothing. The full per-file, per-thread ledger (which stub covers which named gap, and the plan for closing it) lives in docs/FORMALIZATION_PLAN.md, not in this blueprint; it is updated in the same PR that advances any thread.

Sorry count: 0. Enforced by a dedicated CI gate on every push (.github/workflows/build.yml). Declarations named in earlier snapshots of this chapter as carrying a live sorry have each since been resolved — closed with a real proof, converted to a named axiom above, or converted to a True-stub.