hammingWeight_zero
plain-language theorem explainer
The declaration proves that the Hamming weight of the zero element in the elementary abelian 2-group of rank D is zero. Algebraists modeling vector spaces over GF(2) cite it when reducing expressions at the origin in weight calculations. The proof is a term-mode reduction that unfolds the weight definition and applies the zero_apply fact to conclude the filtered set is empty.
Claim. Let $V$ be the elementary abelian 2-group of rank $D$, realized as functions from Fin $D$ to Bool with pointwise XOR. The Hamming weight of the zero vector satisfies wt$(0) = 0$.
background
F2Power D is the type Fin D → Bool equipped with pointwise XOR as the group operation, forming the vector space (Z/2Z)^D. The Hamming weight of a vector v counts the cardinality of indices i where v i equals true. The zero vector is the constant false function, as stated by the zero_apply theorem: (0 : F2Power D) i = false for every i.
proof idea
The proof unfolds hammingWeight and simplifies using the zero_apply theorem, which shows every coordinate of the zero vector is false, so the Finset filter is empty and its cardinality is zero.
why it matters
It is invoked by weight_zero_iff to establish the equivalence hammingWeight v = 0 ↔ v = 0. This fact supports the 1+3+3+1 weight decomposition at D=3 in the module, which yields the count of 7 non-zero elements and justifies the seven one-dimensional subgroups in (Z/2Z)^3 excluding zero, as required by the module documentation for the companion paper Seven_Plots_Three_Dimensions.tex and downstream modules such as Aesthetics.NarrativeGeodesic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.