pith. machine review for the scientific record. sign in
theorem proved term proof

Jcost_pos_of_ne_one

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 231theorem Jcost_pos_of_ne_one (r : ℝ) (hr : 0 < r) (hr_ne : r ≠ 1) :
 232    0 < Jcost r := by

proof body

Term-mode proof.

 233  have h := Jcost_eq_sq (ne_of_gt hr)
 234  rw [h]
 235  apply div_pos
 236  · have : r - 1 ≠ 0 := sub_ne_zero.mpr hr_ne
 237    positivity
 238  · positivity
 239
 240/-! ## §5  Working Memory Capacity -/
 241
 242/-- Working memory capacity prediction: φ³ ≈ 4.236.
 243    The cache hierarchy at ratio φ gives Level 1 (working memory)
 244    capacity = φ³ relative to Level 0 (focal attention, capacity 1). -/

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.