EMAlphaCert
plain-language theorem explainer
Unit certificate packaging four structural facts of the assembled EM inverse fine-structure expression: seed equals 44π, gap weight is forced from the eight-tick weight and ln φ, the exponential φ-dressing assembly holds by definition, and the numeric value lies in (137.030, 137.039). Downstream logic-real constant recovery cites the verified range. Discharge is simp plus ring on the seed identity, definitional rfl on the assembly, and the AlphaBounds inequalities.
Claim. An EM alpha certificate is a unit record whose verification asserts four facts simultaneously: the geometric seed equals $44\pi$; the gap term equals $w_8\ln\varphi$ with $w_8$ the eight-tick spectral weight; the inverse fine-structure expression equals $\alpha_{\mathrm{seed}}\,\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$; and that assembled value lies in the open interval $(137.030,\,137.039)$. Every certificate instance satisfies the predicate.
background
This module certifies the value of the assembled EM coupling expression, not a derivation of the measured infrared constant $\alpha^{-1}(0)=137.035999$. The four conjuncts are: seed identification $\alpha_{\mathrm{seed}}=4\pi\cdot 11=44\pi$ (ledger spherical-closure baseline over 11-edge paths), forced gap $f_{\mathrm{gap}}=w_8\ln\varphi$ with zero $\alpha$-input, canonical exponential dressing $\alpha^{-1}=\alpha_{\mathrm{seed}}\exp(-f_{\mathrm{gap}}/\alpha_{\mathrm{seed}})$, and the numeric band $(137.030,137.039)$.
Upstream, alphaInv is defined exactly as that exponential assembly, and alpha_seed is the geometric seed $4\pi\cdot 11$. The module doc is explicit that the seed is an identification, not a forced coupling: cycle-rank photon DOF is 5, not 11; genuine cube J-cost is $\pi^2$ rather than $4\pi\cdot 11$; and first-order scale identification is excluded by measurement. Exact IR $\alpha^{-1}(0)$ remains an open boundary condition.
proof idea
The structure itself is empty (unit certificate). The content is the simp-normal predicate verified (four conjuncts) and the theorem that every instance satisfies it.
Unfold verified. The seed identity is alpha_seed = 4*π*11, rewritten as $44\pi$ by ring. The gap and assembly conjuncts are definitional (rfl against f_gap and alphaInv). The range splits into the two AlphaBounds facts alphaInv_gt and alphaInv_lt, which place the assembled real in $(137.030,137.039)$.
why it matters
Feeds alphaInvL_bounds in Foundation.LogicRealConstants, which lifts the verified real interval into the logic-real embedding: the recovered inverse lies strictly between the logic-reals of 137.030 and 137.039, by projecting the fourth conjunct of verified_any.
In the Recognition framework this sits on the alpha band cited in the primer (construction inside $(137.030,137.039)$). The exponential dressing and $w_8$ are forced with zero $\alpha$-input; what is not forced is the seed $44\pi$ as a derived coupling, nor equality to CODATA. The honest-status audit records five closed negative routes: exact infrared $\alpha^{-1}(0)$ is an irreducible boundary condition of the present hierarchy, not a theorem. The certificate therefore pins construction value and range without overclaiming a CODATA derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.