weinbergAngle
The definition sets the Weinberg angle θ_W to the arccosine of the W/Z boson mass ratio obtained from Recognition Science's φ-structure. Electroweak physicists mapping RS predictions to Standard Model observables would cite it when converting the mass ratio into the mixing angle. It is implemented as a one-line definition that applies the inverse cosine directly to the sibling massRatio value.
claimDefine the Weinberg angle by $θ_W := arccos(m_W / m_Z)$, where the ratio follows from the φ-quantized electroweak gauge structure.
background
The StandardModel.WZMassRatio module derives the W/Z mass ratio from Recognition Science's φ-structure, where the observed masses satisfy m_W / m_Z ≈ 0.881 and equal cos(θ_W) by the standard electroweak relation. The local massRatio is defined as m_W / m_Z, while the upstream GaugeBosonMassesFromRS.massRatio supplies the explicit form 6 / (3 + phi). Other upstream massRatio definitions handle generational hierarchies and neutrino splittings but are not used here.
proof idea
This is a one-line definition that applies the real arccosine function directly to the massRatio value supplied by the sibling definition in the same module.
why it matters in Recognition Science
It supplies θ_W for the sibling sin²θ_W computation and completes the module's target of deriving electroweak parameters from RS. The module doc frames it as part of the PRL proposition linking φ-constrained gauge mixing to the observed Weinberg angle, closing the path from the T6 phi fixed point to measurable SM quantities.
scope and limits
- Does not derive the mass ratio value from first principles.
- Does not include radiative corrections to the tree-level relation.
- Does not address the full set of electroweak precision observables.
formal statement (Lean)
61noncomputable def weinbergAngle : ℝ := Real.arccos massRatio
proof body
Definition body.
62
63/-- sin²(θ_W) - the key electroweak parameter. -/