OpponentColorCountLaw
plain-language theorem explainer
OpponentColorCountLaw specializes the general count law to opponent color channels at D=2, asserting that the three channels (red-green, blue-yellow, luminance contrast) correspond exactly to the non-zero vectors in the rank-2 F2 space. Perceptual theorists or Recognition Science researchers modeling dimensional reduction from cone responses would reference this to justify the 2^2 -1 structure in color opponency. The definition reduces directly to the CountLaw predicate at dimension 2 via a one-line specialization.
Claim. Let $C$ be a finite type of opponent channels and $e: C → ℱ₂² an encoding. The opponent color count law holds precisely when $e$ is a bijection from $C$ onto the three non-zero elements of the rank-2 elementary abelian 2-group.
background
The module introduces the 2^D -1 count law as a reusable combinatorial principle for D-axis classifications. CountLaw D Family encoding asserts that the encoding map injects Family bijectively onto the non-zero vectors of F2Power D, the elementary abelian 2-group of rank D modeled as Fin D → Bool with pointwise XOR. This forces the cardinality of Family to equal 2^D -1. The local theoretical setting applies the principle at D=2 to opponent colors after reduction of the rod/cone substrate, paralleling the D=3 case for Booker plot families and the D=2 case for massive electroweak bosons (W, Z, H) with the photon as the zero element.
proof idea
The definition is a one-line wrapper that applies CountLaw at dimension 2 to the opponent channel type and its encoding.
why it matters
This declaration instantiates the counting principle of section XXVII for the D=2 opponent-color case, supplying the combinatorial basis for exactly three channels as 2^2 -1. It parallels the seven Booker families at D=3 and the three massive bosons at D=2, reinforcing the framework pattern that the same 2^D -1 structure appears across perceptual, gauge, and narrative classifications. The result supports dimensional reduction arguments consistent with the eight-tick octave and the derivation of D=3 spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.