axis13
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not verify any group axioms or addition table for the ambient space.
- Does not enumerate or classify the remaining six nonzero vectors.
- Does not derive mass formulas, forcing-chain steps, or physical constants.
- Does not address uniqueness of the chosen encoding among possible labelings.
Lean usage
def plotForTragedy : F2Power 3 := axis13formal statement (Lean)
221def axis13 : F2Power 3 := ![true, false, true]