alpha_pos_aux
plain-language theorem explainer
The auxiliary lemma establishes positivity of the fine-structure constant α derived from the RS geometric seed. It is invoked by the three main theorems in WeakCoupling that bound the weak coupling α_W from below. The proof is a one-line term-mode reduction that unfolds α through alphaInv and alpha_seed then applies the positivity tactic.
Claim. $0 < α$, where $α = 1/α_{inv}$ is the electromagnetic fine-structure constant obtained from the RS seed $α_{seed} = 4π·11$ via the resummation $α_{inv} = α_{seed}·exp(−f_{gap}/α_{seed})$.
background
The WeakCoupling module constructs the SU(2) coupling α_W from the tree-level identity α = α_W · sin²θ_W. Here α is imported from Constants.Alpha as the reciprocal of the exponential resummation of the geometric seed, while sin²θ_W = (3 − φ)/6 is taken from the D = 3 gauge embedding in ElectroweakMasses. The module doc states that both inputs are zero-parameter derivations from Q₃ cube geometry, with α coming from the EMAlphaCert chain (44π · exp(−f_gap/44π)). Upstream, alpha is documented simply as the fine-structure constant (α_EM) and alpha_seed as the baseline spherical closure cost over 11-edge interaction paths.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definitions of alpha, alphaInv, and alpha_seed, reducing the goal to an expression whose positivity follows directly from the positive seed 4π·11 and the exponential factor. The positivity tactic then closes the resulting real-number inequality.
why it matters
The lemma supplies the positivity fact required by alpha_W_pos, alpha_W_gt_alpha, and alpha_W_gt_two_alpha, thereby anchoring the tree-level electroweak relation to the independently derived α from the EMAlphaCert pipeline. It supports the module claim that α_W is fully RS-derived and satisfies the expected inequalities α_W > α > 0. Within the Recognition framework it connects the T5 J-uniqueness and T8 D = 3 landmarks to the weak sector without introducing new parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.