weinbergAngle
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.