plotEncoding_image_eq_nonzero
plain-language theorem explainer
The theorem shows that the image of the axis encoding map from BookerPlotFamily coincides exactly with the seven nonzero vectors in F2Power 3. Researchers formalizing the bijection between narrative archetypes and the cube Q3 would cite it to ground the count. The proof combines subset inclusion from the nonzero property with cardinality matching via injectivity and the established count of seven.
Claim. Let $B$ be the set of seven Booker plot families and let $E: B → F_2^3$ be the axis encoding map. Then the image $E(B)$ equals the set of all nonzero vectors in $F_2^3$.
background
The module formalizes a bijection between Booker's seven plot families and the nonzero elements of $Q_3 = F_2^3$, where $F_2^3$ is the elementary abelian 2-group of rank 3 modeled as Fin 3 → Bool with pointwise XOR. The encoding map assigns each family to a distinct nonzero vector per the table in Seven_Plots_Three_Dimensions.tex (Theorem 9). Upstream results include plotEncoding_image_nonzero (every encoded vector is nonzero), plotEncoding_injective (distinct families map to distinct vectors), card_eq_seven (Fintype.card BookerPlotFamily = 7), and F2Power.nonzero_card_three (the nonzero count is 7).
proof idea
The tactic proof applies Finset.eq_of_subset_of_card_le. The subset inclusion step uses plotEncoding_image_nonzero after unfolding the image membership. The cardinality step rewrites the image card via Finset.card_image_of_injective using plotEncoding_injective, equates it to card_eq_seven, and matches against F2Power.nonzero_card_three.
why it matters
This supplies the image equality required by the downstream theorem no_eighth_plot, which states that every nonzero vector in F2Power 3 encodes a Booker plot and thereby excludes an eighth plot on three axes. It replaces an earlier hardcoded count with the actual theorem chained from F2Power.nonzero_card_three, realizing the bijection claimed in the paper's §XXIII.C and tying to the D = 3 forced in UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.