def
definition
hypothesis2
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 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
96 (1.618 - 1)/2 = 0.618/2 = 0.309
97
98 Same as above, too large. -/
99noncomputable def hypothesis2 : ℝ := (phi - 1) / 2
100
101/-- Hypothesis 3: λ = 1/φ²
102
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