`phi_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.JCostGeometry
domain: Foundation
line: 209 · 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 209.

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

depends on

formal source

 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.