Ideas Under Pressure.
Notes on the Shadow Framework, formal verification, celestial holography, spectral theory, quantum gravity, number theory and the parts of the program that still refuse to yield.
Formalization Updates
Current state of GPPVerifyMachine-Checked: The Shadow Framework in Lean 4
The canonical verification page, rewritten to distinguish proved theorems, conditional reductions and deliberately parked open mathematics.
Open status page → NewThe Prime Channel Under the Kernel
The prime as a scattering channel, the self-dual divisor geometry, the exact Schatten threshold, and the routes the kernel has now closed.
Read update → NewShadow Under the Kernel: What Lean Has Actually Proved
The strongest certified results, the false routes formalization killed, and the exact analytic boundary that still separates the RH program from a proof.
Read update → NewBeyond RH: Formalizing Shadow from Gr(2,4) Up
The next phase: build the Grassmannian, atlas, bundles, group actions, measures and representation theory deeply enough to retire downstream stubs honestly.
Read strategy →GPPVerify is public. The blueprint, source, CI history and formalization plan can all be inspected directly.