pith. machine review for the scientific record. sign in
def definition def or abbrev

OpponentColorCountLaw

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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. -/

depends on (14)

Lean names referenced from this declaration's body.