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

zPolarizations

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 242def zPolarizations : ℕ := 3

proof body

Definition body.

 243
 244/-- The W⁺ and W⁻ together have 6 polarization states. -/

depends on (4)

Lean names referenced from this declaration's body.