plotEncoding_image_nonzero
plain-language theorem explainer
The theorem asserts that the axis encoding of any Booker plot family yields a nonzero vector in the three-dimensional vector space over F2. Researchers establishing the bijection between narrative archetypes and the cube Q3 cite this result when assembling the master certificate. The proof is a term-mode case analysis on the seven constructors of BookerPlotFamily followed by decidable checks.
Claim. For every plot family $p$ among Booker's seven families, the encoding map satisfies $plotEncoding(p) ≠ 0$ in $F_2^3$.
background
The module NarrativeGeodesic sets up an explicit bijection between Booker's seven plot families and the seven nonzero elements of the elementary abelian 2-group of rank 3. BookerPlotFamily is the inductive type whose seven constructors are overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy and rebirth. The function plotEncoding sends each constructor to a distinct nonzero element of F2Power 3, which is defined as Fin 3 → Bool equipped with pointwise XOR. This encoding follows the assignment table of Theorem 9 in Seven_Plots_Three_Dimensions.tex and relies on the F2Power construction from Algebra.F2Power.
proof idea
The term proof applies cases to the inductive type BookerPlotFamily, producing seven subgoals, then invokes decide on each to confirm that the corresponding encoded vector differs from the zero function.
why it matters
The result is invoked inside narrativeGeodesicCert to populate the master certificate and inside bookerCountLaw to witness the nonzero clause of the CountLaw 3 instance for BookerPlotFamily. It supplies the nonzeroness half of the bijection between the seven plots and the nonzero vectors of F2Power 3, thereby closing one structural requirement of the aesthetics module. The construction aligns with the framework's use of F2Power for D = 3 and the counting 2^3 - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.