plotWeight
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute J-cost or defect distance for any plot.
- Does not extend the encoding or weight beyond the seven Booker families.
- Does not prove injectivity or surjectivity of plotEncoding.
- Does not incorporate constants from the forcing chain or mass ladder.
Lean usage
example : plotWeight .comedy = 1 := by unfold plotWeight plotEncoding F2Power.hammingWeight; decideformal statement (Lean)
253def plotWeight (p : BookerPlotFamily) : ℕ :=
proof body
Definition body.
254 F2Power.hammingWeight (plotEncoding p)
255
256/-- The three single-axis plots (primary): Rags to Riches, Voyage and
257 Return, Comedy. -/