axis23
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not prove any algebraic property of the element such as its order under addition.
- Does not participate in the proofs of the group structure or the cardinality lemmas.
- Does not generalize the construction to dimensions other than 3.
- Does not compute derived quantities such as Hamming weight or subgroup membership.
Lean usage
def exampleEncoding : F2Power 3 := axis23formal statement (Lean)
222def axis23 : F2Power 3 := ![false, true, true]
proof body
Definition body.
223
224/-- The unique weight-3 vector. -/