three_act_resolution_below_climax
plain-language theorem explainer
In the three-act narrative model, resolution J-cost is strictly below climax J-cost for any state satisfying the positivity and ordering axioms. Researchers formalizing story structure via Recognition Science cost functions cite this to confirm tension release at the end of the arc. The proof is a one-line wrapper that rewrites resolution cost to zero then applies linear arithmetic to the setup positivity and climax ordering fields.
Claim. Let $n$ be a three-act narrative with setup cost $s>0$, climax cost $c>s$, and resolution cost $r=0$. Then $r<c$.
background
The module develops the narrative side of aesthetics by mapping Booker's seven plot families to the seven nonzero vectors of the elementary abelian 2-group $F_2^3$, which models the three-dimensional narrative state space. The structure ThreeActNarrative encodes a three-act story whose fields are setup cost $s$, climax cost $c$, resolution cost $r$, together with the axioms $s>0$, $c>s$, and $r=0$, where the costs are instances of the J-cost function induced by the Recognition Composition Law. This local setting sits inside the broader Recognition framework whose forcing chain produces the J-function $J(x)=(x+x^{-1})/2-1$ and the eight-tick octave.
proof idea
The proof rewrites the resolution_cost field to zero using the resolution_zero hypothesis of the ThreeActNarrative structure, then invokes the linarith tactic on the setup_pos and climax_higher inequalities to obtain the strict comparison.
why it matters
The result is invoked by narrativeGeodesicCert and narrative_geodesic_one_statement, which together certify the explicit bijection between BookerPlotFamily and the nonzero elements of F2Power 3 together with the vanishing of narrative tension at resolution. It supplies the final structural closure for the narrative geodesic construction, confirming that J-cost vanishes exactly when the target intensity is reached, consistent with the master certificate that derives the count 7 from $2^3-1$ and the dimension $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.