mass_from_phi_ladder

formal source

 122
 123/-- **THEOREM (Hierarchy from φ-ladder)**: Each generation sits on a different
 124    rung of the φ-ladder, giving exponential mass ratios. -/
 125theorem mass_from_phi_ladder :
 126    1 < phi := by linarith [Constants.phi_gt_onePointFive]
 127
 128/-! ## Why Not 2 or 4 Generations? -/
 129
 130/-- Could we have 2 generations? No - D=3 requires 3 dimensions.
 131    Could we have 4? No - 8 = 2³ gives exactly 3 bits.
 132    
 133    **Proved**: 8 = 2^3 and the number of bits in a byte is 3 (log₂ 8 = 3). -/
 134theorem why_exactly_three :
 135    -- 8-tick cycle has exactly 3 bits, corresponding to 3 dimensions
 136    (8 : ℕ) = 2^3 := by norm_num
 137
 138/-- **THEOREM (No Fourth Generation)**: Electroweak precision tests and
 139    Higgs production rule out a 4th generation with SM-like couplings.
 140    RS explains WHY: there's no "room" in the 8-tick structure for a 4th. -/
 141theorem no_fourth_generation :
 142    List.length [Generation.first, Generation.second, Generation.third] ≠ 4 := by decide
 143
 144/-! ## Mixing Between Generations -/
 145
 146/-- The CKM matrix elements encode how generations "talk" to each other.
 147    In RS, this comes from the overlap of 8-tick phases. -/
 148structure CKMElement where
 149  /-- From generation (1, 2, or 3). -/
 150  fromGen : Fin 3
 151  /-- To generation (1, 2, or 3). -/
 152  toGen : Fin 3
 153  /-- Mixing amplitude (complex). -/
 154  amplitude : ℂ
 155