IndisputableMonolith.Patterns.TwoToTheDMinusOne
Patterns.TwoToTheDMinusOne supplies the CountLaw predicate that certifies a bijection from a Family to the nonzero vectors of F_2^D. Researchers on structural aesthetics or the Recognition forcing chain cite it to justify the 2^D-1 count for Booker's plot families when D=3. The module imports F2Power and NarrativeGeodesic; the bijection property is established in its sibling lemmas.
claimA CountLaw for dimension $D$, family $F$, and encoding $e$ holds precisely when $e$ realizes a bijection $F$ to the set of nonzero vectors in the elementary abelian 2-group of rank $D$.
background
The module lives in the Patterns domain and imports F2Power together with NarrativeGeodesic. F2Power defines the elementary abelian 2-group of rank $D$ and proves that its nonzero elements number exactly $2^D-1$. NarrativeGeodesic develops the narrative geodesic on the cube $Q_3=(Z/2)^3$ as the Lean counterpart of the paper Seven_Plots_Three_Dimensions.tex, where Booker's seven plot families are asserted to arise from that punctured cube.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies CountLaw and its immediate consequences (countLaw_implies_card, CountLawCert) that certify the cardinality match required by NarrativeGeodesic. That construction in turn closes the structural argument of Seven_Plots_Three_Dimensions.tex, linking the T8 step D=3 of the forcing chain to the aesthetic count of seven via the 2^D-1 pattern.
scope and limits
- Does not construct explicit encodings for concrete families.
- Does not prove existence of any particular Family.
- Does not extend the CountLaw to groups other than F2Power D.
- Does not address dynamical interpretations of the encoding map.