GPPVerify: Lean 4 Formalization of the ONON Framework

13 Standard Model — Dark Matter Abundance

Theorem 13.1 Dark Matter Abundance from Shadow Unitarity
#

If \(c_{2D} = 0\) (shadow unitarity), then the dark matter relic density \(\Omega _{\mathrm{DM}} {\gt} 0\).

Physics: shadow symmetry breaking generates the DM mass scale; unitarity of the shadow amplitude fixes the abundance. Formalized via axioms shadow_breaking_gives_abundance and shadow_unitarity_abundance_pos.