plotWeight
plain-language theorem explainer
plotWeight maps each Booker plot family to the Hamming weight of its vector in F2^3, yielding the count of transformed narrative axes. Researchers classifying plots by axis multiplicity in the Recognition aesthetics module cite it to separate single-axis, two-axis, and three-axis cases. The definition is a direct composition of the explicit encoding map with the coordinate-count function on F2Power 3.
Claim. Let $p$ be one of the seven Booker plot families. The axis-count function returns the number of true coordinates in the nonzero vector of $(Z/2Z)^3$ assigned to $p$ by the explicit bijection from the paper.
background
The module realizes Booker's seven plots as the nonzero elements of the cube $Q_3 = F_2^3$, with the bijection given by plotEncoding per Theorem 9 of the aesthetics paper. BookerPlotFamily is the inductive type whose seven constructors correspond one-to-one with those vectors. F2Power D is defined as Fin D → Bool; hammingWeight(v) returns the cardinality of the set of indices i where v i equals true. The local setting is the structural closure of narrative geodesics on the cube, extending the Recognition framework beyond music to the seven-plot classification.
proof idea
One-line definition that applies hammingWeight to the result of plotEncoding p.
why it matters
The definition supplies the axis counts verified by the downstream theorems singleAxis_plots, twoAxis_plots, and threeAxis_plots, which establish weights 1, 2, and 3 respectively. It operationalizes the bijection between Booker's families and the seven nonzero vectors of F2Power 3, closing the structural part of the aesthetics paper. In the Recognition framework it ties the narrative side to the three-dimensional cube (D = 3) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.