cert
plain-language theorem explainer
Packages a three-field certificate that the domain cost vanishes on equal positive scales, stays nonnegative off-diagonal, and that the canonical threshold is strictly positive. Anyone citing the RS structural claim that the strong coupling at the Z scale is the J-cost of phi would point here. The definition is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate consisting of: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats running couplings on the phi-ladder as a structural consequence of the Recognition J-cost. The headline physics claim is that the strong coupling at the Z mass equals $J(\varphi)$, giving $\alpha_s(M_Z)\approx 0.118$ against the experimental $0.1179$.
Domain cost is the local cost functional on a pair of positive scales (mass and energy, or two renormalization points). The certificate structure demands three elementary properties: vanishing on the diagonal (equal scales cost nothing extra), nonnegativity for positive arguments, and a strictly positive canonical threshold that marks when running is allowed to start.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on the positive reals. The present certificate lifts that fact into the coupling-running setting.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs inside the definition.
why it matters
This is the inhabited certificate object for the structural theorem that running couplings arise from J-cost on the phi-ladder. The module status is zero sorry and zero axiom; the certificate is the concrete witness that the three algebraic side-conditions hold.
In the broader RS chain it sits under the J-uniqueness landmark (T5): once $J(x)=(x+x^{-1})/2-1$ is forced, evaluating at $\varphi$ yields the canonical strong-coupling value. No downstream consumers are wired yet in the graph, so the certificate currently closes the local module rather than feeding a larger theorem. It does not itself compute the numerical match $\alpha_s(M_Z)=J(\varphi)$; that comparison lives in the module narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.