axis13
plain-language theorem explainer
axis13 supplies the concrete vector with true in the first and third slots and false in the middle inside the rank-3 elementary abelian 2-group. Narrative geodesic encodings cite this vector to label the tragedy plot family within the seven-family bijection. The declaration is a direct literal assignment of the Fin-vector notation.
Claim. In the three-dimensional vector space over the field with two elements, realized as maps from a three-element index set to the booleans with pointwise exclusive-or addition, the element whose values are true, false, true at the three successive indices.
background
The module models the elementary abelian 2-group of rank D as the set of all functions from Fin D to Bool, with addition given by pointwise XOR. This construction yields a group of order 2^D whose nonzero elements number exactly 2^D - 1. For D = 3 the module further records the weight decomposition 1 + 3 + 3 + 1 under the Hamming weight function that counts the number of true entries.
proof idea
Direct definition that constructs the literal three-component vector and binds it to the name axis13. No lemmas or tactics are invoked; the declaration rests only on the underlying type being Fin 3 to Bool.
why it matters
The constant supplies one of the seven explicit labels required by the plotEncoding map that realizes the bijection between nonzero group elements and Booker's seven basic plot families. It therefore closes the combinatorial step asserted in the companion paper Seven_Plots_Three_Dimensions.tex and used by the downstream aesthetics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.