axis2_weight
plain-language theorem explainer
The theorem states that the Hamming weight of the specific vector axis2 in the three-dimensional F2 vector space equals one. Researchers counting weight classes in (Z/2)^3 for the decomposition into 1+3+3+1 would cite this when establishing the three weight-one elements. The proof is a direct term-mode reduction that unfolds the weight definition and the explicit vector, then applies a decision procedure to confirm the single true coordinate.
Claim. Let $v = (0,1,0) $ in the vector space over $mathbb{F}_2$ of dimension 3. The Hamming weight of $v$, defined as the number of coordinates equal to 1, equals 1.
background
The module defines F2Power D as the type Fin D to Bool, equipped with pointwise XOR as the abelian group operation, yielding the elementary abelian 2-group of rank D. Hamming weight of a vector v counts the number of coordinates equal to true. The vector axis2 is the explicit element with false in the first and third positions and true in the second, so it has exactly one true coordinate by construction. This sits inside the broader development of weight statistics for D=3, including the decomposition of the 7 nonzero elements into weight classes 1, 2, and 3.
proof idea
The proof is a one-line term wrapper. It unfolds the definitions of hammingWeight and axis2, then invokes the decide tactic, which reduces the equality to a concrete boolean check on the single true entry and confirms it holds.
why it matters
This result supplies one of the four weight-class cardinalities needed to prove the 1+3+3+1 partition of the seven nonzero vectors in F2Power 3. It therefore supports the module's main theorem that the nonzero count equals 7, which the companion paper Seven Plots Three Dimensions uses to derive the asserted count of seven basic plot families from (Z/2)^3 minus the origin. The declaration closes a small but necessary verification step in the chain from the group definition to the combinatorial count that downstream aesthetics and narrative modules rely upon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.