countLawCert
plain-language theorem explainer
The declaration supplies an explicit inhabitant of the CountLawCert structure, certifying that any family satisfying the count law under an encoding into nonzero vectors of F2Power D has cardinality exactly 2^D - 1 and covers every nonzero vector. A researcher classifying gauge-boson families or Booker plots at D = 3 would cite this certificate to justify the universal 2^D - 1 count. The construction is a direct record that wires the cardinality implication, the surjectivity guarantee, the concrete Booker instance at D = 3, and the resulting 7-
Claim. Let CountLaw(D, Family, encoding) assert that encoding : Family → F2Power D is a bijection onto the nonzero vectors of the D-dimensional F2-vector space. The master certificate is the structure whose card_law field states that CountLaw(D, Family, encoding) implies |Family| = 2^D - 1, whose no_extra field states that every nonzero vector is attained, whose booker_instance field is the concrete CountLaw(3, BookerPlotFamily, plotEncoding), and whose booker_card_via_law field is the corollary |BookerPlotFamily| = 7.
background
The module establishes a reusable combinatorial principle: a CountLaw D Family encoding holds precisely when the encoding maps Family bijectively onto the 2^D - 1 nonzero elements of F2Power D. This unifies the seven Booker plot families at D = 3, the three opponent-color channels at D = 2, and the three massive gauge bosons at D = 2 after dimensional reduction. The upstream lemma bookerCountLaw shows that the Booker families satisfy CountLaw 3 via plotEncoding, with the three fields injective, nonzero image, and surjective_on_nonzero. The lemma countLaw_implies_card then extracts the cardinality equality from any such CountLaw instance, while countLaw_implies_no_extra restates the surjectivity on nonzero vectors.
proof idea
The definition constructs the certificate record by direct field assignment: card_law receives the theorem countLaw_implies_card, no_extra receives countLaw_implies_no_extra, booker_instance receives the theorem bookerCountLaw, and booker_card_via_law receives the corollary booker_count_via_law that normalizes 2^3 - 1 to 7. No tactics or reductions occur beyond the record construction itself.
why it matters
This supplies the top-level inhabited certificate for the 2^D - 1 counting principle that the module abstractly states. It closes the pattern for D = 3 classifications used in the Booker plot result and extends uniformly to D = 2 reductions that recover three opponent colors and three massive bosons. The construction directly supports the framework claim that D = 3 spatial dimensions arise from the eight-tick octave (T7-T8) by forcing the same nonzero-vector count that appears in the Recognition Composition Law derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.