`phi_sq`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.JCostGeometry on GitHub at line 202.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.