oneDimSubspace
The definition returns the two-element set consisting of the zero vector and a given vector v inside the elementary abelian 2-group of rank D. Researchers counting the seven lines through the origin in (Z/2)^3 for the Booker plot families cite this construction when building the subgroup lattice. The implementation is a direct Finset literal that exploits the relation v + v = 0 to close the span.
claimFor a vector $v$ in the $D$-dimensional vector space over the field with two elements, the one-dimensional subspace generated by $v$ is the set consisting of the zero vector and $v$.
background
The module defines the type as the set of functions from Fin D to Bool with pointwise XOR serving as the group operation. This yields the elementary abelian 2-group of rank D, whose cardinality is 2 to the power D. The upstream result F2Power establishes the type and its group structure.
proof idea
This is a definition returning the Finset consisting of the zero element and the input vector. It is a one-line wrapper that applies the set constructor directly.
why it matters in Recognition Science
It is invoked by the cardinality theorem that shows each such subspace contains exactly two elements and by the closure theorem that confirms the set is closed under addition. These results in turn establish the existence of seven distinct one-dimensional subspaces for D equal to 3, matching the assertion in the companion paper that the count 7 arises from (Z/2)^3 excluding zero. The definition thereby supplies the concrete objects needed for the subgroup lattice in downstream modules on narrative geodesics and cube bridges.
scope and limits
- Does not impose the condition that the generating vector is nonzero.
- Does not include a proof that the set is closed under the group operation.
- Does not address subspaces of dimension higher than one.
- Does not enumerate all one-dimensional subspaces for a given D.
Lean usage
theorem card_example (v : F2Power 3) (hv : v ≠ 0) : (oneDimSubspace v).card = 2 := oneDimSubspace_card v hvformal statement (Lean)
241def oneDimSubspace (v : F2Power D) : Finset (F2Power D) :=
proof body
Definition body.
242 {0, v}
243