booker_count_via_law
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not construct the explicit bijection from plots to F2Power vectors.
- Does not verify the count law for opponent-color channels or gauge families.
- Does not prove that seven families exhaust all possible narratives.
- Does not derive the count law from the Recognition Composition Law or phi forcing.
Lean usage
example : Fintype.card BookerPlotFamily = 7 := booker_count_via_lawformal statement (Lean)
130theorem booker_count_via_law :
131 Fintype.card BookerPlotFamily = 7 := by
proof body
Term-mode proof.
132 have h := countLaw_implies_card bookerCountLaw
133 -- h : Fintype.card BookerPlotFamily = 2 ^ 3 - 1
134 norm_num at h
135 exact h
136
137/-! ## §5. Cross-domain witness sketches
138
139The instances below are *one-line* templates: each picks a candidate
140encoding and asserts `CountLaw` if and only if the encoding meets
141the three predicates. They are stated as definitions of
142*hypothetical* count-laws: turning them into theorems requires
143filling in the explicit encoding for each domain (which is open
144research, not a Lean exercise).
145-/
146
147/-- The opponent-color count law at `D = 2`: red-green, blue-yellow,
148 and the residual luminance/saturation contrast form three
149 channels = `2 ^ 2 - 1`. The encoding is left abstract; any
150 bijection between the three opponent channels and
151 `F2Power 2 \ {0}` validates the law. -/