The central result establishes that the alternating group A₅ is the unique finite subgroup of SO(3) satisfying three physical principles: non-solvability, simplicity, and perfectness. From this uniqueness, the formalization derives icosahedral invariants (β₀ = V − 1 = E/n + χ/2 = 11), prohibition structures on tensor-product dimensions ({9, 15, 16, 25}), and the solvability of all finite groups of order below 60. This repository provides a complete formal verification in Lean 4 + Mathlib of the mathematical core of the paper. Prohibition structure (formally verified) Index Mechanism Algebraic reason 9 (P1) ρ₄-free: only solvable components from SO(3) 15 (P1)+(P2) ρ₄ absent; Sym²ρ₅ has multiplicity > 1 16 (P1) ρ₄ ⊗ ρ₄ (self-product): includes all 5 irreducibles 25 (P1) ρ₄ absent and self-product ICO correspondence to physical constants (46 quantities) The paper maps icosahedral parameters (F=20, E=30, V=12, n=3, χ=2, |A₅|=60, φ=(1+√5)/2, gap=1/φ³) to 46 physical quantities across 9 categories. Type I = RG-invariant integers; Type II = fixed-point universals; Type III = cosmological freeze-out. Gauge couplings & scales (#1–#10) # Quantity ICO formula ICO value Exp. Dev. Type 1 α⁻¹ Fφ⁴ 137.08 137.036 0.034% I/III 2 α_s(M_Z) gap/2 0.1180 0.1180(9) 0.03% I/III 3 sin²θ_W gap(1−1/(Fπ)) 0.2312 0.2312 0.4% II 4 α/α_G φ²⁰⁴ ~10⁴⁴ ~10⁴⁴ ~2% II 5 α_s/α 10φ 16.18 16.16 <0.1% II 6 β₀(n_f=0) E/n + χ/2 11 11 exact I 7 Quark coeff. |A₅|/(En) 2/3 2/3 exact I 8 Λ_QCD M_Z/φ¹² 283 MeV 292 MeV 3.1% III 9 M_Pl/m_e √F · φ¹⁰⁴ ~2.4×10²² ~2.4×10²² ~1.6% III 10 M_GUT/M_Z φ⁶⁸ ~10¹⁴ ~10¹⁴ order III Charged lepton masses (#11–#14) # Quantity ICO formula ICO Exp. Dev. Type 11 m_e M_Z α²(1−α)/(nπ) 0.511 MeV 0.511 MeV 0.2% II 12 m_μ/m_e φ¹¹ 199.0 206.8 3.7% II 13 m_τ/m_e φ¹⁷ 3571 3477 2.7% II 14 Koide Q 1 − 1/n = 2/3 0.6667 0.6666 0.01% II Quark masses (#15–#20) # Quantity ICO formula ICO Exp. Dev. Type 15 m_t M_Z φ²/√2 ... 172.8 GeV 172.6 GeV 0.14% II 16 m_t/m_b F+V+E/n = 42 42 41.5 1–2% II 17 m_t/m_c φ¹⁰ 123.0 134(±) scheme II 18 m_c/m_s V + φ 13.62 13.6(±) ~0.2% II 19 m_s/m_d F = 20 20 20(±) ~0.2% II 20 m_d/m_u √5 2.236 2.16(±) ~3.5% II Neutrino masses (#21–#23, exploratory) # Quantity ICO formula ICO Exp. Dev. Type 21 m_ν₃ (m_e²/M_Z)φ⁻⁸ ~0.06 eV ~0.05 eV ~22% III 22 m_ν₂/m_ν₃ φ⁻⁶ 0.056 ~0.17 ×3 III 23 m_ν₁/m_ν₂ φ⁻¹¹ 0.005 upper lim. — III Mixing angles (#24–#26) # Quantity ICO formula ICO Exp. Dev. Type 24 sin θ_C gap 0.2361 0.2253 4.8% II 25 sin²θ₁₃(ν) 2/(5φ⁶) 0.0223 0.0218 2.3% II 26 |V_ub| suppression gap³ 0.013 0.004 ×3 (T) II #26: φ-exponent = 9 ∈ prohibited set {9,15,16,25}. Marked as negative control (T). The large deviation is consistent with the prohibition rule. Electroweak boson masses (#27–#30) # Quantity ICO formula ICO Exp. Dev. Type 27 M_Z Reference scale 91.19 GeV 91.19 GeV — — 28 M_W/M_Z √(2/φ) 0.874 0.882 0.9% II 29 v (VEV) M_Z φ² 238.7 GeV 246.2 GeV 3% II Higgs sector (#31–#33) # Quantity ICO formula ICO Exp. Dev. Type 31 m_H/M_Z φ − gap 1.382 1.374 0.6% II 32 m_H/M_W ≈ φ 1.581 1.559 ~0.2% II 33 λ_H (φ−gap)²/(2φ⁴) 0.140 — — II Hadron masses (#34–#35) # Quantity ICO formula ICO Exp. Dev. Type 34 m_p (n + 1/n)Λ_QCD 943 MeV 938 MeV 0.6% II 35 m_p/m_e 6π⁵ × C_pe 1836.2 1836.2 0.002% II Gravity & Planck scale (#36–#38) # Quantity ICO formula ICO Exp. Dev. Type 36 G ℏc/(Fφ²⁰⁸m_e²) ~6.5×10⁻¹¹ 6.674×10⁻¹¹ 3.2% III 37 M_Pl √F · φ¹⁰⁴ · m_e ~1.22×10¹⁹ GeV 1.22×10¹⁹ GeV ~1.6% III Cosmological parameters (#39–#43) # Quantity ICO formula ICO Exp. Dev. Type 39 Λℓ_Pl² φ⁻⁶⁰⁰ ~10⁻¹²² ~10⁻¹²² order III 40 H₀ t_Pl φ⁻²⁹¹ ~10⁻⁶¹ ~10⁻⁶¹ 1.1% III 41 T_CMB/T_Z φ⁻⁷⁰ ~3×10⁻¹¹ ~3×10⁻¹¹ 5.7% III 42 D_cosmic n − 1/n = 8/3 2.667 2.7(±) ~1% III Dark components & baryon asymmetry (#44–#46, speculative) # Quantity ICO formula ICO Exp. Dev. Type 44 Ω_DM/Ω_b |A₅|/V = 5 5.0 5.3(1) ~6% III 45 Ω_Λ φ²/(φ²+1) 0.724 0.685 5.7% III 46 η_B 6φ⁻⁴⁸ ~6×10⁻¹⁰ ~6×10⁻¹⁰ order III Role breakdown (#1–#46) Role Meaning Count Items I Input 1 #27 S Selection 2 #1, #2 P Prediction 18 #3,4,6,7,8,12,13,15,16,17,20,28,29,31,39,40,41,42 D Derived 14 #5,9,10,11,14,18,19,30,32,33,34,35,37,43 X Exploratory 10 #21,22,23,24,25,36,38,44,45,46 T Tension (negative control) 1 #26 (φ-exp = 9 ∈ prohibited) Icosahedral parameters Symbol Value Description F 20 Faces E 30 Edges V 12 Vertices n 3 Face valence (triangular) χ 2 Euler characteristic |A₅| 60 Order of the alternating group φ (1+√5)/2 ≈ 1.618 Golden ratio gap 1/φ³ ≈ 0.2361 Galois deviation rate File structure File Content Auxiliary.lean Foundation lemmas (A₅ properties) SolvabilityBelow60.lean |G| < 60 → IsSolvable G Section1–8_*.lean Paper sections §1–§8 ConjugacyClassGalois.lean Conjugacy class analysis Reproducibility git clone https://github.com/nuu/A5CosmicNecessity && cd A5CosmicNecessity && lake build

If you use this software, please cite it as below.