OpponentColorCountLaw
OpponentColorCountLaw asserts that an encoding of opponent channels into the rank-2 elementary abelian 2-group hits precisely the three nonzero vectors. Visual-perception models in Recognition Science cite this when reducing the three-cone substrate to opponent channels at D=2. The definition is a direct specialization of the general CountLaw at D=2.
claimLet $OpponentChannel$ be a finite type. An encoding $OpponentChannel → ℱ₂² satisfies the opponent-color count law when it injects $OpponentChannel$ bijectively onto the three nonzero elements of ℱ₂².
background
The module introduces the reusable 2^D−1 count law. CountLaw D Family encoding is the proposition that the map Family → F2Power D sends the family exactly onto the nonzero vectors of F2Power D (Fin D → Bool under pointwise XOR). For D=2 this gives exactly three targets. Upstream F2Power supplies the group structure; the shifted cost H from CostAlgebra is listed among dependencies but is not invoked in the definition itself.
proof idea
The definition is a one-line wrapper that applies CountLaw to the concrete parameters D=2 and the opponent-channel family.
why it matters in Recognition Science
It supplies the D=2 case required by the count-law module. The module doc links the same combinatorial fact to seven Booker plot families at D=3, three massive bosons at D=2, and three opponent-color channels after dimensional reduction. This instance therefore anchors the visual-perception application of the 2^D−1 pattern inside the Recognition framework.
scope and limits
- Does not construct or exhibit any concrete encoding of opponent channels.
- Does not derive the count from the Recognition Composition Law or the cost functional equation.
- Does not address existence or uniqueness of the three channels beyond the combinatorial count.
- Does not extend the law to D≠2 or to non-finite families.
formal statement (Lean)
152def OpponentColorCountLaw {OpponentChannel : Type} [Fintype OpponentChannel]
153 (encoding : OpponentChannel → F2Power 2) : Prop :=
proof body
Definition body.
154 CountLaw 2 OpponentChannel encoding
155
156/-- The massive-electroweak-boson count law at `D = 2`: W, Z, H form
157 three massive bosons = `2 ^ 2 - 1`. The photon is the trivial
158 (zero-eigenvalue) element. The encoding is left abstract; any
159 bijection between the three massive bosons and `F2Power 2 \ {0}`
160 validates the law. -/