axis1
plain-language theorem explainer
axis1 defines the first standard basis vector in the 3-dimensional vector space over F2, given explicitly as the function that evaluates to true only at index 0. Narrative theorists and algebraists working on the seven Booker plot families cite this when labeling the weight-1 generators of (Z/2Z)^3. The definition is a direct constant assignment that instantiates the type F2Power 3 with no further computation.
Claim. Let $V = (F_2)^3$ be the elementary abelian 2-group of rank 3. Define the vector $e_1$ in $V$ by $e_1(0) = 1$, $e_1(1) = 0$, $e_1(2) = 0$.
background
The module Algebra.F2Power defines F2Power D as the type Fin D → Bool with pointwise XOR as the group operation, forming the vector space (F_2)^D. The module documentation states that this supplies the elementary abelian 2-group of rank D together with its Fintype instance and the cardinality result 2^D. At D = 3 the three weight-1 vectors are singled out by the doc-comment as the generators used for the 1+3+3+1 weight decomposition.
proof idea
This is a direct definition that assigns the literal vector notation ![true, false, false] to the constant axis1. No lemmas or tactics are invoked; the declaration simply instantiates the type F2Power 3.
why it matters
The definition supplies the concrete representative for axis 1 in the Booker plot encoding, as consumed by plotEncoding which maps .ragsToRiches to axis1. It feeds the weight-1 case of the D = 3 decomposition and the structures RSDisjointSum3 and RSIndependentTriple in the foundation layer. This realizes the paper claim that the count 7 arises from the nonzero elements of (Z/2Z)^3 rather than a hardcoded list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.