Dependencies

\(\tfrac {\varepsilon }{2}\int _{\mathbb R} e^{-\varepsilon |u|}\, du = 1\) exactly, for every \(\varepsilon {\gt} 0\).

Every \(L^2\)-admissible non-trivial zero \(\rho \) of \(\zeta (s)\) satisfies \(\mathrm{Re}(\rho ) = \tfrac {1}{2}\).

Dark energy (cosmological constant \(\Lambda \)) is the only free parameter in the gravitational action consistent with shadow symmetry.

\(c_{2D} = 0 \Rightarrow c_{4D}^{\mathrm{Weyl}} = 0 \Rightarrow n_{\mathrm{gen}} = 3\) (Boyle–Turok 2021).

The three Cayley–Dickson doublings \(\mathbb {R}\to \mathbb {C}\), \(\mathbb {C}\to \mathbb {H}\), \(\mathbb {H}\to \mathbb {O}\) correspond to exactly \(3\) fermion generations.

\(\xi (s) = \tfrac {1}{2} s(s-1) \pi ^{-s/2} \Gamma (s/2) \zeta (s)\).

The \(L^2(\mathbb {A}^\times /\mathbb {Q}^\times )\) spectral decomposition is well-defined after Haar regularization:

1. \(K^1\) compact \(\Rightarrow \) finite Haar measure \(\Rightarrow \) \(L^\infty \subseteq L^2\)

2. Peter-Weyl on \(K^1\): \(L^2(K^1) = \bigoplus _\chi \mathbb {C}\cdot \chi \)

3. Plancherel: \(\| f\| ^2 = \sum _\chi |\hat f(\chi )|^2\)

Algebraic core proved: l_infty_subset_l2_compact (1 sorry: integral_mono with bounded functions, Mathlib 4.19 gap). Three axioms: peter_weyl_K1, plancherel_K1, spectrum_discrete_K1.

The Born rule \(P(\psi ) = |\langle \phi |\psi \rangle |^2\) arises as the unique probability measure on \(L^2(K^1)\) induced by Haar measure and Gleason’s theorem.

Proved clean: Haar measure gives a probability measure on \(K^1\); \(\| f\| ^2 = \int |f|^2 d\mu \) normalizes to \(1\). Axioms: K1_haar_probability, born_from_haar, gleason_uniqueness (Gleason 1957, not in Mathlib).

For \(\sigma \neq 1/2\), the symmetric Cesàro mean \((\int _{1/R}^{R} r^{2\sigma -2}\, dr)/(2\log R)\) tends to \(+\infty \) as \(R \to \infty \). Together with the exact value \(1\) at \(\sigma = 1/2\) (born_rule_cesaro), this makes \(\sigma = 1/2\) the unique locus where the inversion-invariant mean is finite and nonzero.

If \(\mathrm{Re}(\rho ) \neq \tfrac {1}{2}\) then \(1-\bar\rho \neq \rho \).

\(s = 1-s \iff \mathrm{Re}(s) = \tfrac {1}{2}\).

The norm-\(1\) idèle class group \(K^1\) is compact (Fujisaki’s lemma, Weil 1974, Ch. IV §2).

Let \(G\) be a compact second-countable topological group, \(\mu \) a Haar measure, and \(\phi : G \to G\) a bicontinuous group automorphism. Then \(\phi _*\mu = \mu \).

The only normed division algebras over \(\mathbb {R}\) are \(\mathbb {R}\), \(\mathbb {C}\), \(\mathbb {H}\), \(\mathbb {O}\) (Hurwitz 1898). There are exactly \(3\) Cayley–Dickson doublings.

Gap: full Hurwitz theorem not yet in Mathlib 4.19.0.

If \(\overline{s} = 1 - s\) then \(\mathrm{Re}(s) = \tfrac {1}{2}\).

For \(s = \tfrac {1}{2} + i\gamma \), the character \(a \mapsto |a|^{s-1/2}\) has absolute value \(1\).

For \(s \in \mathbb {C}\), \(1 - s = s \iff \mathrm{Re}(s) = \tfrac {1}{2}\).

If \(\xi (\rho ) = 0\) then \(\xi (1-\rho ) = 0\).

If \(\zeta (\rho ) = 0\) then \(\zeta (1-\rho ) = 0\).

