oneDimSubspace_closed
plain-language theorem explainer
The one-dimensional subspace generated by any vector v in the elementary abelian 2-group of rank D is closed under addition. Workers on the Booker plot families and narrative geodesic constructions cite this to establish that each nonzero element spans a subgroup of order two. The argument exhausts the four combinations of elements from the two-point set and reduces them with the identity that every element squares to zero.
Claim. Let $V = (Z/2Z)^D$. For any $v$ in $V$, let $S = {0, v}$. If $a, b$ belong to $S$, then $a + b$ belongs to $S$.
background
The module defines F2Power D as the type Fin D to Bool equipped with pointwise XOR as the group operation, making it the elementary abelian 2-group of rank D. The one-dimensional subspace generated by a nonzero v is the Finset consisting of the zero vector and v itself. This closure result relies on the upstream lemma that v + v = 0 for any v, which follows immediately from the definition of XOR.
proof idea
The proof unfolds the definition of the subspace to expose the membership conditions a equals 0 or a equals v (and likewise for b). It then performs case analysis on these disjunctions, substitutes the resulting equalities, and simplifies each of the four cases using the add_self theorem that any element added to itself yields zero.
why it matters
This closure property is required to confirm that each nonzero element of the rank-3 case generates a genuine subgroup of order two, yielding the seven subgroups needed for the Booker bijection in Aesthetics.NarrativeGeodesic. It fills the algebraic prerequisite stated in the module documentation for replacing hardcoded counts with proved theorems. The result sits inside the D = 3 specialization that connects to the eight-tick octave structure in the broader Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.