plot_count_scaling
plain-language theorem explainer
The number of nonzero vectors in the D-dimensional vector space over F2 equals 2^D minus 1. Researchers establishing the bijection between Booker's seven plot families and the nonzero elements of F2Power 3 cite this to fix the plot count at seven for dimension three. The proof is a direct one-line application of the general nonzero_card result from the F2Power algebra module.
Claim. For any natural number $D$, the cardinality of the set of nonzero vectors in the elementary abelian 2-group of rank $D$ (modeled as functions from Fin $D$ to Bool under pointwise XOR) equals $2^D - 1$.
background
F2Power D is defined as the type Fin D → Bool equipped with pointwise XOR, forming the elementary abelian 2-group of rank D. Its upstream nonzero_card theorem asserts that the filtered Finset of nonzero elements has cardinality exactly 2^D - 1, proved by subtracting the zero vector from the full Fintype.card. The NarrativeGeodesic module places this cardinality in the setting of the cube Q3 = (Z/2)^3, where it supplies the exact count of seven nonzero vectors that match Booker's plot families via the explicit encoding table in the module documentation.
proof idea
The proof is a one-line wrapper that applies the nonzero_card theorem from the F2Power module.
why it matters
This result supplies the general cardinality formula that confirms the seven-plot count for D=3, serving as Falsifier 2 of the paper in cardinality form. It underpins the bijection statements plotEncoding_image_eq_nonzero and booker_seven_eq_2_pow_3_minus_1 within the module. In the Recognition framework it aligns with the forcing of D=3 spatial dimensions (T8) and the structural closure of narrative geodesics on the 3-cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.