def
definition
phi
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Derivations.MassToLight on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
54/-! ## Golden Ratio Powers -/
55
56/-- The golden ratio φ. -/
57noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
58
59/-- Powers of φ give the candidate M/L values. -/
60noncomputable def phi_power (n : ℤ) : ℝ := phi ^ n
61
62/-! ## Geometric Bounds Helper -/
63
64lemma phi_gt_one : phi > 1 := by
65 unfold phi
66 have : Real.sqrt 5 > 1 := by
67 rw [← Real.sqrt_one]
68 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
69 linarith
70
71lemma phi_lt_two : phi < 2 := by
72 unfold phi
73 have : Real.sqrt 5 < 3 := by
74 rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤3)]
75 apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
76 linarith
77
78/-! ## Specific Powers -/
79
80/-- Lower bound for φ. -/
81lemma phi_gt_1_6 : phi > 1.6 := by
82 unfold phi
83 norm_num
84 have : Real.sqrt 5 > 2.2 := by
85 rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.2)]
86 apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
87 linarith