plotEncoding_image_nonzero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that every nonzero vector in F2Power 3 is attained.
- Does not supply a physical interpretation of the three axes.
- Does not invoke J-cost, defectDist or the phi-ladder.
- Does not establish the cardinality of BookerPlotFamily.
Lean usage
example (p : BookerPlotFamily) : plotEncoding p ≠ 0 := plotEncoding_image_nonzero pformal statement (Lean)
157theorem plotEncoding_image_nonzero (p : BookerPlotFamily) :
158 plotEncoding p ≠ 0 := by
proof body
Term-mode proof.
159 cases p <;> decide
160
161/-- The image of `plotEncoding` is exactly the seven non-zero
162 vectors of `F2Power 3`. -/