add_self
plain-language theorem explainer
The theorem establishes that every element v of the elementary abelian 2-group F2Power D satisfies v + v = 0 under pointwise XOR. Researchers deriving the seven Booker plot families from (Z/2)^3 and working on narrative geodesics cite this cancellation law. The proof reduces the claim to the boolean XOR identity via functional extensionality followed by case analysis on each coordinate.
Claim. For every function $v : Fin D → Bool$, where addition is pointwise XOR, the identity $v + v = 0$ holds in the elementary abelian 2-group of rank $D$.
background
F2Power D is defined as the type Fin D → Bool equipped with pointwise XOR as the group operation, realizing the elementary abelian 2-group of rank D. The module documentation explains that this construction proves the count of seven for Booker's basic plot families arises from the nonzero elements of (Z/2)^3, supplying a rigorous algebraic foundation instead of a hardcoded definition. The upstream definition of F2Power provides the underlying type and group structure.
proof idea
The term proof applies functional extensionality to reduce the functional equality to pointwise equality. For each index i it shows xor (v i) (v i) = false by case analysis on the boolean value of v i, with both cases resolving by reflexivity.
why it matters
This supplies the characteristic-2 cancellation property used by plot_composition_cancels_iff in Aesthetics.NarrativeGeodesic to conclude that vanishing composite XOR implies equality of plots. It likewise enables oneDimSubspace_closed by guaranteeing closure of each 1-dimensional subspace {0, v}. In the Recognition Science framework it underpins the derivation of exactly seven subgroups from the nonzero elements of (Z/2)^3, linking directly to the seven plot families asserted in the companion paper and to the T7 eight-tick octave at D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.