1 Overview

This blueprint tracks the formal verification of the ONON framework (On the Nature of Nature, Daniel Toupin, 2026) in Lean 4 with Mathlib 4.19.0.

Primary target: RH Pathway 2 (Spectral/Meyer).

Status of thm:link6: \(c_{2D} = \kappa _0 \cdot c_{4D}^{\mathrm{Weyl}}\) has been formalized in Link6.lean via four physics axioms (Weinberg soft theorem, Cachazo-Strominger, Capper-Duff, Adler-Bardeen). The algebra is clean; the physics derivation is documented as axioms.