axis2
plain-language theorem explainer
The definition supplies the second standard basis vector in the elementary abelian group (Z/2Z)^3. Narrative theorists cite it when labeling the voyage-and-return plot family among the seven nonzero elements. The construction is a direct literal assignment of the Boolean vector with a single true entry in the middle coordinate.
Claim. Let $V = (Z/2Z)^3$. Define the vector $e_2$ in $V$ by $e_2(0) = 0$, $e_2(1) = 1$, $e_2(2) = 0$.
background
F2Power D is defined as Fin D → Bool with pointwise XOR as the group operation, yielding the elementary abelian 2-group of rank D. The module proves that this group has 2^D elements and exactly 2^D - 1 nonzero elements; the D = 3 case produces the seven vectors that classify Booker plot families. The upstream F2Power definition supplies the underlying type together with its Fintype and DecidableEq instances.
proof idea
This is a one-line definition that directly constructs the vector literal ![false, true, false] of type F2Power 3.
why it matters
The vector is the image of the voyageAndReturn family under the encoding map in NarrativeGeodesic.plotEncoding, which realizes the bijection between the seven Booker families and the nonzero elements of (Z/2Z)^3 from Theorem 9 of the companion paper. It also feeds the weight computation axis2_weight and enters the independent-axis constructions in RSCoupledAxis. The definition supplies the concrete representatives that convert the algebraic count of seven into the aesthetic plot classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.