OpponentColorCountLaw

formal source

 149    channels = `2 ^ 2 - 1`. The encoding is left abstract; any
 150    bijection between the three opponent channels and
 151    `F2Power 2 \ {0}` validates the law. -/
 152def OpponentColorCountLaw {OpponentChannel : Type} [Fintype OpponentChannel]
 153    (encoding : OpponentChannel → F2Power 2) : Prop :=
 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. -/
 161def MassiveBosonCountLaw {MassiveBoson : Type} [Fintype MassiveBoson]
 162    (encoding : MassiveBoson → F2Power 2) : Prop :=
 163  CountLaw 2 MassiveBoson encoding
 164
 165/-! ## §6. Master certificate -/
 166
 167/-- **TWO-TO-THE-D-MINUS-ONE COUNT LAW MASTER CERTIFICATE.**
 168
 169    The Booker plot families instantiate the universal `CountLaw 3`
 170    pattern, with `Fintype.card BookerPlotFamily = 2 ^ 3 - 1 = 7`.
 171    The same pattern applies at any dimension: a family in bijection
 172    with the non-zero vectors of `F2Power D` has cardinality exactly
 173    `2 ^ D - 1`. This unifies the seven Booker plots, the three
 174    opponent-color channels (at `D = 2`), and the three massive
 175    electroweak bosons (at `D = 2` in the broken-phase basis with γ
 176    as the zero-eigenvalue element). -/
 177structure CountLawCert where
 178  card_law :
 179    ∀ {D : ℕ} {Family : Type} [Fintype Family]
 180      {encoding : Family → F2Power D},
 181      CountLaw D Family encoding → Fintype.card Family = 2 ^ D - 1
 182  no_extra :