A research programme on one involution — the shadow map — that appears in celestial holography and in the functional equation of the zeta function, developed from self-dual Haar measure on (ℝ⁺, ×) and checked, where possible, by a proof assistant.
dμ(ω⁻¹) = dμ(ω) on (ℝ⁺, ×) — the organizing fact. What follows from it is sorted below into verified, argued, and open.
4D flat-space quantum gravity dual to a 2D CFT on the celestial sphere. The shadow map Δ ↔ 2−Δ is identified with time reversal and with the functional equation. Verified: the dictionary. Conditional: the central-charge statements, which carry their physical inputs as explicit hypotheses.
Under Δ = 2s, celestial unitarity and the critical line Re(s) = ½ are the same locus. The framework reduces RH to a single positivity statement through machine-verified equivalences and develops five routes to it. See the Riemann page.
A constructive route to a Yang–Mills mass gap, M = 2N/(k+N)·ΛQCD, via Haar orthogonality on the celestial sphere. The Clay problem asks for a 4D theory satisfying the axioms with a gap; this is the GPP route to it.
A proposed treatment of Penrose's googly problem: with shadow = T, the self-dual and anti-self-dual sectors are T-conjugates. Verified: shadow = T in the model. Argued in manuscript: the full twistor construction of Einstein gravity.
SU(3)×SU(2)×U(1), three generations and sin²θW = 3/8 as consequences of the division-algebra tower ℝ→ℂ→ℍ→𝕆, with Hurwitz's theorem as the stopping condition. Status: a structural proposal with physical inputs as explicit hypotheses; the three-generation statement is an open placeholder in the formalization.
The Fixed-Point Paradox is an argument, via Lawvere's fixed-point theorem, that Counterfactual Freedom is incoherent under stated definitions, bearing on both libertarian free will and hard determinism. A philosophical result, offered for critical examination.
The framework is being mechanically verified in Lean 4 + Mathlib. The tree has zero sorry and zero custom axioms, and results that are not yet proved are kept as named, counted placeholders so that “0 sorry” cannot be mistaken for “everything proved”. Machine-checked results include:
shadow_equals_time_reversal — shadow = time reversalcritical_line_is_fixed_locus — the shadow map fixes exactly Re(s) = ½rh_iff_weil_pairedForm_nonneg — RH ⟺ Weil-form positivityriemannHypothesis_iff_P_minus — RH ⟺ vanishing of the odd part of every zerotemperedness_iff_critical_line — eau is tempered iff a = 0Stated as open, not assumed: the L² constraint on the idèle class group, the three-generation count, and anomaly cancellation. Each is a named placeholder in the formalization.
"Every theorem that compiles with zero sorries has been checked by a machine that does not accept hand-waving."
Live Proof Dashboard →979-page monograph presenting the full framework: the three-step Haar→shadow derivation, a topological 4π argument, and the shadow bundle construction. The Lean formalization tracks which parts are machine-verified.
Shadow = T from first principles and a Yang–Mills twistor datum: a resolution of Penrose's googly obstruction in 14 pages. The shadow = T step is verified in Lean.
A constructive route to a Yang–Mills mass gap for compact simple gauge groups.
The Haar-measure argument for Re(s) = 1/2 in full, with the L² constraint on the idèle class group at its centre.
2500 Years of Debate Ends Here
Through formal arguments, Daniel Toupin contends that libertarian free will is logically impossible — even for gods — and that hard determinism collapses into compatibilism. What emerges is complete resolution: You are caused. You are free. Both are true.
Buy on Amazon → View in Store →Correspondence welcome.
dtoupin@goldenphysics.org ORCID ↗This research is independently funded. If you find the work valuable, your support keeps it going.
☕ Support the Research