GPPVerify: Lean 4 Formalization of the ONON Framework

6 thm:link6 Formalized

Theorem 6.1 Link 6: \(c_{2D} = \kappa _0 \cdot c_{4D}^{\mathrm{Weyl}}\)
#

The celestial central charge \(c_{2D}\) equals \(\kappa _0\) times the Weyl anomaly \(c_{4D}^{\mathrm{Weyl}}\).

Formalized: The identity is asserted as axiom link6_from_physics with four supporting physics axioms: Weinberg soft graviton theorem, Cachazo-Strominger celestial OPE, Capper-Duff one-loop Weyl anomaly, Adler-Bardeen non-renormalization. The algebraic corollary link6_corollary (\(c_{2D} = 0 \iff c_{4D}^{\mathrm{Weyl}} = 0\)) is proved clean.

Corollary 6.2 Three Generations from \(c = 0\)
#

\(c_{2D} = 0 \Rightarrow c_{4D}^{\mathrm{Weyl}} = 0 \Rightarrow n_{\mathrm{gen}} = 3\) (Boyle–Turok 2021).