nonzero_card_three
plain-language theorem explainer
The theorem establishes that the elementary abelian 2-group of rank 3 contains exactly seven nonzero vectors. Researchers modeling the seven Booker plot families cite this result to ground the bijection in Aesthetics.NarrativeGeodesic with a proved count rather than an assertion. The proof is a direct specialization of the general nonzero_card theorem at D=3 followed by arithmetic reduction via norm_num.
Claim. $|F_2^3setminus{0}|=7$, where $F_2^3$ is the set of functions from a 3-element index set to the two-element set equipped with pointwise XOR.
background
F2Power D is defined as the type Fin D → Bool with pointwise XOR serving as the abelian group operation, making it the elementary abelian 2-group of rank D. The sibling theorem nonzero_card states that the cardinality of the nonzero elements in F2Power D equals 2^D - 1 for any natural number D. This module is a theorem module with no internal axioms or sorrys; its MODULE_DOC states that the count 7 at D=3 is proved so downstream modules can chain off a real theorem instead of a hardcoded definition.
proof idea
The proof applies the general nonzero_card theorem instantiated at D=3. It then uses norm_num to establish that 2^3 - 1 equals 7 and rewrites the equality to obtain the desired statement.
why it matters
This corollary supplies the concrete count of seven for the nontrivial one-dimensional subgroups of Q_3 = F2Power 3. It is used directly by plotEncoding_image_eq_nonzero and Q3_nontrivial_subgroup_count in Aesthetics.NarrativeGeodesic, which in turn support the bijection with Booker plot families. The result closes the algebraic step asserted in the companion paper Seven_Plots_Three_Dimensions.tex and instantiates the D=3 case required by the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.