plotEncoding_image_nonzero
plain-language theorem explainer
The axis-encoding map from Booker's seven plot families to vectors in (Z/2Z)^3 sends each family to a nonzero vector. Workers on the structural bijection between narrative archetypes and the cube Q3 cite this lemma when assembling the master certificate. The proof reduces to exhaustive case analysis on the inductive definition of the plot families followed by a decision procedure on each case.
Claim. For every plot family $p$ among Booker's seven families, the axis-encoding map satisfies $π(p) ≠ 0$ in $(ℤ/2ℤ)^3$.
background
The module sets up an explicit bijection between Booker's seven plot families and the seven nonzero elements of F2Power 3, the elementary abelian 2-group of rank 3 modeled as Fin 3 → Bool with pointwise XOR. The plotEncoding function supplies the axis assignment (protagonist status, world status, value alignment) that realizes the table from Theorem 9 of Seven_Plots_Three_Dimensions.tex. BookerPlotFamily is the inductive type whose seven constructors are the plots Overcoming the Monster, Rags to Riches, The Quest, Voyage and Return, Comedy, Tragedy, and Rebirth.
proof idea
The term proof performs case analysis on the inductive type BookerPlotFamily. For each of the seven constructors the decide tactic confirms that the image under plotEncoding differs from the zero vector in F2Power 3.
why it matters
The lemma supplies the nonzero property required by the CountLaw 3 instance in bookerCountLaw and by the master certificate narrativeGeodesicCert. It completes one direction of the explicit bijection stated in Theorem 9 of the aesthetics paper, confirming that no plot family maps to the zero vector in the cube Q3. The result sits inside the aesthetics module that deepens the structural closure for the seven-plot correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.