narrativeTension_nonneg
plain-language theorem explainer
Narrative tension, defined as the J-cost of the ratio of actual to target intensity, is non-negative whenever that ratio is positive. Researchers modeling narrative structures via Recognition Science geodesics cite this to keep costs bounded below in the Q3 cube. The proof is a direct one-line reduction to the J-cost non-negativity lemma after unfolding the definition.
Claim. Let $J$ denote the J-cost function. For real numbers $a,t$ with $t≠0$ and $0<a/t$, the narrative tension satisfies $0≤J(a/t)$.
background
The module develops narrative geodesics on the cube $Q_3=(Z/2Z)^3$ by placing Booker's seven plot families in explicit bijection with its seven nonzero vectors via the plotEncoding map, which is proved injective with image exactly the nonzero elements. Narrative tension is introduced as the recognition cost of deviation: narrativeTension actual target h := Jcost (actual/target), where the target is required nonzero. The upstream Jcost_nonneg lemma states that J(x)≥0 for all x>0, proved via the squared representation J(x)=(x-1)^2/(2x) and positivity of the numerator and denominator.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of narrativeTension to expose Jcost (actual/target), then applies the lemma Jcost_nonneg directly to the hypothesis that the ratio is positive.
why it matters
The result supplies the non-negativity axiom for tension in the aesthetics module, ensuring the three-act J-geodesic construction (Act 1 cost s, Act 2 climax c>s, Act 3 resolution 0) remains a valid cost function. It inherits the AM-GM foundation of J-cost and supports the structural closure claimed for the Seven Plots paper by keeping all narrative deviations on the positive ray non-negative. No downstream uses appear yet, but the lemma is required for any geodesic length or minimization argument in this setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.