narrativeTension
plain-language theorem explainer
Narrative tension is the J-cost of the ratio actual divided by target intensity when the target is nonzero. Researchers formalizing narrative geodesics on the F2Power 3 cube cite it to quantify deviation costs in the aesthetics component of Recognition Science. The definition is a direct one-line substitution of the normalized ratio into the imported J-cost function.
Claim. Narrative tension between actual intensity $a$ and nonzero target intensity $t$ is defined as $J_ {cost}(a/t)$, where $J_{cost}$ is the recognition cost function with $J_{cost}(1)=0$.
background
The NarrativeGeodesic module formalizes Booker's seven plot families as the nonzero elements of F2Power 3, the cube in three dimensions, with an explicit injective encoding whose image exhausts those elements. J-cost is the recognition cost imported from the Cost module and implements the J-uniqueness map J(x)=(x + x^{-1})/2 - 1 for positive ratios. Upstream results supply the is predicates from OptionAEmpiricalProgram and SimplicialLedger that guarantee collision-free empirical programs and algebraic edge lengths in the ledger.
proof idea
One-line definition that applies Jcost directly to the ratio actual/target under the nonzero-target hypothesis. No tactics beyond the assignment are required.
why it matters
The definition supplies the tension primitive used inside NarrativeGeodesicCert and the narrative_geodesic_one_statement theorem, which together prove the bijection of Booker plots with the seven nonzero vectors of F2Power 3 and zero tension at exact resolution. It completes the aesthetics row by providing a cost measure consistent with T5 J-uniqueness and the D=3 spatial structure of the narrative state space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.