axis12
plain-language theorem explainer
axis12 defines the specific vector (1,1,0) inside the 3-dimensional vector space over F2. Researchers encoding the seven Booker plot families would cite this definition when mapping narrative structures to the non-zero elements of (Z/2)^3. The implementation is a direct constant assignment of the vector literal.
Claim. The vector $v = (1,1,0)$ in the elementary abelian 2-group of rank 3, modeled as functions from Fin 3 to Bool with pointwise XOR.
background
The module defines F2Power D as Fin D → Bool equipped with pointwise XOR, yielding the elementary abelian 2-group of rank D. For D=3 the module proves there are exactly seven non-zero elements via nonzero_card_three and decomposes them by Hamming weight into 1+3+3+1. axis12 supplies one of the three weight-2 vectors in this decomposition.
proof idea
This is a direct definition that assigns the vector literal ![true, true, false] to the name axis12 in type F2Power 3.
why it matters
This definition supplies the concrete representative needed by plotEncoding to map the theQuest plot family onto one of the seven non-zero vectors in F2Power 3. It realizes the explicit axis encoding of the seven Booker plot families asserted in Theorem 9 of Seven_Plots_Three_Dimensions.tex and supports the subgroup bijection described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.