axis123_weight
plain-language theorem explainer
The theorem states that the all-true vector in the rank-3 elementary abelian 2-group has Hamming weight exactly 3. Researchers counting the 1+3+3+1 weight classes in (Z/2)^3 cite it to anchor the bijection from nonzero vectors to 1-dimensional subspaces. The proof is a one-line wrapper that unfolds the two definitions and invokes a decision procedure.
Claim. Let $v = (1,1,1) : (F_2)^3$. The Hamming weight of $v$, defined as the cardinality of the set of coordinates equal to true, equals 3.
background
F2Power D is defined as the type Fin D → Bool equipped with pointwise XOR as the group operation, yielding the elementary abelian 2-group of rank D. Hamming weight of a vector v is the cardinality of the Finset of indices i where v i equals true. axis123 is the constant-true vector in dimension 3, described in its definition as the unique weight-3 vector. The module establishes the full weight distribution at D=3 as the partition 1+3+3+1 and the bijection from the 7 nonzero vectors to the 7 one-dimensional subspaces.
proof idea
The proof is a one-line wrapper that unfolds hammingWeight and axis123, then applies the decide tactic to confirm the resulting numerical equality.
why it matters
This theorem supplies the weight-three term in the 1+3+3+1 decomposition required for the subgroup count in the F2Power module. The module document states that the count of 7 for Booker's basic plot families is proved here rather than asserted, enabling downstream chaining in Aesthetics.NarrativeGeodesic and Patterns.TwoToTheDMinusOne. It directly supports the combinatorial step from (Z/2)^3 to the seven 1-dimensional subspaces used in the companion paper Seven_Plots_Three_Dimensions.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.