alpha_W
plain-language theorem explainer
The definition sets the weak coupling α_W equal to the fine-structure constant α divided by sin²θ_W = (3 − φ)/6. Researchers deriving electroweak parameters from Q₃ geometry inside Recognition Science cite this when linking the EM sector to the SU(2) coupling. The construction is a direct algebraic quotient that inherits positivity and ordering from its two RS-derived inputs.
Claim. $α_W := α / sin²θ_W$ where $α$ is the fine-structure constant obtained from the 44π seed and gap resummation, and $sin²θ_W = (3 − φ)/6$ is the value fixed by the gauge embedding at three spatial dimensions.
background
In Recognition Science the fine-structure constant is defined by α = 1/alphaInv with alphaInv = alpha_seed ⋅ exp(−f_gap / alpha_seed). The weak mixing angle is supplied by sin²θ_W_rs = (3 − φ)/6, which follows from the gauge embedding (D − φ)/(2D) evaluated at D = 3. The present definition combines these two quantities via the tree-level electroweak identity α = α_W ⋅ sin²θ_W.
proof idea
The declaration is a direct definition performing the quotient alpha / sin2_theta_W_rs. No lemmas are invoked; the body is the division itself.
why it matters
This definition supplies the RS-native weak coupling referenced by WeakCouplingCert and by the expanded form alpha_W_expanded. It completes the zero-parameter derivation of α_W from the EMAlphaCert chain and the phi-forced gauge angle, placing the weak coupling on the same footing as α. The construction uses the D = 3 dimension and the golden-ratio fixed point φ that appear in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.