weak_coupling_cert
plain-language theorem explainer
The declaration certifies that the weak coupling α_W is obtained directly from the RS-derived fine-structure constant α and the Weinberg angle sin²θ_W = (3-φ)/6 without introducing free parameters. A researcher modeling electroweak interactions from first principles would reference this to anchor α_W in the Recognition Science cube geometry. The proof constructs the certificate structure by reflexivity on the defining relations and direct appeal to the positivity and ordering lemmas for α_W.
Claim. The RS-derived weak coupling satisfies $α_W = α / sin²θ_W$ where $sin²θ_W = (3-φ)/6$, with $α_W > 0$ and $α_W > α$, and $α$ obtained from the exponential form $α^{-1} = α_{seed} exp(-f_{gap}/α_{seed})$.
background
In the StandardModel.WeakCoupling module the weak coupling α_W is defined via the tree-level relation α = α_W · sin²θ_W. Here α is the fine-structure constant taken from the EMAlphaCert chain (44π seed plus f_gap from the eight-tick octave) while sin²θ_W = (3-φ)/6 is taken from the gauge-embedding geometry at D=3. The WeakCouplingCert structure packages these inputs together with the derived positivity and ordering statements.
proof idea
The proof is a term-mode structure constructor for WeakCouplingCert. It supplies reflexivity for the three definitional equalities (alpha_from_cube, sin2_from_phi, alpha_W_def) and inserts the lemmas alpha_W_pos and alpha_W_gt_alpha for the positivity and ordering fields.
why it matters
This theorem completes the zero-parameter RS derivation of α_W inside the Standard Model sector, confirming that both α and sin²θ_W trace to Q₃ cube geometry and the golden ratio φ. It directly supports the framework claim that all electroweak parameters arise from the eight-tick octave and D=3 without external constants. The certificate closes the structural derivation of the weak coupling and is available for any downstream construction that needs an RS-native α_W.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.