theorem
proved
phi_plus_inv
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.Inequalities on GitHub at line 109.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
106theorem phi_sq : φ^2 = φ + 1 := Constants.phi_sq_eq
107
108/-- φ + 1/φ = √5 -/
109theorem phi_plus_inv : φ + 1/φ = Real.sqrt 5 := by
110 unfold φ Constants.phi
111 have hroot_pos : (0 : ℝ) < 5 := by norm_num
112 have hroot_ne : Real.sqrt 5 + 1 ≠ 0 := by
113 have := Real.sqrt_nonneg 5
114 linarith
115 field_simp
116 ring_nf
117 rw [Real.sq_sqrt (le_of_lt hroot_pos)]
118 ring
119
120/-- J-cost of φ -/
121theorem J_cost_phi : (φ + 1/φ) / 2 - 1 = (Real.sqrt 5 - 2) / 2 := by
122 rw [phi_plus_inv]
123 ring
124
125end Inequalities
126end Foundation
127end IndisputableMonolith