WeakCouplingCert
plain-language theorem explainer
WeakCouplingCert packages the RS-derived inverse fine-structure constant from the 44π seed and exponential gap correction, the geometric expression for sin²θ_W in terms of φ, the resulting definition of α_W as α divided by that angle, and the two inequalities establishing positivity and ordering. A model builder needing a zero-parameter value for the SU(2) coupling would cite this certificate. The structure is instantiated by reflexivity on the defining equations together with two positivity lemmas from the same module.
Claim. The certificate asserts that the inverse fine-structure constant satisfies $α^{-1} = α_{seed} exp(-f_{gap}/α_{seed})$, that the weak mixing angle is given by $sin²θ_W = (3-φ)/6$, that the weak coupling obeys $α_W = α / sin²θ_W$, and that $0 < α_W$ together with $α < α_W$, where $α$ is the fine-structure constant, $φ$ the golden ratio, and the seed and gap derive from the cube geometry.
background
The module derives the weak coupling α_W from two RS quantities. The inverse fine-structure constant α^{-1} is obtained from the geometric seed α_seed = 44π and the gap weight f_gap via the exponential resummation α^{-1} = α_seed exp(−f_gap / α_seed), as defined in Constants.Alpha. The weak mixing angle squared is fixed by the gauge embedding geometry at D = 3 as sin²θ_W = (3 − φ)/6, where φ is the golden ratio, coming from ElectroweakMasses. The tree-level relation α = α_W sin²θ_W then determines α_W = α / sin²θ_W. The structure collects these identities along with the positivity statements. The local setting is the Standard Model weak coupling derived from Q3 cube structure with zero free parameters.
proof idea
This is a structure definition whose fields are the asserted equalities and inequalities. The downstream theorem weak_coupling_cert populates the structure by reflexivity on the first three fields and by direct application of the lemmas alpha_W_pos and alpha_W_gt_alpha to the last two fields.
why it matters
The certificate is consumed by the theorem weak_coupling_cert, which constructs an instance of it. It completes the RS derivation of α_W from the eight-tick octave (T7) that produces the gap weight and the spatial dimension D=3 (T8) that fixes the embedding factor (3−φ)/6. The derivation traces to the Recognition Composition Law and the phi-ladder without adjustable parameters. It leaves open whether radiative corrections preserve the same geometric form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.