alpha_em_low
plain-language theorem explainer
The declaration supplies the low-energy electromagnetic fine-structure constant as the fixed numerical value 1/137.036. A physicist comparing coupling evolution across scales or checking unification bounds would cite this constant as the infrared reference. The definition is a direct numerical assignment with no computation or lemmas.
Claim. $α_{em}(low) = 1/137.036$
background
The module derives running couplings from φ-ladder scaling, where each rung corresponds to a distinct energy scale and J-cost optimization changes with rung. Low-energy α_em is the infrared starting point that increases toward 1/127 at the Z mass, while α_s decreases due to asymptotic freedom. Upstream, the anchor Z maps lepton and quark sectors to integers via the formula Z(sector, Q) = (6Q)^2 + (6Q)^4 plus sector offsets, supplying the integer charges used in mass and coupling anchors.
proof idea
The definition is a direct numerical assignment with no lemmas or tactics applied.
why it matters
This supplies the infrared anchor for the downstream theorem alpha_gut_intermediate, which proves α_s_Z > α_GUT > α_em_low by direct comparison after unfolding. It instantiates the low-energy end of the RS running-coupling picture in which φ-ladder rungs set the scale dependence and the observed 1/137 value lies inside the predicted band. The definition leaves open the derivation of the exact digit string from the J-cost functional or RCL alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.