twoAxis_plots
plain-language theorem explainer
The declaration establishes that the compound narrative plots The Quest, Tragedy, and Overcoming the Monster each transform exactly two axes under the encoding into the three-dimensional vector space over F2. Researchers verifying the structural correspondence between Booker's seven plot families and the nonzero elements of F2^3 would cite this result to confirm the two-axis weight assignments in the bijection. The proof is a direct term-mode computation that unfolds the weight and encoding definitions then applies a decision procedure on the 8
Claim. Let $w$ denote the Hamming weight of the encoding vector in $F_2^3$ for a Booker plot family. Then $w($The Quest$) = 2$, $w($Tragedy$) = 2$, and $w($Overcoming the Monster$) = 2$.
background
The module develops a narrative geodesic on the cube $Q_3 = (Z/2Z)^3$, establishing an explicit bijection between Booker's seven plot families and the seven nonzero vectors in this space per the assignment table in Seven_Plots_Three_Dimensions.tex. The three axes are protagonist status, world status, and value alignment. The encoding map assigns each plot family to a distinct nonzero vector in $F_2^3$, modeled as Fin 3 to Bool with pointwise XOR. The weight function is the Hamming weight of this vector, which counts the number of narrative axes transformed by the plot. Upstream, hammingWeight is defined as the cardinality of the set of coordinates equal to true.
proof idea
The proof is a one-line term wrapper. It refines the conjunction into three separate goals and then unfolds the definitions of plotWeight, plotEncoding, and hammingWeight before invoking the decide tactic to verify the equalities on the concrete vectors.
why it matters
This result completes the weight verification for the two-axis plots in the bijection between BookerPlotFamily and the nonzero elements of F2Power 3, supporting the structural closure of the narrative model. It aligns with the framework's assignment of D = 3 spatial dimensions and the explicit mapping in Theorem 9 of the referenced paper. The computation is fully discharged with no open questions touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.