singleAxis_plots
plain-language theorem explainer
The theorem establishes that Rags to Riches, Voyage and Return, and Comedy each transform exactly one narrative axis under the F₂³ encoding of Booker's plots. Researchers classifying narrative structures via the Recognition Science cube geometry would cite this when separating primary from compound plots. The proof is a one-line term that unfolds the weight definition to the explicit vector map and decides the resulting equalities by computation.
Claim. Let $w$ be the Hamming weight of the encoding of a Booker plot family into the nonzero vectors of $F_2^3$. Then $w$ (Rags to Riches) = 1, $w$ (Voyage and Return) = 1, and $w$ (Comedy) = 1.
background
The module develops the narrative geodesic on the cube $Q_3 = (Z/2Z)^3$, placing Booker's seven plot families in explicit bijection with the seven nonzero elements of $F_2^3$ via the axis assignment of Theorem 9 in the companion paper. The three axes are protagonist status, world status, and value alignment. plotEncoding sends each plot family to its corresponding vector in $F_2^3$, with Rags to Riches to the first standard basis vector, Voyage and Return to the second, and Comedy to the third. plotWeight extracts the Hamming weight of that vector, which counts the number of axes transformed by the plot. F2Power models the elementary abelian 2-group of rank D as Fin D → Bool, and hammingWeight counts the true coordinates.
proof idea
The proof is a one-line term wrapper. It refines the conjunction into three subgoals and discharges each by unfolding plotWeight to F2Power.hammingWeight composed with plotEncoding, then invoking decide on the resulting numerical statement.
why it matters
The result isolates the three single-axis plots within the seven-family classification on the F₂³ cube, confirming they correspond to the weight-1 vectors. It supports the structural bijection proved elsewhere in the module and aligns with the Recognition Science use of D = 3 spatial dimensions realized as the rank of F2Power. No downstream theorems depend on it directly, so it functions as a classification lemma rather than a bridge to further results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.