nonzero_card
The theorem states that the elementary abelian 2-group of rank D has exactly 2^D - 1 nonzero vectors. Researchers deriving the count of Booker plot families or generalizing plot scaling in narrative geodesics cite this to ground the D=3 case of seven families in a proved algebraic identity rather than an assertion. The tactic proof first rewrites the filtered set as the full universe with zero erased, applies the erase cardinality lemma, then substitutes the total cardinality from the companion card_eq result.
claimThe cardinality of the set of nonzero vectors in the elementary abelian 2-group of rank $D$ is $2^D - 1$.
background
F2Power D is the type Fin D → Bool equipped with pointwise XOR, forming the elementary abelian 2-group of rank D. The module proves it carries an AddCommGroup instance and a Fintype instance whose cardinality is given by the upstream card_eq theorem: Fintype.card (F2Power D) = 2^D, obtained by unfolding to the product of D copies of Bool.
proof idea
The proof introduces an auxiliary equality that rewrites the filtered set as Finset.univ.erase 0, applies Finset.card_erase_of_mem using that 0 lies in the universe, then rewrites the resulting expression with card_eq to reach 2^D - 1.
why it matters in Recognition Science
This result supplies the general cardinality that downstream modules rely on, including booker_seven_eq_2_pow_3_minus_1 in Aesthetics.NarrativeGeodesic (which equates the number of Booker plot families to 2^3 - 1) and plot_count_scaling (which states the same identity for arbitrary D). It discharges the combinatorial count asserted in the companion paper Seven_Plots_Three_Dimensions.tex, replacing a hardcoded 7 with a derivation from D = 3. In the Recognition framework the identity supports the structural count at the eight-tick octave (period 2^3) and the emergence of three spatial dimensions.
scope and limits
- Does not prove any group homomorphism or subgroup lattice beyond the raw count of nonzero elements.
- Does not establish the bijection between nonzero vectors and Booker plot families.
- Does not extend the count to other base fields or infinite-dimensional analogues.
- Does not derive physical constants, forcing-chain steps, or mass formulas.
Lean usage
theorem plot_count_scaling (D : ℕ) : (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 := F2Power.nonzero_cardformal statement (Lean)
126theorem nonzero_card :
127 (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 := by
proof body
Tactic-mode proof.
128 have h : (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card =
129 Fintype.card (F2Power D) - 1 := by
130 rw [show (Finset.univ.filter (fun v : F2Power D => v ≠ 0)) =
131 Finset.univ.erase 0 from ?_, Finset.card_erase_of_mem (Finset.mem_univ _)]
132 · rfl
133 · ext v
134 simp [Finset.mem_filter, Finset.mem_erase, Finset.mem_univ]
135 rw [h, card_eq]
136
137/-- At `D = 3`, the non-zero count is `7`. The seven Booker plot
138 families bijection in `Aesthetics.NarrativeGeodesic` chains off
139 this corollary. -/