GPPVerify: Lean 4 Formalization of the Shadow 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 not asserted. It is carried as the explicit hypothesis Link6Hypothesis, so every consumer displays its dependence on Link 6 in its own statement rather than inheriting a global axiom. The five axioms this entry previously named (link6_from_physics plus Weinberg soft-graviton, Cachazo–Strominger celestial OPE, Capper–Duff one-loop Weyl anomaly, Adler–Bardeen non-renormalization) were retired on 2026-08-30; the four physics inputs survive as documented open_ placeholders. The algebraic corollary link6_corollary (\(c_{2D} = 0 \iff c_{4D}^{\mathrm{Weyl}} = 0\), given \(\kappa _0 {\gt} 0\)) is proved clean and is unconditional on Link 6 itself.

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