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

narrativeTension_nonneg

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)

 295theorem narrativeTension_nonneg (actual target : ℝ) (h : target ≠ 0)
 296    (h2 : 0 < actual / target) :
 297    0 ≤ narrativeTension actual target h := by

proof body

Term-mode proof.

 298  unfold narrativeTension
 299  exact Jcost_nonneg h2
 300
 301/-! ## §7. Three-act structure as J-geodesic -/
 302
 303/-- Three-act narrative state. Act 1 has J-cost `s`, Act 2 (climax)
 304    has J-cost `c > s`, Act 3 (resolution) has J-cost `0`. -/

depends on (11)

Lean names referenced from this declaration's body.