hammingWeight_le
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not provide a matching lower bound on Hamming weight.
- Does not enumerate the vectors achieving each possible weight.
- Does not extend the bound to other group operations or infinite-dimensional analogs.
- Does not invoke the group law or the addition operation in F2Power.
formal statement (Lean)
159theorem hammingWeight_le (v : F2Power D) : hammingWeight v ≤ D := by
proof body
Tactic-mode proof.
160 unfold hammingWeight
161 calc (Finset.univ.filter (fun i => v i = true)).card
162 ≤ Finset.univ.card := Finset.card_filter_le _ _
163 _ = D := by simp [Finset.card_univ, Fintype.card_fin]
164