axis1
axis1 supplies the explicit first standard basis vector in the three-dimensional F2-vector space whose seven nonzero elements label the basic plot families. Researchers on narrative classification or the Booker bijection cite it when mapping families such as rags-to-riches to their axis coordinate. The declaration is a direct vector-literal assignment that instantiates the Fin 3 to Bool representation with a single true entry.
claimLet $V = (Z/2Z)^3$ be the elementary abelian 2-group of rank 3, realized as functions from Fin 3 to Bool with pointwise XOR. Define the first weight-one vector by $e_1 := (1,0,0)$, where true stands for the additive identity's opposite.
background
The module defines F2Power D as the type Fin D → Bool equipped with pointwise XOR, yielding the elementary abelian 2-group of rank D. Its Fintype instance gives card_eq : Fintype.card (F2Power D) = 2^D, and the nonzero_card corollary isolates the 2^D - 1 nonzero elements. At D = 3 this produces exactly seven nonzero vectors, which the module doc links directly to the seven basic plot families asserted in Seven_Plots_Three_Dimensions.tex.
proof idea
Direct definition that applies the vector literal constructor to the Boolean triple (true, false, false). No lemmas or tactics are invoked; the declaration simply names the concrete element of the already-defined F2Power 3 type.
why it matters in Recognition Science
The definition is the concrete representative used by NarrativeGeodesic.plotEncoding to assign the seven plot families to the nonzero vectors of F2Power 3, realizing Theorem 9 of the companion paper. It is referenced by axis1_weight, the RSDisjointSum3 and RSIndependentTriple structures, and PlanetStrataCert. Within the Recognition framework it supplies the D = 3 case that follows from the eight-tick octave and the T8 forcing of three spatial dimensions.
scope and limits
- Does not prove any algebraic closure or subgroup properties of the vector.
- Does not generalize the construction to dimensions other than 3.
- Does not address physical or geometric interpretations of the axes.
- Does not claim uniqueness among all possible weight-one vectors.
Lean usage
def plotExample : F2Power 3 := axis1formal statement (Lean)
203def axis1 : F2Power 3 := ![true, false, false]