def
definition
massHierarchyPattern
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.ThreeGenerations on GitHub at line 120.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
117 - muon/electron ≈ 207 ≈ φ^11
118
119 The pattern is φ^n for various n. -/
120def massHierarchyPattern : String :=
121 "Masses scale as φ^n for generation-dependent n"
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