def
definition
phi_power
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Derivations.MassToLight on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
88
89/-- Upper bound for φ. -/
90lemma phi_lt_1_7 : phi < 1.7 := by