Pith. sign in
module module high

IndisputableMonolith.Masses.ElectroweakMasses

show as:
view Lean formalization →

Electroweak mass and mixing inputs for Recognition Science: Weinberg angle from gauge geometry, experimental W/Z/H anchors, and a certified MeV-scale interval for the Z prediction on the phi-ladder. VEV, Fermi-constant, weak-coupling, and electroweak scorecard modules import these values. The file is mostly definitions plus elementary positivity and interval lemmas, not a deep forcing proof.

claimRS electroweak sector data: $\sin^2\theta_W=(3-\varphi)/6$, $\cos^2\theta_W=1-\sin^2\theta_W$, experimental anchors $m_W$, $m_Z$, $m_H$, and a predicted $Z$ mass in the open interval $(91075.09,\,91075.10)$ MeV on the $\varphi$-ladder (with $\varphi$ the golden ratio).

background

Recognition Science places particle masses on a $\varphi$-ladder (yardstick times $\varphi$ to a rung index, with sector gaps). The electroweak sector is treated here as a Model-layer package: geometric mixing angles and ladder predictions live beside imported PDG-style experimental numbers used only for comparison.

The Weinberg angle is not fitted. Downstream scorecards state $\sin^2\theta_W=(3-\varphi)/6$ from gauge-embedding geometry, with $\varphi=(1+\sqrt{5})/2$. Cosine forms follow by complement. Anchor and Verification imports supply the canonical mass-constant layout and the quarantined exp-vs-prediction comparison pattern; PhiBounds supplies rigorous algebraic bounds on $\varphi$.

Constants import the RS-native tick and related base units. Experimental $m_W$, $m_Z$, $m_H$ appear as named anchors; the $Z$ prediction interval in the module doc is the certified numerical claim this file exposes to importers.

proof idea

Definition-heavy module. Golden-ratio identification, $\sin^2\theta_W$ and $\cos^2\theta_W$ (and $\cos\theta_W$) are closed-form defs from $\varphi$; equality lemmas rewrite the cosine square as the geometric complement. Positivity and $\sin^2\theta_W<1/2$ are elementary inequalities on $(3-\varphi)/6$ using $\varphi$ bounds. Experimental masses are numeric constants. The $Z$ prediction is an interval statement certified against PhiBounds-style arithmetic, not a long tactic derivation of the rung formula itself.

why it matters in Recognition Science

This is the shared electroweak input surface for the mass and SM coupling stack. VEVConsistency uses $m_Z$ and the RS $\sin^2/\cos^2$ to prove the Higgs VEV is not independent: $v^2=m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$. FermiFromRSInputs continues that chain to $G_F=1/(\sqrt{2},v^2)$.

ElectroweakZeroParamScoreCard lists $\sin^2\theta_W=(3-\varphi)/6$ among the four SM electroweak parameters forced from the T5–T7 chain and geometry. WBosonAbsoluteScoreCard takes $m_Z$ on rung 51 and the same mixing angle toward a zero-parameter $W$ mass. WeakCoupling builds $\alpha_W$ from RS $\alpha$ and this module's $\sin^2\theta_W$. Without these defs, the zero-parameter electroweak scorecards have no common numeric spine.

scope and limits

used by (5)

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)