theorem
proved
mixingAngles_geometric_origin
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogSpec.RSBridge on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
151
152The [1/φ] is a first-order approximation; full derivation uses geometric structure.
153-/
154theorem mixingAngles_geometric_origin :
155 (1 : ℕ) / edgeDualCount = 1 / 24 ∧
156 cabibboProjection = -3 := by
157 constructor <;> rfl
158
159/-!
160### Numeric Approximations
161
1621. **V_cb ≈ 0.0417**: (1/24) matches the V_cb observation.
1632. **φ⁻³ ≈ 0.236**: Golden projection part of the Cabibbo angle.
164-/
165
166theorem V_cb_approx : (1 : ℚ) / 24 > 0.04 ∧ (1 : ℚ) / 24 < 0.05 := by
167 constructor <;> norm_num
168
169end RecogSpec
170end IndisputableMonolith