cos2_theta_positive
plain-language theorem explainer
The RS Weinberg angle satisfies cos² θ_W > 0, which keeps the derived W boson mass positive and real. Electroweak mass calculations in the phi-ladder framework rely on this to maintain the gauge hierarchy m_W = m_Z cos θ_W. The proof is a one-line algebraic reduction that unfolds the cosine definition and applies linear arithmetic to the established sin² θ_W < 1/2 bound.
Claim. $0 < 1 - ((3 - φ)/6)$, where φ denotes the golden ratio fixed point and the expression for sin² θ_W follows from the Recognition Composition Law.
background
The module derives electroweak boson masses from the phi-ladder. The Z boson sits at rung 1 in the Electroweak sector, so m_Z = 2 φ^51 / 10^6 MeV. The W mass follows from the gauge relation m_W = m_Z cos θ_W, with the RS-native prediction sin² θ_W = (3 - φ)/6. cos2_theta_W_rs is defined directly as 1 - sin2_theta_W_rs. The upstream lemma sin2_theta_lt_half establishes sin2_theta_W_rs < 1/2 by unfolding the definition and invoking phi_pos together with linear arithmetic.
proof idea
One-line wrapper that unfolds cos2_theta_W_rs to 1 - sin2_theta_W_rs and invokes linarith on the sin2_theta_lt_half lemma.
why it matters
This inequality closes the basic positivity requirement for the Weinberg angle inside the electroweak mass formulas. It supports the downstream Z-boson mass prediction and the overall gauge-boson hierarchy in the Recognition Science chain (T5 J-uniqueness and T6 phi fixed point). The result is consistent with the eight-tick octave and the alpha band constraints but does not itself derive the sin² value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.