IndisputableMonolith.Patterns.TwoToTheDMinusOne
This module defines CountLaw, a certification that a Family is in bijection with the non-zero vectors of F_2^D via an encoding map. Researchers working on structural enumerations in three-dimensional aesthetics or particle classifications would cite it to inherit a verified count of 2^D - 1. The argument imports the algebraic structure of F2Power together with the narrative geodesic on the 3-cube and establishes the bijection through cardinality and uniqueness lemmas.
claimLet $D$ be a natural number and let Family be a type equipped with an encoding map. A CountLaw $D$ Family encoding is a proof that encoding realizes a bijection between Family and the set of nonzero vectors in the $D$-dimensional vector space over the field with two elements.
background
The module Patterns.TwoToTheDMinusOne resides in the Patterns domain and imports F2Power, which defines the elementary abelian 2-group of rank D whose underlying set has cardinality 2^D and whose nonzero elements therefore number exactly 2^D - 1. It further imports NarrativeGeodesic, the Lean development of the structural closure of Booker's seven plot families on the cube Q_3 = (Z/2)^3, serving as the formal counterpart to the paper Seven_Plots_Three_Dimensions.tex.
proof idea
This is a definition module that introduces the CountLaw predicate and then proves the auxiliary results countLaw_implies_card and countLaw_implies_no_extra. The proofs apply the cardinality theorem already established inside F2Power together with direct injectivity and surjectivity arguments drawn from the NarrativeGeodesic construction on the 3-cube.
why it matters in Recognition Science
The module supplies the formal bridge between the algebraic count 2^D - 1 and the concrete families appearing in the Recognition Science framework, directly supporting the claim in Seven_Plots_Three_Dimensions.tex that Booker's seven plots arise from the nonzero vectors of (Z/2)^3. It feeds the sibling theorems that certify counts for opponent colors and massive bosons. By discharging the count via F2Power it replaces an assertion in the companion paper with a verified theorem.
scope and limits
- Does not construct explicit encodings for arbitrary families.
- Does not address dimensions beyond those for which F2Power is defined.
- Does not prove uniqueness of CountLaw beyond the stated bijection property.
- Does not connect the count to physical constants or the phi-ladder.