axis3
plain-language theorem explainer
axis3 defines the third standard basis vector in the elementary abelian 2-group F2Power 3, realized as the map from Fin 3 to Bool that returns true only at index 2. Researchers encoding the seven Booker plot families would cite it when assigning the comedy family to the value-alignment axis in the explicit bijection of Theorem 9. The construction is a direct literal assignment with no lemmas or computation.
Claim. In the vector space $V = (Z/2Z)^3$ modeled by $Fin 3 → Bool$ with pointwise XOR, the vector $e_3$ is the standard basis element satisfying $e_3(2) = true$ and $e_3(i) = false$ for $i < 2$.
background
F2Power D is the type Fin D → Bool equipped with pointwise XOR, forming the elementary abelian 2-group of rank D. The module establishes that its cardinality is 2^D and that the number of nonzero elements is exactly 2^D - 1, which equals 7 at D = 3; this count is the algebraic source of the seven basic plot families asserted in Seven_Plots_Three_Dimensions.tex. The three weight-1 vectors (axis1, axis2, axis3) together with their sums furnish the 1+3+3+1 decomposition of the nonzero elements.
proof idea
This is a direct definition that binds axis3 to the literal vector constructor ![false, false, true]. No lemmas are applied and no tactics are executed; the body is the explicit term that constructs the required element of F2Power 3.
why it matters
axis3 is invoked by plotEncoding to map the comedy family to the third axis and by axis3_weight to confirm its Hamming weight equals 1. It supplies one leg of the RSIndependentTriple and RSDisjointSum3 structures that realize the three coupled axes. The definition therefore closes the explicit basis required to prove that (Z/2Z)^3 minus zero contains exactly seven elements, linking the algebraic count directly to the D = 3 case of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.