booker_count_via_law
plain-language theorem explainer
The theorem establishes that Booker plot families number exactly seven by specializing the D-dimensional count law at D equals 3. Researchers in narrative theory or gauge boson taxonomy cite this for the explicit D=3 instance. The proof is a direct application of the general cardinality implication to the Booker count-law instance followed by numerical normalization.
Claim. Let $B$ denote the set of Booker plot families. Then the cardinality of $B$ equals 7.
background
The module defines CountLaw D Family encoding as the proposition that an encoding injects Family bijectively onto the non-zero vectors of F2Power D, the elementary abelian 2-group of rank D given by functions from Fin D to Bool under pointwise XOR. The lemma countLaw_implies_card states that any family satisfying CountLaw has cardinality exactly 2^D minus 1. BookerPlotFamily is the inductive type whose seven constructors (overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn, comedy and the remaining two) stand in explicit bijection with the seven non-zero elements of F2Power 3 via plotEncoding. This rests on the F2Power definition and the BookerPlotFamily inductive supplied by the aesthetics module.
proof idea
The proof applies countLaw_implies_card to bookerCountLaw, producing the equality Fintype.card BookerPlotFamily equals 2^3 minus 1, then uses norm_num to evaluate the right-hand side as 7 and closes the goal.
why it matters
This corollary populates the countLawCert certificate that bundles the general card law, the no-extra theorem, and the Booker instance. It realizes the reusable 2^D minus 1 counting principle at D equals 3, aligning with the eight-tick octave of period 2^3 and the forcing of three spatial dimensions. The same pattern classifies three opponent-color channels at D equals 2 and three massive gauge bosons, while the task of supplying explicit encodings for further domains remains open research.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.