1 Overview
1.1 What this project is
This blueprint tracks the machine-checked formalization, in Lean 4 with Mathlib, of the shadow framework developed by Daniel Toupin. Every statement marked below has been checked by Lean’s kernel. Everything else is stated honestly as open.
1.2 What it is trying to find out
The organising question is not a single conjecture. It is a correspondence:
Analytic number theory and celestial holography appear to be describing the same object from two sides. What is that object, and how far does the dictionary go?
On the number-theory side sit the completed zeta function \(\xi (s)\), its functional equation \(s \mapsto 1-s\), the idèle class group \(\mathbb {A}^\times /\mathbb {Q}^\times \) with its Haar measure, and the Weil explicit formula. On the holography side sit celestial amplitudes, the principal series, Mellin transforms, and the shadow transform \(\Delta \mapsto 2-\Delta \) on conformal dimensions.
The shared structure is a shadow involution. Under the dictionary \(\Delta = 2s\) it is the same map on both sides, and its fixed locus is exactly the critical line — proved here as GppFE.critical_line_is_fixed_locus: for \(s \in \mathbb {C}\), \(\overline{s} = 1-s \iff \operatorname {Re}(s) = \tfrac 12\). (The involution that matters is \(s \mapsto 1-\overline{s}\), not \(s \mapsto 1-s\); the latter fixes only the single point \(s = \tfrac 12\).)
Because the involution is shared, so are its consequences. That is what makes the correspondence worth formalizing rather than merely asserting: each transfer either survives kernel-checking or fails in a specific, nameable place.
1.3 Shadow holography
The framework reads the shared involution holographically, at three nested levels, each a Mellin or Pontryagin duality and therefore an exact dictionary rather than an analogy.
Line and sphere. The multiplicative line \(\mathbb {R}_+\), split at its fixed point \(x=1\), is the boundary. The spectral sphere, split by the critical line (the equator) into two hemispheres, is its hologram. Inversion \(x\mapsto 1/x\) becomes the reflection \(s\mapsto 1-\overline{s}\), and support on a half-line becomes analyticity on a hemisphere.
Integers as modes. The integers are the Fourier modes of a circle, and Poisson self-duality of that lattice becomes the functional equation.
Primes as a torus. By unique factorization the primes span a compact torus \(\prod _p S^1\) dual to \(\mathbb {Q}_+^\times \), and the critical line embeds in it densely: a hologram inside a hologram.
On the celestial side the same equator is the scale sector, since boosts act on energy by dilation. This is an exact structural parallel. It is not a claim that \(\xi \) is a correlator of a physical theory.
In this language the functional equation says the hologram is symmetric; the Riemann Hypothesis says it is also positive (reflection-positive across the equator). The finite core of that statement is proved (GppHolographicRP.reflectionForm_nonneg_iff: positivity across the equator holds exactly when there are no off-equator mirror pairs). Constructing that positivity for the actual arithmetic distribution is equivalent to RH and remains open.
1.4 Goals, in order of ambition
Map the dictionary precisely. For each object on one side, identify its counterpart on the other, and prove the transfer or name exactly what blocks it.
Understand the shadow involution as a single mathematical object rather than as two coincidentally similar symmetries.
The Riemann Hypothesis as one open question inside the framework: the positivity half of the hologram. Several routes to it have been developed here and several recorded as dead ends; none is the thesis of the project, and the tower has value whether or not any of them closes.
Physical consequences of the same involution: CPT and time reversal, complete positivity, three fermion generations, the Einstein equations as a rigidity statement.
1.5 How to read this blueprint
Results carry when the Lean proof is complete and kernel-checked. A statement without it is open, and the surrounding text says what is missing.
Three categories are tracked separately and never conflated:
sorry — zero, and CI fails the build if any appears.
custom axiom — zero, down from thirteen. The last one, exp_growth_not_tempered, was proved on 2026-08-31 once the move to Mathlib 4.33 made a concrete nonzero Schwartz witness constructible.
True-stubs — open results deliberately parked. Every one is named open_…, and CI rejects any that is not. A file full of stubs still reports “0 sorry, 0 axiom”, so the prefix is what keeps that honest.
What is deliberately not claimed. Nobody proves RH in this repository by accident. The value is that every reduction and constant in the surrounding tower is kernel-checked, with each remaining gap named precisely. Where a route was tried and failed, the failure is recorded rather than quietly dropped.
1.6 Coverage caveat
This blueprint is hand-authored; it does not regenerate itself from the Lean source. Proved material can therefore exist in the repository before it appears in the chapters below. Absence from this document is not evidence that something is unproved — check the Lean source.