sin2_pos
plain-language theorem explainer
The theorem asserts that the RS-derived weak mixing parameter satisfies sin²θ_W > 0. Researchers constructing the weak coupling α_W = α / sin²θ_W from first principles would cite it to guarantee that divisions remain defined and the resulting α_W stays positive. The proof is a direct term application of the positivity lemma already established in the ElectroweakMasses module.
Claim. $0 < (3 - φ)/6$, where φ is the golden ratio and the left-hand side is the RS weak mixing parameter sin²θ_W^{RS} obtained from the gauge embedding (D - φ)/(2D) at D = 3.
background
The module constructs the SU(2) weak coupling α_W from the RS fine-structure constant α and the independently derived sin²θ_W = (3 - φ)/6. The expression for sin²θ_W follows from the gauge embedding formula (D - φ)/(2D) evaluated at the three spatial dimensions fixed by the forcing chain. The upstream theorem sin2_theta_positive unfolds the definition and applies the inequality φ < 2 together with linear arithmetic to reach the same positivity claim.
proof idea
The proof is a one-line term wrapper that directly invokes the theorem sin2_theta_positive from the ElectroweakMasses module.
why it matters
The result supplies the positivity prerequisite needed to define α_W = α / sin²θ_W and to prove α_W > α inside the same module. It therefore sits inside the RS derivation of the tree-level electroweak identity that begins from the forcing sequence T0-T8 and the Recognition Composition Law. No open questions or scaffolding are touched by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.