Q3_nontrivial_subgroup_count
plain-language theorem explainer
The theorem establishes that the three-dimensional vector space over the field with two elements has exactly seven nonzero vectors. Researchers formalizing the bijection between Booker plot families and algebraic structures in Recognition Science cite this count to anchor the narrative geodesic construction. The proof is a direct one-line application of the general nonzero cardinality result for F2Power at rank 3, followed by numerical simplification to 7.
Claim. The cardinality of the set of nonzero vectors in the three-dimensional vector space over the field with two elements equals 7, i.e., $|(Z/2Z)^3setminus{0}|=7$.
background
The module treats Q3 as the elementary abelian 2-group of rank 3, realized as maps from a three-element index set to the two-element set with pointwise XOR. This group supplies the seven nonzero vectors that stand in explicit bijection with the seven Booker plot families via the assignment table in the accompanying paper. The upstream nonzero cardinality theorem for F2Power at dimension 3 supplies the count 2^3-1, which the module doc describes as replacing an earlier hardcoded definition with a proved dependence on the algebra layer.
proof idea
The proof is a one-line wrapper that invokes the nonzero cardinality theorem for F2Power at rank 3. That upstream result reduces the filtered cardinality to 2^3-1 and applies a numerical normalization to obtain 7.
why it matters
The result supplies the exact count required for the bijection between Booker plot families and the nonzero elements of Q3, feeding directly into the equality theorem that equates the two cardinalities and into the master certificate for the narrative geodesic. It realizes the D=3 spatial dimension landmark of the forcing chain by exhibiting the 2^3-1 structure that the aesthetics module links to narrative forms. No open scaffolding remains on this count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.