axis1_weight
plain-language theorem explainer
axis1_weight establishes that the first standard basis vector in the 3-dimensional space over F2 has Hamming weight exactly one. Researchers counting weight classes in (Z/2Z)^3 or building the 1+3+3+1 decomposition would cite it when verifying the three weight-one elements. The argument is a direct term computation that unfolds the weight function and the explicit vector definition before applying a decision procedure.
Claim. Let $v = (true, false, false)$ be the first axis vector in $F_2^3$. The Hamming weight of $v$, defined as the number of coordinates equal to true, equals 1.
background
The module defines F2Power D as the type Fin D → Bool with pointwise XOR, yielding the elementary abelian 2-group of rank D. Hamming weight of a vector v is the cardinality of the set of indices i where v i = true. The constant axis1 is the explicit vector ![true, false, false] in F2Power 3, one of the three weight-one elements listed in the module documentation.
proof idea
The proof is a one-line term wrapper. It unfolds hammingWeight and axis1, reducing the claim to a concrete numerical equality that the decide tactic resolves by exhaustive enumeration.
why it matters
The result supplies one concrete case in the 1+3+3+1 weight decomposition at D=3 that the module uses to prove nonzero_card_three = 7. This count is required by the companion paper Seven_Plots_Three_Dimensions.tex to replace a hardcoded assertion with a theorem, enabling the subgroup bijection in downstream modules such as Aesthetics.NarrativeGeodesic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.