countLaw_implies_card
plain-language theorem explainer
If a finite family admits an encoding into the D-dimensional vector space over F2 that is injective, avoids the zero vector, and hits every nonzero vector, then the family has cardinality exactly 2^D - 1. Researchers classifying gauge bosons, opponent colors, or Booker plot families cite this to obtain the universal count 7 at D = 3 or 3 at D = 2. The proof equates the image of the encoding to the nonzero vectors via the law's surjectivity and injectivity fields, then applies the known cardinality of nonzero vectors in F2Power D.
Claim. Let $D$ be a natural number and let $F$ be a finite type. Suppose there exists a map $e : F → ℱ_2^D$ that is injective, satisfies $e(x) ≠ 0$ for all $x ∈ F$, and is surjective onto the nonzero vectors of $ℱ_2^D$. Then the cardinality of $F$ equals $2^D - 1$.
background
The module abstracts a reusable counting principle for D-axis classifications in Recognition Science. A CountLaw D Family encoding is a structure asserting that the encoding map is a bijection from Family onto the nonzero vectors of F2Power D, where F2Power D is the elementary abelian 2-group of rank D modeled as functions Fin D → Bool with pointwise XOR. The three fields of CountLaw are: injective (the map is one-to-one), nonzero (no family member maps to the zero vector), and surjective_on_nonzero (every nonzero vector is hit). Upstream, the theorem nonzero_card states that the number of nonzero vectors in F2Power D is exactly 2^D - 1.
proof idea
The tactic proof first builds an equality between the image of encoding and the Finset filter of nonzero vectors in F2Power D. It uses the nonzero field to show the image lies inside the filter and the surjective_on_nonzero field to show the converse. A second step applies Finset.card_image_of_injective using the injective field to equate the image cardinality with Fintype.card Family. The final rewrite invokes F2Power.nonzero_card to conclude the result.
why it matters
This is the universal corollary that converts any CountLaw instance into an explicit cardinality. It directly feeds booker_count_via_law (which normalizes to 7 at D = 3) and countLawCert (the master certificate bundling card_law, no_extra, and the Booker instance). The result supplies the combinatorial step underlying the 2^D - 1 pattern for Booker plots at D = 3, opponent-color channels at D = 2, and the three massive gauge bosons at D = 2, consistent with the framework's T8 forcing of three spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.