pith. sign in
module module high

IndisputableMonolith.Masses.ElectroweakMasses

show as:
view Lean formalization →

The ElectroweakMasses module supplies RS-derived electroweak quantities including the Z-boson mass interval (91075.09, 91075.10) MeV and sin²θ_W = (3 − φ)/6. Model builders constructing parameter-free extensions of the Standard Model cite these values. The module assembles definitions and interval assertions from the imported Anchor, Verification, and PhiBounds modules with no internal proofs.

claim$m_Z \in (91075.09, 91075.10)$ MeV and $\sin^2 \theta_W = (3 - \phi)/6$, together with companion definitions for $m_W$, $m_H$, and the golden-ratio identification of $\phi$.

background

This module belongs to the Masses domain and imports canonical mass constants from Anchor, which centralises parameter-free constants derived from the Recognition Science forcing chain with the note that everything lives in the Model layer and no proofs claim experimental agreement. It further imports experimental comparison machinery from Verification, where experimental values are imported constants not derived from RS, and rigorous algebraic bounds on $\phi = (1 + \sqrt{5})/2$ from PhiBounds. The local setting uses the phi-ladder mass formula together with the Recognition Composition Law to fix electroweak parameters.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies sin²θ_W = (3 − φ)/6 to the WeakCoupling module, which defines the SU(2) weak coupling constant α_W by combining two independently RS-derived quantities: α from Constants/Alpha.lean and sin²θ_W = (3 − φ)/6 from Masses/ElectroweakMasses.lean. It thereby fills the electroweak sector of the mass predictions and supports the T5–T8 steps of the forcing chain for particle masses.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (21)