CountLaw
plain-language theorem explainer
CountLaw D Family encoding asserts that a map from a finite family to the nonzero vectors of F2Power D forms a bijection. Researchers classifying patterns in Recognition Science cite it to recover cardinalities such as seven at D=3 for Booker plots or three at D=2 for massive bosons. The structure is introduced by directly bundling the three required properties on the encoding map.
Claim. Let $D$ be a natural number, let $F$ be a type equipped with a Fintype instance, and let $e : F → ℝ₂^D$ be a function. The predicate CountLaw$(D, F, e)$ holds precisely when $e$ is injective, $e(x) ≠ 0$ for every $x ∈ F$, and every nonzero vector in ℝ₂^D lies in the image of $e$.
background
F2Power D is the elementary abelian 2-group of rank D, realized as the set of functions Fin D → Bool with pointwise XOR; this supplies the D-dimensional vector space over GF(2) whose nonzero elements number exactly 2^D - 1. The module Patterns.TwoToTheDMinusOne introduces CountLaw as a reusable combinatorial principle that abstracts D-axis classifications, covering the seven Booker plot families at D=3, three opponent-color channels at D=2, and three massive electroweak bosons at D=2. The construction rests on the upstream definition of F2Power and directly enables the cardinality corollary countLaw_implies_card.
proof idea
CountLaw is introduced as a structure whose three fields are exactly the required conditions: injectivity of the encoding, nonzeroness of every image, and surjectivity onto the nonzero vectors of F2Power D. No lemmas are invoked and no tactics are executed; the definition itself assembles the bundled proposition.
why it matters
CountLaw supplies the foundational pattern that unifies the recurring 2^D -1 count throughout Recognition Science, feeding directly into bookerCountLaw (which instantiates it for the seven plots) and CountLawCert (the master certificate). It aligns with the forcing chain at T7 (eight-tick octave) and T8 (D=3) by explaining why 2^3 -1 =7 appears in multiple physical families. It leaves open the construction of explicit encodings for further families such as those arising in nucleosynthesis tiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.