cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single RS4 certificate for the strong-coupling foundation layer: diagonal vanishing, nonnegativity on positive masses/energies, and a positive canonical threshold. Anyone citing the structural alpha_s(M_Z)=J(phi) claim uses this witness. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero real $r$ against itself vanishes, $\mathrm{domainCost}(r,r)=0$; (ii) for positive mass and energy, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
This module is the RS Foundation session-3 layer. Its headline structural claim is $\alpha_s(M_Z)=J(\varphi)\approx 0.11803$ against the PDG value $0.1179$ (about $0.01\sigma$). The cost side of that story is the Recognition J-cost $J(x)=(x+x^{-1})/2-1$, forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law.
Here the local object is a domain cost on pairs of reals (mass/energy style arguments), not the raw event cost. The certificate structure AlphaStrRS4Cert records exactly three properties needed downstream: diagonal vanishing away from zero, nonnegativity when both arguments are positive, and positivity of a canonical threshold scale.
Upstream, ObserverForcing already has nonnegativity of recognition-event cost via $J$-cost nonnegativity on positive states. The present certificate lifts the analogous facts to the domain-cost interface used by the alpha-strong RS4 packaging.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No new algebra is performed; the definition is pure packaging.
why it matters
Gives a single named witness that the domain-cost interface is well-behaved for the RS4 strong-coupling foundation. The module status line treats the alpha_s match as a structural theorem (zero sorry, zero axiom) with RS_PASS confirmed; this certificate is the cost-side bundle that such a claim sits on.
It sits next to the T5 J-uniqueness landmark ($J(x)=\cosh(\log x)-1$) and the phi fixed-point story (T6), because the reported value is exactly $J(\varphi)$. No used-by edges are recorded yet, so the immediate consumer is the local foundation narrative and the sibling inhabitance fact rather than a named parent theorem outside the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.