alpha_W
plain-language theorem explainer
The definition supplies the weak coupling α_W by dividing the RS-derived electromagnetic fine-structure constant α by the gauge mixing factor sin²θ_W = (3 − φ)/6. Researchers modeling electroweak interactions or beta functions in the Standard Model would reference this when requiring a zero-parameter expression for the SU(2) coupling strength. The construction is a direct abbreviation that invokes the tree-level identity α = α_W sin²θ_W together with the independently derived inputs.
Claim. $α_W = α / sin²θ_W$ where $α$ is the fine-structure constant from the exponential resummation of the structural seed and $sin²θ_W = (3 - φ)/6$ is fixed by three-dimensional cube geometry.
background
In Recognition Science the electromagnetic fine-structure constant α is obtained from the inverse alphaInv = alpha_seed * exp(−f_gap / alpha_seed), with α = 1/alphaInv. The weak mixing angle squared is fixed by the three-dimensional cube geometry as sin²θ_W = (3 − φ)/6. This module assembles the tree-level electroweak relation α = α_W sin²θ_W to produce α_W without additional parameters. Upstream results include the definition of alpha in Constants.Alpha and the structural derivation of sin²θ_W in ElectroweakMasses.
proof idea
The declaration is a one-line definition that applies the division alpha / sin2_theta_W_rs, where sin2_theta_W_rs is the RS value (3 − φ)/6. No tactics are required; the body is the direct abbreviation.
why it matters
This definition supplies the input for the WeakCouplingCert structure, which records that α_W is fully determined by the Q₃ cube geometry and the eight-tick forcing chain. It is referenced by the running-coupling module in QFT and by the positivity and comparison theorems alpha_W_pos, alpha_W_gt_alpha within the same file. The construction closes the parameter-free derivation of the weak coupling from the Recognition Composition Law and the D = 3 spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.