weight_zero_iff
plain-language theorem explainer
The equivalence asserts that for v in the elementary abelian 2-group of rank D, modeled as functions Fin D to Bool, the Hamming weight vanishes exactly when v is the zero vector. Researchers deriving the 1+3+3+1 weight partition at D=3 for Booker's plot families cite it to anchor the unique zero element. The proof is a bidirectional tactic proof that unfolds the weight definition, applies Finset.card_eq_zero, performs coordinate case analysis, and invokes the zero-weight lemma in the reverse direction.
Claim. Let $v$ be a function from the finite set of $D$ indices to the Boolean values. Let $w(v)$ be the cardinality of the set of indices at which $v$ evaluates to true. Then $w(v)=0$ if and only if $v$ is the constant-false function.
background
The module defines F2Power D as the type Fin D → Bool equipped with pointwise XOR, yielding an AddCommGroup and Fintype instance whose cardinality is 2^D. Hamming weight is the cardinality of the Finset of indices where the function returns true; the sibling lemma hammingWeight_zero already records that this weight is zero on the zero vector. The local setting is the theorem module that converts the combinatorial count of seven non-zero elements at D=3 into a proved statement, replacing the assertion in the companion paper Seven_Plots_Three_Dimensions.tex that this count supplies Booker's seven basic plot families.
proof idea
The tactic proof opens with constructor to split the biconditional. The left-to-right direction unfolds hammingWeight, rewrites with Finset.card_eq_zero, applies funext, and performs case analysis on v i to derive a contradiction from the assumption that any coordinate is true. The right-to-left direction substitutes the hypothesis v=0 and applies the upstream lemma hammingWeight_zero.
why it matters
The result is invoked by the downstream theorem card_weight_zero_three, which uses it inside an extensionality argument to conclude that the weight-zero subset at D=3 is exactly the singleton containing zero. This step completes the 1+3+3+1 partition that matches Booker's classification and supplies the seven subgroups required by NarrativeGeodesic and KinshipGraphCohomology. It thereby discharges the combinatorial prerequisite for the seven-element lists asserted in the companion paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.