alpha_W
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 in Recognition Science
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.
scope and limits
- Does not compute a numerical approximation of α_W.
- Does not incorporate higher-order radiative corrections.
- Does not derive the value of sin²θ_W from first principles within this module.
- Does not address the running of the coupling with energy scale.
formal statement (Lean)
44def alpha_W : ℝ := alpha / sin2_theta_W_rs
proof body
Definition body.
45
46/-- α_W expressed in terms of RS primitives:
47 α_W = (1/alphaInv) / ((3 − φ)/6) = 6 / (alphaInv · (3 − φ)) -/