plotEncoding_image_eq_nonzero
plain-language theorem explainer
The encoding from Booker's seven plot families to vectors in the three-dimensional space over GF(2) is surjective onto the nonzero vectors. Researchers examining the geometric model of narrative archetypes would cite this equality to close the bijection. The proof establishes set equality by verifying that the image lies inside the nonzero filter and that the two sides have identical cardinality seven.
Claim. Let $f$ map each of the seven plot families to its assigned vector in the vector space $V = (Z/2Z)^3$. Then the image of $f$ equals the set of all nonzero vectors in $V$.
background
The module constructs the narrative geodesic on the cube $Q_3 = (Z/2Z)^3$, placing Booker's seven plot families in explicit bijection with the seven nonzero vectors of this space via an axis assignment (protagonist status, world status, value alignment). The function $f$ realizes the table from the associated paper, sending each family to a distinct nonzero vector. Upstream results supply the definition of the elementary abelian 2-group of rank 3 as maps from a 3-element index set to Bool, the injectivity of $f$, the fact that every encoded vector is nonzero, and the cardinality theorem that the plot families number exactly seven.
proof idea
Apply the finite-set equality lemma that requires one-sided inclusion plus a cardinality bound. The inclusion direction uses the nonzero property of each encoded vector. The cardinality direction rewrites the image cardinality via the injectivity lemma to the plot-family cardinality, then matches it against the nonzero cardinality of the 2-group.
why it matters
This equality supplies the surjectivity half of the bijection and is invoked directly by the no-eighth-plot theorem, which functions as Falsifier 1: every nonzero vector in the 3-space encodes some plot and no eighth plot exists on three axes. It replaces an earlier asserted count with the algebraic identity $2^3-1=7$ derived from the F2Power construction. The result sits inside the aesthetics module that realizes the structural closure for the narrative side of the Recognition framework, consistent with the forcing of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.