axis3
plain-language theorem explainer
The declaration supplies the concrete vector with a single 1 in the third coordinate inside the elementary abelian 2-group of rank 3. Authors of aesthetics and coupled-axis modules cite it when encoding the seven non-zero elements of (Z/2)^3 as plot families or independent axes. It is introduced by a direct one-line assignment that instantiates the F2Power type constructor at D=3.
Claim. Let $e_3$ be the element of the vector space $V = (Fin 3) → Bool$ (with pointwise addition modulo 2) whose components are $(false, false, true)$.
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 together with its Fintype instance and cardinality 2^D. The companion paper Seven_Plots_Three_Dimensions.tex asserts that the 7 non-zero elements at D=3 label Booker's basic plot families; the module proves the count via nonzero_card_three and supplies the weight decomposition 1+3+3+1. The upstream definition F2Power supplies the underlying type whose elements are these vectors.
proof idea
Direct definition that lists the three Boolean components explicitly.
why it matters
This definition is referenced by plotEncoding to map the comedy family onto the third axis and by axis3_weight to confirm Hamming weight 1. It participates in the 1+3+3+1 decomposition that supports the subgroup count feeding RSIndependentTriple and RSDisjointSum3. It instantiates the D=3 case required by the forcing chain step that fixes spatial dimensions at three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.