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