AlphaStrRS4Cert
plain-language theorem explainer
Certificate structure that packages three foundation facts used by the RS alpha_s claim: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone assembling or discharging the session-3 foundation witness cites it. Pure structure definition with no proof body; inhabitants are built by plugging in the three sibling lemmas.
Claim. A foundation certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module is RS Foundation session 3, a structural package with zero sorry and zero axioms. Its headline claim is $\alpha_s(M_Z)=J(\varphi)\approx 0.11803$ against the PDG value $0.1179$ (about $0.01\sigma$).
Domain cost is the real-valued cost assigned to a pair of positive scale parameters (measure and expectation style arguments). The first field demands that cost vanish when the two arguments coincide and are nonzero, i.e. the diagonal is a zero set of the cost. The second field is ordinary nonnegativity on the positive quadrant. The third field asserts that the module's canonical threshold constant is strictly positive, so it can serve as a genuine cutoff.
Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J$-cost nonnegativity at positive state. The present structure lifts that style of positivity into a single named certificate type for the alpha_s foundation layer.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Downstream, the definition cert inhabits the structure by assigning the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields. cert_inhabited is then the one-line Nonempty witness ⟨cert⟩.
why it matters
Gives a single named type for the cost-and-threshold package that the session-3 alpha_s structural theorem needs. Downstream cert and cert_inhabited exist only to produce and advertise an inhabitant of this type, so later foundation consumers can depend on one object rather than three separate lemmas.
In the broader Recognition chain this sits under the J-cost layer (T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$) and the forced self-similar scale $\varphi$ (T6). The module headline equates $\alpha_s(M_Z)$ with $J(\varphi)$, so the certificate's diagonal-zero and nonnegativity fields are the minimal cost axioms needed before that numerical identification is trustworthy. It does not itself compute the coupling; it only certifies the cost infrastructure the coupling claim rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.