bookerCountLaw
plain-language theorem explainer
The bookerCountLaw theorem certifies that the seven Booker plot families satisfy the CountLaw structure at D=3 under the plotEncoding map. Researchers working on narrative classification or the 2^D-1 counting principle for gauge families would cite this to obtain the cardinality result. The proof is a term-mode construction that directly supplies the three fields of CountLaw from the injectivity, nonzeroness, and surjectivity lemmas on plotEncoding.
Claim. Let $B$ be the type of Booker plot families and let $e : B → ℱ_2^3$ be the plot encoding map. Then $e$ is injective, $e(b) ≠ 0$ for every $b ∈ B$, and for every nonzero $v ∈ ℱ_2^3$ there exists $b ∈ B$ such that $e(b) = v$.
background
CountLaw D Family encoding is the proposition that the given encoding function realizes a bijection from Family onto the nonzero vectors of F2Power D. It bundles three conditions: the encoding is injective, its image avoids the zero vector, and it is surjective onto the nonzero vectors. The module abstracts the reusable 2^D-1 counting principle that yields seven elements at D=3, three opponent-color channels at D=2, and three massive gauge bosons at D=2. Upstream, BookerPlotFamily is the inductive type whose seven constructors are placed in explicit bijection with the nonzero vectors of F2Power 3 by plotEncoding; the supporting lemmas plotEncoding_injective, plotEncoding_image_nonzero, and no_eighth_plot establish the three required properties of that map.
proof idea
The proof is a term-mode construction of the CountLaw structure. It supplies the injective field from plotEncoding_injective, the nonzero field from plotEncoding_image_nonzero, and the surjective_on_nonzero field from no_eighth_plot.
why it matters
This supplies the concrete CountLaw instance for Booker plot families at D=3. It is invoked by booker_count_via_law to obtain Fintype.card BookerPlotFamily = 7 and by countLawCert to inhabit the master certificate. In the module it realizes the 2^D-1 count law for narrative structures, which the surrounding text shows also classifies opponent colors and gauge bosons at lower D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.