card_weight_zero_three
plain-language theorem explainer
The theorem states that exactly one vector in F2^3 has Hamming weight zero. Algebraists and Recognition Science modelers working on the 1+3+3+1 weight partition of the 8-element group would cite it to ground the zero class before counting the seven nonzero elements. The proof reduces the filtered finset to the singleton {0} via the weight-zero equivalence and concludes by reflexivity.
Claim. Let $V = (F_2)^3$ and let $wt(v)$ denote the Hamming weight of $v$. Then $|{v in V : wt(v) = 0}| = 1$.
background
F2Power D is defined as the type Fin D → Bool, equipped with pointwise XOR as the abelian group operation. Hamming weight of a vector v counts the number of coordinates equal to true. The supporting lemma weight_zero_iff states that this weight equals zero if and only if v is the zero vector. The module proves the full weight decomposition 1+3+3+1 at D=3 so that the count of seven nonzero elements can be used downstream instead of a hardcoded constant.
proof idea
The tactic proof first establishes an extensional equality between the filtered finset and the singleton {0} by applying simp with the weight_zero_iff lemma. It then rewrites the original cardinality expression with this equality and finishes with reflexivity.
why it matters
This result supplies the weight-zero term in the 1+3+3+1 partition of F2^3, which the module documentation uses to prove that the number of nonzero elements is exactly 7. That count replaces an assertion in the companion paper Seven_Plots_Three_Dimensions.tex and feeds the subgroup bijection in Aesthetics.NarrativeGeodesic. It thereby closes the algebraic foundation for the D=3 case before any Recognition Science forcing or phi-ladder arguments are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.