plotEncoding
plain-language theorem explainer
The definition assigns each of Booker's seven plot families to a distinct non-zero vector in F_2^3 by mapping rags to riches to axis1, voyage and return to axis2, comedy to axis3, the quest to axis12, tragedy to axis13, overcoming the monster to axis23, and rebirth to axis123. Researchers working on the narrative geodesic would cite it to realize the explicit bijection of Theorem 9 in Seven_Plots_Three_Dimensions.tex. The definition is a direct case split on the seven constructors of BookerPlotFamily that delegates each case to the axis vectors
Claim. Let B be the set of seven Booker plot families. The map plotEncoding : B → F_2^3 sends rags to riches to (1,0,0), voyage and return to (0,1,0), comedy to (0,0,1), the quest to (1,1,0), tragedy to (1,0,1), overcoming the monster to (0,1,1), and rebirth to (1,1,1).
background
The module treats narrative as a geodesic on the cube Q_3 = (Z/2Z)^3, with Booker's seven plot families placed in explicit bijection to the seven non-zero vectors. BookerPlotFamily is the inductive type whose constructors are the seven families; each is assigned to a unique combination of the three axes (protagonist status via axis1, world status via axis2, value alignment via axis3). The axis vectors and their sums are supplied by the F2Power algebra. The local setting is the aesthetics extension of Recognition Science, where the bijection count 7 = 2^3 - 1 follows from the forced dimension D = 3.
proof idea
The definition is a pure pattern match on the seven constructors of BookerPlotFamily. Each case returns the corresponding axis vector (axis1, axis2, axis3, axis12, axis13, axis23, axis123) imported from F2Power. No lemmas or tactics are applied.
why it matters
This supplies the concrete encoding required by NarrativeGeodesicCert and the one-statement theorem narrative_geodesic_one_statement. It realizes the paper's Theorem 9 bijection and feeds the no-eighth-plot result and the XOR-additivity of plot composition. It instantiates the framework landmark that D = 3 is forced in the unified chain, here applied to the narrative state space whose non-zero elements are exhausted by the seven plots.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.