def
definition
def or abbrev
MassiveBosonCountLaw
show as:
view Lean formalization →
formal statement (Lean)
161def MassiveBosonCountLaw {MassiveBoson : Type} [Fintype MassiveBoson]
162 (encoding : MassiveBoson → F2Power 2) : Prop :=
proof body
Definition body.
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). -/