axis23
plain-language theorem explainer
The definition constructs the element of the rank-three elementary abelian 2-group whose support lies on the second and third coordinates. Researchers mapping Booker plot families to the seven nonzero vectors of (Z/2Z)^3 cite this when assigning combined-axis encodings in narrative geometry. The definition is a direct boolean-vector literal with no computation or lemma application.
Claim. Define the vector $v$ in the elementary abelian 2-group of rank 3 by the boolean triple $(0,1,1)$, where the coordinates label the three axes.
background
The F2Power module models the elementary abelian 2-group of rank D as the type Fin D → Bool with pointwise XOR as the group operation. At D = 3 the module proves there are exactly seven nonzero elements and establishes the 1+3+3+1 decomposition by Hamming weight via separate cardinality lemmas. The companion paper Seven_Plots_Three_Dimensions.tex asserts that these seven elements correspond to Booker's basic plot families; the module supplies the proved count that downstream code can use instead of a hardcoded constant.
proof idea
The definition is a direct application of the vector constructor to the boolean triple false, true, true.
why it matters
This supplies one of the explicit vectors required by the plotEncoding definition, which realizes the bijection between the seven Booker plot families and the nonzero elements of (Z/2Z)^3 asserted in Theorem 9 of the companion paper. It participates in the subgroup-counting argument that produces exactly seven families from the rank-three group. The construction rests on the F2Power type and the nonzero-cardinality result proved in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.