oneDimSubspace_card
plain-language theorem explainer
The result shows that the one-dimensional subspace generated by any nonzero vector v in the elementary abelian 2-group F2Power D has cardinality exactly 2. Researchers modeling the seven Booker plot families via (Z/2)^3 or chaining combinatorial counts in Recognition Science would cite this fact. The proof is a direct term-mode simplification that unfolds the two-element Finset definition and invokes the insert-cardinality lemma under the distinctness hypothesis.
Claim. Let $D$ be a natural number and let $v$ be a nonzero element of the elementary abelian 2-group of rank $D$, realized as maps from Fin $D$ to Bool under pointwise XOR. The one-dimensional subspace generated by $v$, defined as the Finset containing zero and $v$, has cardinality 2.
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 whose cardinality is 2^D. The companion definition oneDimSubspace v constructs the explicit Finset {0, v}. This algebraic setup is introduced to replace hardcoded counts with theorems, supporting the claim that the number of nonzero elements is 2^D - 1 and, at D = 3, exactly 7 elements as required for the Booker plot families.
proof idea
The term proof unfolds the definition of oneDimSubspace to obtain the Finset {0, v}, then applies simp using Finset.card_insert_of_notMem together with the symmetry of the nonzero hypothesis hv to conclude that the inserted element is distinct and the cardinality equals 2.
why it matters
This supplies the verified cardinality of each 1-dimensional subgroup in F2Power 3, enabling the exact count of 7 such subgroups that correspond to the basic plot families. It feeds the constructions in Aesthetics.NarrativeGeodesic and Patterns.TwoToTheDMinusOne by replacing ad-hoc definitions with a theorem. In the Recognition Science framework it anchors the combinatorial origin of the number 7 in the D = 3 case, consistent with the spatial dimension fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.