oneDimSubspace
plain-language theorem explainer
The definition produces the two-element set consisting of the zero vector and an arbitrary vector v inside the D-dimensional vector space over the field with two elements. Researchers counting subgroups of (Z/2)^D or establishing the seven one-dimensional subgroups at D=3 cite this construction. The implementation is a direct Finset literal with no further computation.
Claim. Let $V = (F_2)^D$. For any $v$ in $V$, the one-dimensional subspace spanned by $v$ is the set $ {0, v} $.
background
F2Power D is defined as the type Fin D → Bool equipped with pointwise XOR as addition, forming the elementary abelian 2-group of rank D. This realizes the D-dimensional vector space over GF(2), where the zero element is the constant-false function. The module documentation notes that this type yields the count of nonzero elements equal to 2^D - 1, with the D=3 case giving exactly seven nonzero vectors that label the basic plot families in the companion paper.
proof idea
The definition is a direct Finset literal that assembles the set containing the zero element and the input vector v.
why it matters
This definition supplies the object whose cardinality equals two (oneDimSubspace_card) and whose closure under addition holds (oneDimSubspace_closed). It thereby enables the enumeration of the seven one-dimensional subgroups of (Z/2)^3 that the module documentation links to the Booker bijection in Aesthetics.NarrativeGeodesic and to the asserted count of seven plot families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.