theorem proved tactic proof

`jBit_pos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 218theorem jBit_pos : 0 < jBit := Real.log_pos (by

proof body

Tactic-mode proof.

 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

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

finite_capacity_veto in IndisputableMonolith.Foundation.TopologicalVeto decl_use
link_penalty_positive in IndisputableMonolith.Foundation.TopologicalVeto decl_use

depends on (2)

Lean names referenced from this declaration's body.

jBit in IndisputableMonolith.Foundation.JCostGeometry decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use