hammingWeight
plain-language theorem explainer
The function counting true coordinates in a vector from the elementary abelian 2-group of rank D. Narrative geometers cite it to classify the seven Booker plot families by axis multiplicity at D=3. The definition extracts this count directly as the cardinality of the support set in the Fin D to Bool representation.
Claim. For $v :$ Fin $D$ to Bool, the Hamming weight $w(v)$ equals the cardinality of the set of indices $i$ where the $i$-th coordinate of $v$ equals true.
background
F2Power D is the type Fin D to Bool equipped with pointwise XOR, forming the elementary abelian 2-group of rank D. The module establishes that this group has cardinality 2^D and exactly 2^D minus 1 nonzero elements, with the weight function supplying the 1+3+3+1 decomposition at D=3. The companion paper Seven_Plots_Three_Dimensions.tex asserts that these counts arise from (Z/2)^3 excluding zero; the module converts the assertion into theorems.
proof idea
One-line definition that applies the cardinality operator to the Finset obtained by filtering Finset.univ on the predicate that the coordinate equals true.
why it matters
This definition feeds plotWeight, singleAxis_plots, twoAxis_plots and threeAxis_plots in NarrativeGeodesic, which assign the seven plot families their axis counts. It realizes the subgroup count for (Z/2)^3 that matches the seven basic plots, closing the combinatorial step required by the Recognition framework at T8 where D equals 3. The weight decomposition also supports the J-cost analysis of narrative tension in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.