plotEncoding_image_nonzero
plain-language theorem explainer
The explicit axis encoding of Booker's seven plot families into the rank-3 elementary abelian 2-group maps every family to a nonzero vector. Workers establishing the bijection between narrative archetypes and the geometry of (Z/2)^3 cite this when verifying that the assignment avoids the zero element. The argument is settled by exhaustive case analysis on the seven constructors followed by a decision procedure.
Claim. Let $B$ be the inductive type whose seven constructors are the plot families. Let $e: B → (ℤ/2ℤ)^3$ be the axis assignment that sends each family to a coordinate triple according to protagonist status, world status, and value alignment. Then $e(p) ≠ 0$ for every $p ∈ B$.
background
The module develops the structural correspondence between Booker's seven plot families and the nonzero elements of F2Power 3, modeled as Fin 3 → Bool with pointwise XOR. The encoding realizes the explicit bijection of the companion paper by mapping each family to a distinct nonzero vector via three axes. This result supplies one of the four properties required for the master certificate that inhabits the NarrativeGeodesicCert structure.
proof idea
The term proof performs case analysis on the inductive type BookerPlotFamily and then invokes decide to confirm that each of the seven images under the encoding differs from the zero vector in F2Power 3.
why it matters
The lemma supplies the nonzero property required by narrativeGeodesicCert and by the CountLaw instance bookerCountLaw. It closes one direction of the bijection between the seven plot families and the seven nonzero vectors of (Z/2)^3, which is the geometric content of the rank-3 case of the eight-tick octave. The companion result plotEncoding_image_eq_nonzero then upgrades the image statement to equality with the full nonzero set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.