16 Axiom Inventory

16.1 Mathematical Axioms

1. arithmetic_admissibility — Meyer spectral-Weil (2005). Sole remaining gap for unconditional RH. Requires: adèlic Fourier analysis, explicit formula, Weil positivity. Partially addressed by SpectralWeil.lean.

2. riemannZeta_conj_axiom — \(\zeta (\bar s) = \overline{\zeta (s)}\). Provable from Dirichlet series + analytic continuation; not named in Mathlib 4.19.0.

3. schwartz_integral_clm_exists — \(\phi \mapsto \int \phi \) is CLM on \(\mathcal{S}\). Provable once SchwartzMap.integralCLM exists in Mathlib.

4. exp_growth_not_tempered — \(e^{au}\) (\(a \neq 0\)) is not a tempered distribution. Provable once SchwartzMap.tendsto_shift + Gaussian integral exists in Mathlib.

5. link6_from_physics — \(c_{2D} = \kappa _0 \cdot c_{4D}^{\mathrm{Weyl}}\). Physics derivation from Weinberg soft theorem + Cachazo-Strominger OPE + Capper-Duff anomaly + Adler-Bardeen non-renormalization.

16.2 Physics Axioms (New — Celestial Holography)

1. weinberg_soft_tree — Weinberg soft graviton theorem.

2. cachazo_strominger — Cachazo-Strominger celestial OPE.

3. capper_duff_one_loop — Capper-Duff one-loop Weyl anomaly.

4. adler_bardeen_nonrenorm — Adler-Bardeen non-renormalization.

5. boyle_turok_2021 — \(c_{4D}^{\mathrm{Weyl}} = 0 \Rightarrow n_{\mathrm{gen}} = 3\).

16.3 Infrastructure Axioms (new files)

1. peter_weyl_K1, plancherel_K1, spectrum_discrete_K1 — spectral theory of \(L^2(K^1)\).

2. weil_explicit_formula, meyer_spectral_weil_identity, weil_distribution_positivity — Weil explicit formula.

3. shadow_breaking_gives_abundance, shadow_unitarity_abundance_pos — DM abundance from shadow breaking.

4. K1_haar_probability, born_from_haar, gleason_uniqueness — Born rule.

5. lovelock_theorem, shadow_forces_massless_graviton, c0_eliminates_higher_curvature — Einstein rigidity.

6. celestial_amplitude_has_cut, disc_equals_loop_integrand, shadow_disc_mellin_density — shadow discontinuity.

16.4 Infrastructure Sorries (non-mathematical gaps)

1. adelic_quotient_compact_factor — Fujisaki’s lemma. Requires adèle ring topology in Mathlib.

2. tate_functional_equation — Tate’s thesis. Requires Schwartz-Bruhat functions on adèles.

3. gamma_reflection_half — \(\Gamma (s/2)\Gamma (1-s/2) = \pi /\sin (\pi s/2)\). Substitution form of reflection formula; provable with Mathlib Gamma API.

4. penrose_antipodal_from_hodge — Penrose twistor correspondence. Not in Mathlib.

5. l2_shadow_eigenvalue_forces_critical_re — Peter-Weyl on \(K^1\). Requires Hecke character theory in Mathlib.

6. K1_compact_haar — Fujisaki’s lemma (adèlic form). Requires Mathlib.NumberTheory.NumberField.Adeles.

7. hurwitz_classification — Hurwitz theorem. Not yet in Mathlib 4.19.0.

8. l_infty_subset_l2_compact — \(L^\infty \subseteq L^2\) on finite measure spaces. 1 sorry: integral_mono with nnorm bound absent in Mathlib 4.19.0.