narrative_geodesic_one_statement
plain-language theorem explainer
The theorem consolidates five structural claims: Booker's seven plot families have cardinality exactly 2^3 - 1, the explicit encoding map from families to nonzero vectors in (Z/2Z)^3 is bijective, narrative tension vanishes at exact resolution, and resolution cost lies strictly below climax cost in any three-act structure. A researcher modeling narrative as geometry on the F2-cube would cite this as the single-statement closure of the seven-plot correspondence. The proof is a direct term-mode conjunction of the five supporting lemmas already on
Claim. Let $B$ denote the set of Booker's seven plot families and let $E: B → (ℤ/2ℤ)^3$ be the explicit axis encoding. Then $|B| = 2^3 - 1$, $E$ is injective, the image of $E$ is exactly the set of nonzero vectors, the tension $T(a,t) := J(a/t)$ satisfies $T(t,t) = 0$ whenever $t ≠ 0$, and every three-act narrative satisfies resolution cost < climax cost.
background
BookerPlotFamily is the inductive type whose seven constructors are the standard plot families (Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, Rebirth). The module works on the cube Q₃ = F2Power 3, the three-dimensional vector space over GF(2). plotEncoding assigns each family to a unique nonzero vector according to the three axes (protagonist status, world status, value alignment). narrativeTension is defined as Jcost(actual/target) and therefore vanishes when actual equals target. ThreeActNarrative is the structure with setup cost s > 0, climax cost c > s, and resolution cost exactly 0. The upstream result booker_seven_eq_2_pow_3_minus_1 states that the cardinality equals 2^3 - 1 because the count is taken from the dimension D = 3 rather than asserted directly.
proof idea
The proof is a one-line term-mode wrapper. It applies refine to the five component results: booker_seven_eq_2_pow_3_minus_1 for the cardinality, plotEncoding_injective for injectivity, no_eighth_plot for surjectivity onto the nonzero vectors, narrativeTension_resolution for the vanishing of tension at resolution, and three_act_resolution_below_climax for the strict cost inequality.
why it matters
This declaration supplies the consolidated one-statement form of the narrative-geodesic claims in Seven_Plots_Three_Dimensions.tex. It closes the structural loop on the F2-cube by proving that exactly seven plots exist and that tension resolves cleanly, consistent with the D = 3 forced by the upstream chain. Because the cardinality is derived from F2Power.nonzero_card rather than hardcoded, the result inherits the geometric origin of the seven-plot count. No downstream uses are recorded yet, leaving open whether the statement will be invoked inside larger aesthetic or recognition-cost arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.