alpha_W_pos
plain-language theorem explainer
The result establishes positivity of the weak coupling constant obtained by dividing the RS-derived electromagnetic fine-structure constant by the phi-based Weinberg angle squared. Researchers verifying electroweak relations in Recognition Science would reference it. The proof applies the division positivity lemma directly to the auxiliary positivity results for the fine-structure constant and the Weinberg angle squared.
Claim. $0 < α_W$ where $α_W = α / sin²θ_W$ and $sin²θ_W = (3 - φ)/6$, with $α$ the fine-structure constant from the EMAlphaCert chain.
background
The WeakCoupling module defines the weak coupling via the tree-level electroweak identity $α = α_W · sin²θ_W$. The angle factor $sin²θ_W_rs = (3 - φ)/6$ arises from the gauge embedding at spatial dimension D = 3. The electromagnetic $α$ is taken from the Constants.Alpha module as part of the zero-parameter EMAlphaCert derivation. Upstream, sin2_theta_positive proves $0 < sin²θ_W_rs$ by linarith after showing φ < 2 via goldenRatio_lt_two. alpha_pos_aux proves $0 < α$ by unfolding the seed expression and applying positivity.
proof idea
The term proof unfolds the definition of alpha_W and applies the div_pos lemma to alpha_pos_aux together with sin2_theta_positive.
why it matters
This positivity result supplies the alpha_W_positive field inside weak_coupling_cert, which certifies the full structural derivation of the weak coupling from Q3 cube geometry and the phi expression for the Weinberg angle. It confirms consistency with the D = 3 and phi-ladder elements of the forcing chain while keeping the module free of axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.