hammingWeight_le
plain-language theorem explainer
The theorem bounds the Hamming weight of any element of the elementary abelian 2-group of rank D by D itself. Workers on the Recognition Science account of the seven Booker plot families cite it when partitioning the nonzero elements of (Z/2)^3 according to weight. The argument is a direct application of the general inequality between the size of a filtered finite set and the size of its ambient set, followed by simplification of the cardinality of Fin D.
Claim. For every function $v :$ Fin $D$ to Bool, the cardinality of the set of indices $i$ where $v(i)$ equals true is at most $D$.
background
The module models the elementary abelian 2-group of rank D as the set of functions from Fin D to Bool, equipped with pointwise XOR as addition. The Hamming weight of such a function v is defined as the number of coordinates where v evaluates to true. This construction supplies the combinatorial substrate for counting the 7 nonzero elements in the D=3 case, as required by the companion paper Seven_Plots_Three_Dimensions.tex.
proof idea
The proof first unfolds the definition of hammingWeight, exposing it as the cardinality of the Finset filter that selects coordinates equal to true. It then applies the standard Finset lemma that the cardinality of any filtered subset is at most the cardinality of the full universe. The final step simplifies the cardinality of the universe of Fin D to exactly D.
why it matters
This bound closes the elementary properties of the F2Power construction and enables the 1+3+3+1 weight decomposition at D=3 that underpins the bijection to the seven nonzero elements of (Z/2)^3. Downstream modules such as Aesthetics.NarrativeGeodesic rely on this decomposition to realize the subgroup structure for narrative geodesics. It directly supports the Recognition Science claim that the count of seven plot families arises from the structure of the eight-tick octave at spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.