pith. sign in
module module high

IndisputableMonolith.Masses.ElectroweakMasses

show as:
view Lean formalization →

This module assembles RS-derived electroweak quantities including the weak mixing angle and a narrow Z-boson mass interval. It supplies sin²θ_W = (3 - φ)/6 together with related mass expressions built from the phi-ladder. The structure imports anchor constants, verification machinery, and phi bounds to produce these parameter-free results.

claimThe module states $m_Z^{pred} = 91075.095$ MeV (interval (91075.09, 91075.10)) and defines $sin^2 θ_W = (3 - φ)/6$ along with $m_W$, $m_H$, and cosine relations derived from the golden ratio.

background

The module resides in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants, canonical mass constants from Anchor, and rigorous algebraic bounds on φ = (1 + √5)/2 from PhiBounds. Anchor centralises parameter-free constants described in the mass manuscripts. Verification supplies the comparison framework while keeping experimental values as imported constants, not RS derivations.

proof idea

This is a definition module with supporting lemmas. It establishes phi_eq_goldenRatio via PhiBounds, then applies interval arithmetic and algebraic identities to derive sin²θ_W, cos²θ_W, and the Z-mass interval from the anchor mass ladder.

why it matters in Recognition Science

The module feeds the WeakCoupling module, which combines sin²θ_W = (3 - φ)/6 with the RS fine-structure constant to obtain α_W. It supplies the electroweak mass predictions and Weinberg angle required for the Standard Model sector in the Recognition framework.

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)