plotWeight
plain-language theorem explainer
plotWeight maps each Booker plot family to the integer count of narrative axes it activates, obtained by taking the Hamming weight of its assigned nonzero vector in F2Power 3. Narrative theorists citing the Recognition Science aesthetics section would reference this when quantifying plot dimensionality on the cube Q3. The definition is realized as the direct composition of plotEncoding with F2Power.hammingWeight.
Claim. For a Booker plot family $p$, the weight $w(p)$ equals the Hamming weight of the vector assigned to $p$ by the encoding map from the seven families to the nonzero elements of $F_2^3$.
background
BookerPlotFamily is the inductive type whose seven constructors (overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy, tragedy, rebirth) stand in explicit bijection with the seven nonzero vectors of F2Power 3 via plotEncoding. F2Power D is the elementary abelian 2-group Fin D → Bool with pointwise XOR; hammingWeight counts the true coordinates of such a vector. The module NarrativeGeodesic realizes the structural closure of the seven-plot bijection stated in Seven_Plots_Three_Dimensions.tex (Theorem 9), replacing an earlier hardcoded count with the actual F2Power 3 cardinality.
proof idea
The definition is a one-line wrapper that applies F2Power.hammingWeight to the result of plotEncoding p.
why it matters
plotWeight supplies the integer values verified by the downstream theorems singleAxis_plots (weight 1), twoAxis_plots (weight 2), and threeAxis_plots (weight 3). It completes the explicit bijection step of the aesthetics module, tying narrative axis count to the rank-3 cube in the Recognition framework and preparing the ground for J-cost interpretations of plot tension. The parent result is the proved cardinality booker_seven_eq_2_pow_3_minus_1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.