plotEncoding_injective
plain-language theorem explainer
The assignment of Booker's seven plot families to vectors in the three-dimensional space over GF(2) is one-to-one. Researchers formalizing narrative structures within Recognition Science cite this to secure the bijection with the non-zero elements of the cube Q3. The proof is a compact term-mode case analysis that exhausts all constructor pairs and resolves equalities or contradictions by reflexivity and the decide tactic.
Claim. The map sending each Booker plot family to its assigned non-zero vector in $F_2^3$ is injective: distinct plots receive distinct vectors.
background
The module sets up the structural correspondence between Booker's seven plot families and the geometry of the cube $Q_3 = F_2^3$. BookerPlotFamily is the inductive type whose seven constructors are ragsToRiches, voyageAndReturn, comedy, theQuest, tragedy, overcomingTheMonster and rebirth. The function plotEncoding supplies the explicit axis assignment (protagonist status, world status, value alignment) that realizes the table in Theorem 9 of Seven_Plots_Three_Dimensions.tex, sending each constructor to a unique non-zero vector such as axis1 for ragsToRiches. Upstream the definition plotEncoding provides the case-by-case mapping; the module imports F2Power and Cost to ground the vectors in the Recognition algebra.
proof idea
The proof introduces plots p and q together with the hypothesis that their encodings coincide. It applies cases on both p and q, then uses a first tactic that either returns reflexivity when the constructors match or derives a contradiction by reverting the equality and invoking decide on the mismatched encodings.
why it matters
Injectivity is required to inhabit the master certificate narrativeGeodesicCert and to prove the one-statement theorem narrative_geodesic_one_statement that asserts exactly seven plots with no eighth. It also supplies the injective field of the CountLaw instance bookerCountLaw in Patterns.TwoToTheDMinusOne. Within the framework the result closes the aesthetics module by confirming the bijection between narrative families and the seven non-zero elements of F2Power 3, thereby linking story structure to the D=3 cube and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.