For \(|\alpha | {\lt} \varepsilon \): \(\tfrac {\varepsilon }{2}\int _{\mathbb R} e^{-\varepsilon |u|}e^{\alpha u}\, du = \varepsilon ^2/(\varepsilon ^2 - \alpha ^2)\).

On any compact topological group, \(\phi _*\mu = \mu \) for \(\phi = (-)^{-1}\). Instance: \(\mathbb {A}^\times /\mathbb {Q}^\times \) with Haar measure \(d^\times a\) satisfies \(d^\times (a^{-1}) = d^\times a\).

With \(c_{4D}^{\mathrm{Weyl}} = 0\) and SM gauge group, anomaly cancellation (Boyle–Turok 2021) forces \(48 = 16 \times 3\) Weyl fermions, i.e., \(n_{\mathrm{gen}} = 3\).

Under \(\Delta = 2s\), shadow \(\Delta \leftrightarrow 2-\Delta \) is the functional equation \(s \leftrightarrow 1-s\).

\(\mathrm{Re}(\Delta ) = 1\) under \(\Delta = 2s\) gives \(\mathrm{Re}(s) = \tfrac {1}{2}\).

If \(c_{2D} = 0\) (shadow unitarity), then the dark matter relic density \(\Omega _{\mathrm{DM}} {\gt} 0\).

Physics: shadow symmetry breaking generates the DM mass scale; unitarity of the shadow amplitude fixes the abundance. Formalized via axioms shadow_breaking_gives_abundance and shadow_unitarity_abundance_pos.

Under \(\Lambda \mapsto \Lambda ^\perp \), the symplectic normalisation forces \(\omega \mapsto \omega ^{-1}\).

\(2^{1-s} = 1\) iff \(s = 1 - 2\pi i k/\log 2\) for some \(k \in \mathbb Z\); every such zero has \(\operatorname {Re} s = 1\) (GppCompletedEta.eta_periodic_zero_re), outside the open critical strip.

\(\xi (s) = \xi (1-s)\) for all \(s \in \mathbb {C}\) away from poles. This is the arithmetic shadow symmetry.

The shadow involution \(\phi : g \mapsto g^{-1}\) preserves the Haar measure on any compact group (instance: \(\mathrm{Gr}(2,4)\)).

If \(\chi _s \in L^2(K^1)\) is an eigenfunction of the shadow involution \(T: a \mapsto a^{-1}\), then \(\mathrm{Re}(s) = \tfrac {1}{2}\).

The proof assembles: Haar self-duality \(\Rightarrow \) \(T\) preserves \(L^2\); Plancherel on \(K^1\) \(\Rightarrow \) \(T\)-eigenvalue is unitary; unitarity \(\Rightarrow \) \(\mathrm{Re}(s) = \tfrac {1}{2}\).

Adèlic infrastructure (Hecke characters, Peter–Weyl on \(K^1\)) awaits Mathlib.NumberTheory.NumberField.Adeles.

The celestial central charge \(c_{2D}\) equals \(\kappa _0\) times the Weyl anomaly \(c_{4D}^{\mathrm{Weyl}}\).

Formalized: The identity is asserted as axiom link6_from_physics with four supporting physics axioms: Weinberg soft graviton theorem, Cachazo-Strominger celestial OPE, Capper-Duff one-loop Weyl anomaly, Adler-Bardeen non-renormalization. The algebraic corollary link6_corollary (\(c_{2D} = 0 \iff c_{4D}^{\mathrm{Weyl}} = 0\)) is proved clean.

The orthogonal complement \(\Lambda \mapsto \Lambda ^\perp \) on \(\mathrm{Gr}(2,4)\) acts as the antipodal map on \(S^2\) via the Penrose correspondence.

\(L^2(K^1, d^\times a)\) decomposes into finite-dimensional irreducibles, so any left-invariant self-adjoint operator on \(L^2(K^1)\) has discrete spectrum.

If the Weil/Yakaboylu paired form is positive semidefinite on every finite subset of the nontrivial zero set, then every non-trivial zero of \(\zeta (s)\) satisfies \(\mathrm{Re}(s) = \tfrac {1}{2}\).

Status: the former arithmetic_admissibility axiom (which asserted RH verbatim) is retired. The conditional above is proved with no axioms beyond Mathlib’s built-ins; the open analytic content is the positivity hypothesis (explicit formula / operator compression).

Every nontrivial zero lies on the critical line iff the paired form is positive semidefinite on every finite subset of the nontrivial zero set. A rigorous reduction — not a proof of RH: the analytic input that would discharge the positivity hypothesis is not claimed.

