def
definition
hypothesis3
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.CKMMatrix on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
103 1/2.618 = 0.382
104
105 Even larger. -/
106noncomputable def hypothesis3 : ℝ := 1 / phi^2
107
108/-- Hypothesis 4: λ = (3 - φ)/3
109
110 (3 - 1.618)/3 = 1.382/3 = 0.461
111
112 Too large. -/
113noncomputable def hypothesis4 : ℝ := (3 - phi) / 3
114
115/-- Hypothesis 5: λ = sin(π/(4φ))
116
117 sin(π/6.472) = sin(0.485) ≈ 0.466
118
119 Too large. -/
120noncomputable def hypothesis5 : ℝ := Real.sin (Real.pi / (4 * phi))
121
122/-- Hypothesis 6: λ = (φ - 1)^2 / φ
123
124 0.618² / 1.618 = 0.382 / 1.618 = 0.236
125
126 Close! Only 4% off from observed 0.227. -/
127noncomputable def hypothesis6 : ℝ := (phi - 1)^2 / phi
128
129/-- **BEST FIT**: λ ≈ (φ - 1)² / φ ≈ 0.236
130
131 Observed: 0.2265
132 Predicted: 0.236
133 Error: ~4%
134
135 This is a promising φ-connection! -/
136noncomputable def bestCabibboFit : ℝ := hypothesis6