pith. machine review for the scientific record. sign in
def

phi

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.JCostGeometry
domain
Foundation
line
199 · github
papers citing
1 paper (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.JCostGeometry on GitHub at line 199.

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

 196  ring
 197
 198/-- **F1.5.2**: The golden ratio -/
 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 (showing 1 of 1)