NarrativeGeodesicCert
plain-language theorem explainer
The NarrativeGeodesicCert structure certifies that Booker's seven plot families stand in explicit bijection with the seven nonzero vectors of the three-dimensional vector space over GF(2). An aesthetics researcher extending Recognition Science would cite this certificate to close the seven-plot model under the D=3 constraint. The certificate is assembled by direct references to the cardinality theorems, encoding injectivity, and tension-vanishing property already established in the module.
Claim. Let $B$ be the set of Booker's seven plot families and let $V = (Z/2Z)^3$. There exists a structure certifying that $|B| = 7 = 2^3 - 1$, that the encoding map $e: B → V$ is injective with image exactly the nonzero vectors of $V$, that narrative tension vanishes when actual intensity equals target intensity, and that resolution cost lies strictly below climax cost in any three-act narrative.
background
In the module on narrative geodesics over the cube $Q_3 = (Z/2Z)^3$, Booker's plot families form an inductive type whose seven constructors correspond to the standard seven-plot taxonomy. The plotEncoding function maps each family to a unique nonzero vector in F2Power 3, which is defined as Fin 3 → Bool with pointwise XOR and models the three axes of protagonist status, world status, and value alignment. Narrative tension is the J-cost of the ratio of actual to target intensity, while a three-act narrative records setup, climax, and resolution costs with resolution fixed at zero.
proof idea
As a structure definition the certificate is assembled by referencing the pre-proved facts: cardinality of BookerPlotFamily equals 7 and equals 2^3 - 1, injectivity and nonzero image of plotEncoding, equality of the image to all nonzero vectors in F2Power 3, vanishing of narrativeTension at equal arguments, and the strict inequality of resolution cost below climax cost in ThreeActNarrative.
why it matters
This certificate supplies the inhabited master object that narrativeGeodesicCert constructs and that downstream aesthetics results depend upon. It closes the bijection between Booker's plots and the nonzero elements of the D=3 state space, directly implementing the T8 dimension constraint and the reduction to 2^3 - 1 nonzero states. The construction confirms the weight decomposition 1+3+3+1 matches the primary/compound/transcendent grouping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.