alpha_W_gt_alpha
plain-language theorem explainer
Recognition Science defines the weak coupling constant as the electromagnetic fine-structure constant divided by sin squared theta sub W, where the latter equals three minus phi over six. This theorem establishes that the weak coupling exceeds the fine-structure constant. Researchers in particle physics and Recognition Science cite the result to confirm the ordering of the couplings in the electroweak sector. The proof reduces the claim to an elementary inequality on the Weinberg parameter using a division rule and a bound less than one half.
Claim. $α < α_W$ where $α_W := α / sin²θ_W$ and $sin²θ_W := (3 - φ)/6$.
background
This declaration sits in the StandardModel.WeakCoupling module, which constructs the weak coupling constant from two RS-derived inputs: the fine-structure constant alpha from Constants.Alpha and the parameter sin2_theta_W_rs defined as (3 - phi)/6 in ElectroweakMasses. The module uses the tree-level identity alpha equals alpha_W times sin squared theta_W to obtain alpha_W as their quotient. Upstream lemmas establish that sin2_theta_W_rs is positive and strictly less than one half, enabling the strict inequality.
proof idea
The tactic proof first unfolds the definition of the weak coupling. It then rewrites the inequality alpha less than alpha_W using the lemma lt_div_iff_0 together with the positivity of sin2_theta_W_rs. The resulting claim alpha times sin2_theta_W_rs less than alpha is proved by applying mul_lt_mul_of_pos_left to the bound sin2_theta_W_rs less than one half, using the positivity of alpha. The final step identifies the right-hand side with alpha via the arithmetic lemma mul_one.
why it matters
The theorem supplies the ordering property alpha_W exceeds alpha that is required by the downstream weak_coupling_cert, which packages the full structural certificate for the weak sector. It thereby confirms a direct consequence of the tree-level relation once sin squared theta_W is shown less than one. The result aligns with the eight-tick octave and three-dimensional geometry of the Recognition Science framework but does not address renormalization group flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.