CountLawCert
plain-language theorem explainer
The CountLawCert structure packages the universal counting law asserting that any family bijective with the non-zero vectors of F2Power D has cardinality exactly 2^D - 1, together with the explicit BookerPlotFamily instance at D = 3. Researchers classifying narrative plots or electroweak bosons would cite it to justify the 7-element count. It is assembled as a structure definition that directly bundles the general card and surjectivity corollaries with the concrete Booker data.
Claim. Let $D$ be a natural number, let Family be a finite type, and let encoding : Family → F₂^D be a map. If CountLaw(D, Family, encoding) holds then |Family| = 2^D − 1 and the image of encoding is exactly the set of non-zero vectors in F₂^D. In particular CountLaw(3, BookerPlotFamily, plotEncoding) holds and |BookerPlotFamily| = 7.
background
CountLaw D Family encoding is the Prop that encodes a bijection: the map is injective, lands only on non-zero elements of F2Power D, and hits every non-zero element. F2Power D is the elementary abelian 2-group of rank D, realized as Fin D → Bool with pointwise XOR. The module abstracts the reusable 2^D − 1 counting principle that appears across D-axis classifications in Recognition Science.
proof idea
The declaration is a structure definition with four fields. card_law and no_extra are the direct corollaries of the CountLaw structure. booker_instance is the explicit CountLaw 3 BookerPlotFamily plotEncoding instance supplied by the upstream bookerCountLaw. booker_card_via_law is the resulting cardinality equality obtained by applying countLaw_implies_card to that instance.
why it matters
CountLawCert supplies the master certificate that countLawCert (the downstream definition) inhabits. It unifies the seven Booker plots at D = 3 with the three opponent-color channels and three massive bosons at D = 2, furnishing the combinatorial substrate for the eight-tick octave (T7) and the emergence of D = 3. The construction closes the counting step in the Patterns module without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.