`phi_sq`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.JCostGeometry
domain: Foundation
line: 202 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.JCostGeometry on GitHub at line 202.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

 199noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
 200
 201/-- phi satisfies φ² = φ + 1 -/
 202theorem phi_sq : phi ^ 2 = phi + 1 := by
 203  unfold phi
 204  have h5 : (0 : ℝ) ≤ 5 := by norm_num
 205  have hsq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
 206  nlinarith [hsq]
 207
 208/-- phi > 0 -/
 209theorem phi_pos : 0 < phi := by
 210  unfold phi
 211  have : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 5)
 212  linarith
 213
 214/-- The link-penalty cost J_bit = ln φ -/
 215noncomputable def jBit : ℝ := Real.log phi
 216
 217/-- J_bit > 0 -/
 218theorem jBit_pos : 0 < jBit := Real.log_pos (by
 219  unfold phi
 220  have : 1 < Real.sqrt 5 := by
 221    rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
 222    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 223  linarith)
 224
 225end JCostGeometry
 226end Foundation
 227end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.