sin2ThetaW
sin²(θ_W) is defined as one minus the square of the W to Z boson mass ratio. Electroweak modelers in the Recognition Science program cite this when converting the φ-derived mass ratio into the Weinberg angle. The definition is a one-line algebraic transcription of the standard relation cos θ_W = m_W / m_Z.
claim$sin^2(θ_W) := 1 - (m_W / m_Z)^2$
background
The module derives W and Z boson masses from the φ-structure of Recognition Science, with the observed ratio m_W / m_Z ≈ 0.8815 tied to the Weinberg angle by m_W / m_Z = cos θ_W. The sibling massRatio is defined as m_W / m_Z. Upstream GaugeBosonMassesFromRS supplies the explicit form 6 / (3 + phi); ThreeGenerations and NeutrinoMassHierarchy give related φ-scaled ratios for generations and neutrino splittings. The module doc states the target is to derive the ratio from φ-quantized gauge structure, yielding the numerical target sin²(θ_W) ≈ 0.223.
proof idea
One-line definition that applies the trigonometric identity sin²θ = 1 - cos²θ to the mass ratio.
why it matters in Recognition Science
This definition supplies the electroweak mixing parameter for the WZBosonRatioScoreCardCert structure and the row_sin2_from_WZ_masses theorem, which certify 0.22 < sin²(θ_W) < 0.23. It also feeds the couplingRatio that extracts tan θ_W ≈ 0.536. The declaration realizes the module's core insight on φ-constrained SU(2) × U(1) mixing and supports the paper proposition on electroweak parameters from RS.
scope and limits
- Does not derive the numerical value of the mass ratio.
- Does not include radiative corrections to the tree-level relation.
- Does not constrain the value of phi from other sectors.
- Does not address neutrino or generation mass hierarchies.
formal statement (Lean)
64noncomputable def sin2ThetaW : ℝ := 1 - massRatio^2
proof body
Definition body.
65
66/-- **THEOREM**: sin²(θ_W) ≈ 0.223. -/