MassiveBosonCountLaw

formal source

 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 :
 183    ∀ {D : ℕ} {Family : Type} [Fintype Family]
 184      {encoding : Family → F2Power D},
 185      CountLaw D Family encoding →
 186        ∀ v : F2Power D, v ≠ 0 → ∃ x : Family, encoding x = v
 187  booker_instance :
 188    CountLaw 3 BookerPlotFamily plotEncoding
 189  booker_card_via_law :
 190    Fintype.card BookerPlotFamily = 7
 191