axis1
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove any algebraic property of the vector beyond its explicit value.
- Does not generalize the construction to dimensions other than 3.
- Does not define or reference the companion vectors axis2 and axis3.
Lean usage
example : plotEncoding .ragsToRiches = axis1 := rflformal statement (Lean)
203def axis1 : F2Power 3 := ![true, false, false]