cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single RS Physics Module 1 certificate: diagonal vanishing, nonnegativity for positive arguments, and a strictly positive canonical threshold. Anyone citing the QCD running-coupling structural theorem (alpha_s(M_Z) = J(phi)) uses this record as the local cost interface. Construction is a pure structure instance that wires three already-proved sibling lemmas.
Claim. There is a certificate record whose fields assert: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 1 targets the QCD running coupling at the Z pole: the Recognition claim is $\alpha_s(M_Z)=J(\varphi)\approx 0.11803$, matching PDG $0.1180$, and is marked STRUCTURAL THEOREM (zero sorry, zero axiom).
The local cost interface is the structure RSPhysics001Cert. Its three fields are pure real-analysis statements about domainCost (the module's cost functional on pairs of positive reals) and canonicalThreshold (a fixed positive scale used as a comparison level). Upstream, nonnegativity of recognition cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The present certificate specializes that idea to the module's domain cost and adds the diagonal-zero and threshold-positivity clauses.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work or algebraic reduction occurs inside the definition.
why it matters
Gives the module a single named inhabitant of the cost-certificate interface so downstream physics statements can assume diagonal vanishing, cost nonnegativity, and a positive threshold without re-proving them. The module doc ties this interface to the QCD claim $\alpha_s(M_Z)=J(\varphi)$, which sits on the T5 $J$-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$) and the golden fixed point $\varphi$ from T6. No used_by edges are recorded yet; the certificate is the local packing step that later alpha-band or running-coupling lemmas are expected to consume. It does not itself compute the numerical match to PDG.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.