countLaw_implies_no_extra
plain-language theorem explainer
Every encoding satisfying CountLaw for dimension D is surjective onto the nonzero vectors of F2Power D. Researchers classifying gauge families or narrative plots in Recognition Science cite it to confirm that a given family exhausts all nonzero binary vectors. The proof is a one-line wrapper that projects the surjectivity field of the CountLaw hypothesis.
Claim. If CountLaw holds for dimension $D$, family type $Family$, and encoding map $encoding : Family → F_2^D$, then for every nonzero vector $v ∈ F_2^D$ there exists $x ∈ Family$ such that $encoding(x) = v$.
background
CountLaw D Family encoding is a structure that certifies the encoding map is injective, lands only on nonzero elements of F2Power D, and covers every nonzero element. F2Power D is the elementary abelian 2-group of rank D, realized as Fin D → Bool under pointwise XOR. The module abstracts the reusable 2^D − 1 counting principle that classifies Booker's seven plots at D = 3, three opponent-color channels at D = 2, and three massive gauge bosons at D = 2.
proof idea
The proof is a one-line wrapper that applies the surjective_on_nonzero field of the CountLaw hypothesis directly to the given nonzero vector v.
why it matters
This supplies the no_extra field of countLawCert, the master certificate bundling cardinality, no-extra, and the Booker instance. It completes the universal no-eighth-member statement inside the 2^D − 1 counting law of the Recognition framework, supporting the D = 3 classification of seven plots and the D = 2 reduction to three massive bosons. It touches the open extension of the pattern to other physical families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.