Localizing Physical Arbitrariness in the A₅ to Standard Model Pathway

Overview The gauge group SU (3) C × SU (2) L × U (1) Y of the Standard Model with three fermion generations is dissected along the algebraic pathway A5 → 2I → Ê8 → E6 × A2 → SU (3) 3 → SM under a strict three-layer epistemological separation: machine-verified mathematics (M), physical bridging hypotheses (P), and observational facts (E). Structure of the pathway A5 → 2I (double cover): The alternating group A5 (order 60), the unique non-solvable finite subgroup of SO (3), has a unique double cover 2I (binary icosahedral group, order 120) via the Schur multiplier H2 (A5, U (1) ) = Z2. 2I → Ê8 (McKay correspondence): The McKay graph of 2I ⊂ SU (2) — with 9 irreps as vertices and tensor product decomposition as edges — coincides with the affine Dynkin diagram Ê8. The 9 nodes carry marks summing to the Coxeter number h = 30 and split into A5-type (0, 2, 3, 5, 7, Σd² = 60) and spinorial (1, 4, 6, 8, Σd² = 60) by parity. Ê8 → E6 × A2 (M58–M61): Among the 8 maximal subalgebras of E8 (Dynkin classification), E6 × A2 is uniquely selected by three conditions: product structure (C1), complex-type representation in the 248 branching (C2), and family dimension = 3 (C3). The same conclusion is independently reached by complete enumeration of single-node removal from Ê8: only removal of node 7 (mark 3, ρ′3) yields an E6 factor (M60), establishing the mark-3 dichotomy (M61). McKay–family dictionary (M49): The Galois pair ρ3, ρ′3 = node 2, node 7 splits asymmetrically: ρ′3 (node 7) is removed to become the family index (the "3" in (27, 3) ), while ρ3 (node 2) remains inside E6. This identification is unique and convention-independent. CP structure (M50–M57): All A5 irreps are real type (ν2 = +1), making CP violation impossible within A5 alone (M50). The first complex receptacle appears at E6, where the fundamental 27 ≇ 27̄ (M51). The unique CP source is arg (λ3) of the cubic invariant dijk (M52). The Galois involution σ: √5 → −√5 swaps nodes 2 ↔ 7 on the McKay graph, realizing (27, 3) ↔ (27̄, 3̄) as the generalized CP transformation (M53–M56), and induces a CP-sensitive channel splitting between mass eigenvalues (Q (√5) ) and mixing angles (Q) (M57). E6 → SU (3) 3 (M62–M63): Among the 6 maximal subalgebras of E6, SU (3) 3 is uniquely selected by two independent conditions: all simple factors isomorphic (T2, M62) and equal-dimensional 27 branching 27 = 9+9+9 (T3, M63). The three factors are permuted by a Z3 cyclic symmetry. Combined total rank: 3×2 + 2 = 8 = rank (E8). SU (3) 3 → SM: Identifying one of the three Z3-equivalent SU (3) factors as color requires the physical inputs E2 (non-abelian strong force), E3 (asymptotic freedom), and P-4b (color identification). Main results Rigidity: The core pathway A5 → 2I → Ê8 → E6 × A2 is uniquely fixed in the M layer with only n = 3 and Ngen = 3 as external inputs. Localization: The minimal hypothesis set Σmin = E1a, E1b, E2, E3, P-4a′, P-4b is complete and irreducible. The structural P-layer degrees of freedom are localized to exactly two points: the equal-rank democracy principle (P-4a′) and color identification (P-4b). Contents Lean 4 + Mathlib formal verification code (sorry = 0, axiom = 0; ~45 files, ~10, 800 lines, 60+ named theorems M01–M63) GAP 4. 15. 1 and Python cross-verification scripts Supplementary Material: Theorem–Lean 4 Identifier Correspondence Table (PDF) License Apache License 2. 0