alpha_W
plain-language theorem explainer
The weak coupling constant is fixed at 1/30 in RS-native units. Electroweak model builders matching to the Fermi constant would cite this value when anchoring tree-level parameters. It is supplied by direct numerical assignment with no reduction steps or lemmas.
Claim. The weak coupling constant satisfies $α_W = 1/30$.
background
Recognition Science treats running couplings as consequences of φ-ladder scaling: each rung sets an energy scale at which J-cost optimization determines the effective coupling. The module QFT.RunningCouplings derives these from the φ-ladder, with α_W tied to the weak sector and Fermi constant. Upstream, scale(k) := φ^k supplies the ladder rungs, while the for structure encodes orbit coherence axioms needed for self-reference consistency. The beta definitions supply inverse-temperature and PPN contexts that frame the renormalization-group flow.
proof idea
One-line definition that directly assigns the constant 1/30. No tactics or upstream lemmas are invoked; the body is a literal real number.
why it matters
This supplies the numerical anchor for α_W in the StandardModel.WeakCoupling module, enabling the theorems alpha_W_pos, alpha_W_gt_alpha, alpha_W_gt_two_alpha and the WeakCouplingCert structure. The cert records that α_W traces to the 44π seed plus f_gap from the eight-tick octave and to sin²θ_W = (3 − φ)/6 from gauge embedding. It therefore closes the QFT-011 target for φ-derived running couplings at the weak scale, even though the present definition is scale-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.