alpha_W_gt_two_alpha
plain-language theorem explainer
Recognition Science derives the weak coupling α_W = α / sin²θ_W with sin²θ_W = (3 − φ)/6 from gauge embedding in three dimensions. This theorem shows α_W > 2α follows directly from sin²θ_W < 1/2. A physicist verifying the RS prediction for the weak sector would cite it to confirm the coupling hierarchy without free parameters. The proof unfolds the definition and reduces the inequality via the known bound on sin²θ_W together with positivity of α.
Claim. $2α < α_W$, where $α_W = α / sin²θ_W$ and $sin²θ_W = (3 - φ)/6 < 1/2$.
background
The module defines the SU(2) weak coupling α_W by combining two RS-derived quantities: the fine-structure constant α from Constants.Alpha and sin²θ_W = (3 − φ)/6 from ElectroweakMasses, via the tree-level identity α = α_W · sin²θ_W. Both inputs trace to Q₃ cube geometry and the golden ratio φ without free parameters. Upstream, tick supplies the fundamental RS time quantum τ₀ = 1, while f_gap encodes the gap weight from the eight-tick DFT-8 projection used in the α derivation.
proof idea
The tactic proof unfolds alpha_W, rewrites the target via lt_div_iff₀ using sin2_theta_positive, then applies a calc block. It bounds 2 * alpha * sin2_theta_W_rs strictly below 2 * alpha * (1/2) by mul_lt_mul_of_pos_left with sin2_lt_half and alpha_pos_aux, which rings to alpha and yields the strict inequality.
why it matters
The result completes the structural certificate that α_W is fully RS-derived from the EMAlphaCert chain (44π seed plus f_gap from the eight-tick octave) and the D = 3 gauge embedding. It feeds the WeakCouplingCert that certifies zero free parameters. The inequality reinforces the expected hierarchy α_W > α > 2α within the phi-ladder and T8 three-dimensional setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.