WeakCouplingCert
WeakCouplingCert packages the RS-derived weak coupling α_W by combining the fine-structure constant α with sin²θ_W = (3 − φ)/6. A physicist verifying electroweak unification parameters would cite it to confirm that α_W follows from Q₃ cube geometry and the eight-tick gap with zero free parameters. The structure definition assembles five fields that reference prior lemmas on α, the gap function, and positivity inequalities.
claimThe structure asserts that the inverse fine-structure constant satisfies $α^{-1} = α_{seed} exp(-f_{gap}/α_{seed})$, that $sin²θ_W = (3 - φ)/6$, that $α_W = α / sin²θ_W$, together with the inequalities $0 < α_W$ and $α < α_W$.
background
This module derives the SU(2) weak coupling constant α_W from Recognition Science first principles by combining two zero-parameter inputs: the fine-structure constant α from Constants.Alpha and sin²θ_W = (3 − φ)/6 from ElectroweakMasses. The tree-level identity α = α_W sin²θ_W then determines α_W. Upstream, alphaInv is defined as alpha_seed ⋅ exp(−f_gap / alpha_seed) with alpha_seed = 44π and f_gap the logarithmic gap weight from the DFT-8 projection; alpha is its reciprocal. The angle formula traces to the D = 3 gauge embedding (D − φ)/(2D).
proof idea
As a structure definition the construction is direct: each of the five fields is supplied by an already-established equality or lemma in sibling declarations. The alpha_from_cube and sin2_from_phi fields are definitional equalities; alpha_W_def is the division identity; positivity and ordering follow from the lemmas alpha_W_pos and alpha_W_gt_alpha.
why it matters in Recognition Science
WeakCouplingCert supplies the certified record used by the downstream theorem weak_coupling_cert, which builds an explicit instance via reflexivity on the equalities and the positivity lemmas. It closes the RS derivation of α_W from the EMAlphaCert chain (44π seed plus eight-tick gap) and the D = 3 geometry that also fixes sin²θ_W, confirming that the weak coupling emerges from the same Q₃ cube and golden-ratio fixed point that determine α.
scope and limits
- Does not include higher-order loop corrections or running of α_W.
- Does not derive the full electroweak Lagrangian or boson mass spectrum.
- Does not address neutrino mixing angles or CP phases.
- Does not perform numerical comparison with experimental data.
Lean usage
theorem weak_coupling_cert : WeakCouplingCert where alpha_from_cube := rfl sin2_from_phi := rfl alpha_W_def := rfl alpha_W_positive := alpha_W_pos alpha_W_exceeds_alpha := alpha_W_gt_alphaformal statement (Lean)
95structure WeakCouplingCert where
96 alpha_from_cube : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed))
97 sin2_from_phi : sin2_theta_W_rs = (3 - Constants.phi) / 6
98 alpha_W_def : alpha_W = alpha / sin2_theta_W_rs
99 alpha_W_positive : 0 < alpha_W
100 alpha_W_exceeds_alpha : alpha < alpha_W
101