`jBit_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.JCostGeometry on GitHub at line 218.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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.