sin2_lt_half
plain-language theorem explainer
The theorem establishes that the RS-derived weak mixing parameter satisfies sin²θ_W < 1/2. Workers on electroweak couplings cite it to obtain α_W > 2α from the tree-level relation α = α_W sin²θ_W. The proof is a direct one-line reference to the upstream inequality already shown in the electroweak masses module.
Claim. $sin^2 θ_W^{RS} < 1/2$
background
The WeakCoupling module obtains α_W from the identity α = α_W sin²θ_W, taking sin²θ_W = (3 - φ)/6 from the electroweak masses module. Here φ is the golden ratio fixed point of the Recognition Science forcing chain, and the expression follows from the gauge embedding (D - φ)/(2D) at D = 3. The upstream definition sin2_theta_W_rs records this quantity explicitly, while the companion theorem sin2_theta_lt_half proves the bound by unfolding the definition and applying linear arithmetic with the positivity of φ.
proof idea
The proof is a one-line term wrapper that directly applies the upstream theorem sin2_theta_lt_half from ElectroweakMasses. No further unfolding or tactics occur at this site.
why it matters
The result is invoked by the downstream theorem alpha_W_gt_two_alpha to conclude α_W > 2α. It supplies the comparison between weak and electromagnetic couplings required by the RS derivation of α_W, consistent with the mild mixing from the D = 3 embedding. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.