cert_inhabited
plain-language theorem explainer
The certificate type packing three structural properties of the RS domain cost (diagonal vanishing, nonnegativity, positive canonical threshold) is nonempty. Anyone citing the Foundation layer for the strong-coupling match alpha_s(M_Z)=J(phi) needs this existence fact. The proof is a one-line term that supplies the concrete witness cert.
Claim. There exists a certificate asserting that the domain cost vanishes whenever its two arguments are equal and nonzero, that the domain cost is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
In the RS Foundation module (session 3), the strong coupling is identified with the J-cost at the golden ratio: $\alpha_s(M_Z)=J(\varphi)\approx 0.11803$, matching PDG $0.1179$ at $0.01\sigma$ (RS_PASS confirmed). The module is marked a structural theorem with zero sorry and zero axioms.
The structure AlphaStrRS4Cert packages three elementary properties used in that identification: (i) domain cost vanishes on the diagonal for nonzero arguments, (ii) domain cost is nonnegative when both mass and energy arguments are positive, and (iii) the canonical threshold is strictly positive. Domain cost is the local cost comparison between mass and energy scales; the canonical threshold is the positive cutoff against which recognition events are scored.
proof idea
Term-mode one-liner. The goal is Nonempty AlphaStrRS4Cert. The proof applies the anonymous constructor of Nonempty to the already-constructed value cert, which is the concrete inhabitant of the three-field structure. No tactics, no further lemmas.
why it matters
Closes the existence obligation for the RS4 strong-coupling certificate in the Foundation layer. The module status line records this as a structural theorem supporting $\alpha_s(M_Z)=J(\varphi)$ against the PDG value. No downstream dependents appear in the current graph; the declaration is the inhabitedness lemma for the certificate bundle itself. It sits under the J-uniqueness landmark (T5), since the strong-coupling identification is $J(\varphi)$ with $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.