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