alpha_em_Z
plain-language theorem explainer
The declaration supplies the accepted numerical value of the electromagnetic fine structure constant at the Z-boson mass scale. Researchers comparing Recognition Science φ-ladder predictions to electroweak data would cite this constant when anchoring running-coupling calculations. The definition consists of a direct numerical assignment with no further computation or lemmas.
Claim. The electromagnetic fine-structure constant evaluated at the Z-boson mass scale is given by $1/127.9$.
background
The QFT module derives running couplings from φ-ladder scaling, where distinct rungs label energy scales and J-cost optimization changes with rung. Electromagnetic coupling increases from its low-energy value near 1/137 to the supplied value at the Z mass near 91 GeV. Upstream, the integer map Z from Masses.Anchor assigns sector-dependent integers via the formula involving Q6 powers for leptons and quarks; the certified abbrev in AnchorPolicyCertified maps species directly to these integers for use in mass and coupling formulas.
proof idea
The definition is a direct constant assignment of the numerical value 1/127.9. No lemmas or tactics are applied; it functions as an input datum for later running-coupling expressions in the module.
why it matters
This supplies the reference electromagnetic coupling at the Z scale, enabling direct comparison of φ-ladder running against measured values inside the alpha band. It supports the module target of obtaining running couplings from φ-scaling and J-cost variation, consistent with T5 J-uniqueness and the eight-tick octave. It leaves open the precise mapping of the Z mass to a specific φ-rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.