zPolarizations
plain-language theorem explainer
zPolarizations assigns the integer 3 to the polarization count of the neutral weak boson. Electroweak model builders reference it when enumerating degrees of freedom after symmetry breaking. The assignment is a direct constant that encodes the standard count for a massive spin-1 particle.
Claim. The neutral weak vector boson $Z^0$ possesses three polarization states.
background
The module derives W and Z boson masses from the Higgs mechanism and weak mixing angle after electroweak symmetry breaking, which corresponds to the J-cost minimum on the phi-ladder. Upstream anchors include the definition of W as the wallpaper group count (17) that sets topological fractions in mass formulas, together with related W definitions in lepton and mass-topology modules. The local setting treats the Z boson as the massive neutral carrier whose mass satisfies m_Z = m_W / cos(theta_W).
proof idea
The definition is a direct constant assignment of 3. It encodes the standard result that a massive spin-1 particle possesses three polarization states in three spatial dimensions.
why it matters
This definition supplies the polarization count required for degree-of-freedom accounting in the electroweak sector. It is consistent with the forcing-chain result D = 3 and the eight-tick octave structure. The module places the electroweak scale on the phi-ladder and predicts m_Z near 91 GeV; the polarization datum closes the counting step for the Z boson.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.