The Einstein field equations \(G_{\mu \nu } = 8\pi G T_{\mu \nu }\) are uniquely determined by:

1. Shadow symmetry \(\Delta \mapsto 2-\Delta \) (diffeomorphism covariance),

2. Two-derivative truncation (\(c_{4D}^{\mathrm{Weyl}} = 0\)),

3. Positive energy (Weyl anomaly positivity).

Algebraic core proved: graviton_shadow_dimension: \((2:\mathbb {Z}) - 2 = 0\) (by decide); lovelock_uniqueness_algebraic: trivial stub.

Axioms: lovelock_theorem (Lovelock 1971), shadow_forces_massless_graviton, c0_eliminates_higher_curvature.

\(\int _0^\infty u/\cosh ^2 u\, du = \log 2\) — that is, \(\eta (1) = \log 2\) in Mellin disguise, proved with no series interchange via the explicit antiderivative \(u\tanh u - \log \cosh u\).

On the principal series \(\Delta = 1+i\lambda \), time reversal \(T\) sends \(\Delta \mapsto 2-\Delta \): the shadow transform. (Most-cited result in ONON52: 16 cross-references.)

The discontinuity of a celestial amplitude across the shadow cut \(z \mapsto \bar{z}\) (i.e., \(\Delta \mapsto 2-\bar\Delta \)) equals the loop integrand, replacing Feynman diagrams with analytic continuation.

Proved clean:

• \(\mathrm{Disc}\, f(x) = 2i\, \mathrm{Im}\, f(x)\) (basic complex analysis).

• Shadow is an involution: \(2-(2-s)=s\).

• Shadow equals conjugate on principal series \(\Delta = 1+i\lambda \).

• Residue at simple pole: algebraic identity.

Gap: celestial amplitude theory, unitarity cut equations, celestial OPE (not in Mathlib 4.19.0).

The map \(\Delta \mapsto 2-\Delta \) has order \(2\).

The Weil explicit formula expresses \(\sum _\rho h(\rho )\) in terms of local data. Meyer’s (2005) spectral interpretation identifies the adèlic \(L^2\) spectrum with the multiset of zeta zeros, closing arithmetic_admissibility.

Gap: Weil explicit formula and Meyer’s spectral-Weil identity require full adèlic Fourier analysis (not in Mathlib 4.19.0). Documented as three axioms: weil_explicit_formula, meyer_spectral_weil_identity, weil_distribution_positivity.

For any Schwartz-Bruhat function \(\Phi \) on \(\mathbb {A}\): \(Z(\Phi , s) = Z(\hat\Phi , 1-s)\). Follows from Haar self-duality + Poisson summation over \(\mathbb {Q} \subset \mathbb {A}\).

\(e^{au}\) defines a tempered distribution on \(\mathbb {R}\) iff \(a=0\). Two sorries: requires SchwartzMap.tsum not yet in Mathlib.

If \(\zeta (\rho ) = 0\) with \(\mathrm{Re}(\rho ) \neq \tfrac {1}{2}\), there exist at least two distinct zeros with \(\mathrm{Im}(s) = \mathrm{Im}(\rho )\). (Zero sorries, zero axioms.)

If \(Z \subseteq \mathbb C\) is closed under an involution \(\iota \) and the paired form \(\sum _{\rho \in S} \overline{c(\iota \rho )}\, c(\rho )\) has nonnegative real part on every finite \(S \subseteq Z\), then every point of \(Z\) is fixed by \(\iota \).

On the strip \(1 - \varepsilon {\lt} \sigma {\lt} 1 + \varepsilon \): \(\tfrac {\varepsilon }{2}\bigl(\int _0^1 t^{\sigma -2+\varepsilon }\, dt + \int _1^\infty t^{\sigma -2-\varepsilon }\, dt\bigr) = \varepsilon ^2/(\varepsilon ^2-(\sigma -1)^2)\), with value \(1\) at \(\sigma = 1\) and limit \(0\) as \(\varepsilon \to 0^+\) for \(\sigma \neq 1\): the Kronecker-delta selection \(\rho ' = 1-\bar\rho \).

The nontrivial zero set of \(\zeta \) is closed under \(\rho \mapsto 1 - \bar\rho \) — a proved theorem (functional equation composed with the proved conjugation symmetry), not an assumption.