MassiveBosonCountLaw
plain-language theorem explainer
MassiveBosonCountLaw asserts that a finite type of three elements equipped with a map to the nonzero vectors of F2Power 2 satisfies the universal CountLaw at dimension 2. Electroweak model builders would cite it to classify W, Z, and H while assigning the photon to the zero vector. The definition is a direct one-line wrapper that instantiates CountLaw at D equals 2.
Claim. Let $M$ be a finite type. An encoding map $e : M → ℱ₂² satisfies the massive-boson count law when $e$ is a bijection onto the three nonzero vectors of ℱ₂².
background
The module abstracts the combinatorial pattern that any family in bijection with the nonzero vectors of F2Power D has cardinality exactly 2^D - 1. F2Power D is the elementary abelian 2-group of rank D, realized as functions Fin D → Bool under pointwise XOR. CountLaw D Family encoding is the Prop asserting that the encoding map injects Family onto precisely the nonzero elements of F2Power D. The module doc states this pattern unifies Booker plots at D=3, opponent-color channels at D=2, and the three massive electroweak bosons at D=2 with the photon as the zero-eigenvalue element.
proof idea
The definition is a one-line wrapper that applies CountLaw at dimension 2 to the supplied family and encoding.
why it matters
This declaration embeds the three massive electroweak bosons inside the Recognition Science 2^D - 1 counting framework at D=2. It contributes to the master certificate that unifies Booker plot families, color channels, and gauge bosons. The parent result is the general CountLaw from the same module, which rests on F2Power algebra. It touches the open question of explicit physical encodings for the boson families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.