axis123
plain-language theorem explainer
axis123 supplies the all-ones vector in the three-dimensional vector space over F2. Researchers working on the seven Booker plot families cite it as the unique weight-three element completing the 1+3+3+1 decomposition at D=3. The definition is introduced by a direct vector literal in the Fin 3 to Bool representation.
Claim. Let $V = (Z/2Z)^3$. Then $v := (1,1,1)in V$ is the unique vector of Hamming weight 3.
background
F2Power D is the type Fin D to Bool equipped with pointwise XOR as the group operation, forming the elementary abelian 2-group of rank D. The module establishes that the nonzero elements number exactly 2^D - 1, with the D=3 case yielding the seven nonzero vectors that label the plot families. The local setting is the algebraic foundation for the bijection in Seven_Plots_Three_Dimensions.tex, where each nonzero vector generates a one-dimensional subgroup under XOR.
proof idea
The definition is a direct abbreviation that applies the vector constructor to the triple (true, true, true) in the F2Power 3 representation.
why it matters
This definition supplies the weight-three vector required by the 1+3+3+1 decomposition at dimension three. It feeds plotEncoding, which maps the seven plot families to the nonzero vectors of F2Power 3, and axis123_weight, which verifies the Hamming weight equals three. The construction closes the algebraic count of seven subgroups in (Z/2Z)^3 minus zero that underpins Theorem 9 of the plots paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.