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 Goals, in order of ambition

1. 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.

2. Understand the shadow involution as a single mathematical object rather than as two coincidentally similar symmetries.

3. The Riemann Hypothesis is a major target, and RH Pathway 2 (Spectral/Meyer) is the route developed furthest here — but it is one goal among several, not the thesis of the project. The surrounding tower has value whether or not that pathway closes.

4. Physical consequences of the same involution: CPT and time reversal, complete positivity, three fermion generations, the Einstein equations as a rigidity statement.

1.4 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.5 Coverage caveat

This blueprint is hand-authored; it does not regenerate itself from the Lean source. Substantial proved material therefore exists in the repository without appearing in the chapters below. An audit on 2026-08-31 found 122 of 183 modules with no blueprint reference at all. Chapters are being added as that backlog is worked through, starting with the half-flip/CPT thread below. Absence from this document is not evidence that something is unproved — check the Lean source.