theorem
proved
phi_sq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.Inequalities on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
103 exact hdiv.symm
104
105/-- φ² = φ + 1 (the defining equation) -/
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