plotEncoding
plain-language theorem explainer
The explicit mapping from Booker's seven plot families to the non-zero vectors of F_2^3, sending each family to a distinct axis combination according to the table in Theorem 9 of the source paper. Researchers establishing the bijection between narrative structures and the cube Q_3 would cite this definition when invoking the master certificate or the one-statement theorem. It is realized as a direct pattern match on the seven constructors of the inductive type BookerPlotFamily.
Claim. Let B be the inductive type whose constructors are the seven Booker plot families. Define the function phi : B to F_2^3 by phi(rags to riches) = (1,0,0), phi(voyage and return) = (0,1,0), phi(comedy) = (0,0,1), phi(the quest) = (1,1,0), phi(tragedy) = (1,0,1), phi(overcoming the monster) = (0,1,1), and phi(rebirth) = (1,1,1), where the right-hand sides are the indicated vectors in F_2^3.
background
The module NarrativeGeodesic develops the narrative geodesic on the cube Q_3 = (Z/2Z)^3 as the Lean counterpart of the paper Seven_Plots_Three_Dimensions.tex. It supplies the inductive type BookerPlotFamily whose seven constructors stand in explicit bijection with the seven non-zero elements of F2Power 3. The three axes are protagonist status, world status, and value alignment; the axis vectors themselves are supplied by the upstream definitions axis1, axis2, axis3, axis12, axis13, axis23, and axis123 in Algebra.F2Power.
proof idea
The declaration is a definition by pattern matching on the seven constructors of BookerPlotFamily, each clause returning the corresponding axis vector from F2Power.
why it matters
This definition supplies the concrete encoding required by the downstream master certificate NarrativeGeodesicCert and the one-statement theorem narrative_geodesic_one_statement. It realizes the explicit bijection of Theorem 9 in the paper and thereby connects the seven-plot count to the framework landmark D = 3. The same encoding is used to prove that plot composition is XOR-additive and that no eighth plot exists on three axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.