def
definition
hypothesis1
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 92.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
89 1/(2 × 1.618) = 1/3.236 = 0.309
90
91 Too large compared to observed 0.227. -/
92noncomputable def hypothesis1 : ℝ := 1 / (2 * phi)
93
94/-- Hypothesis 2: λ = (φ - 1)/2
95
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 / φ