cert
plain-language theorem explainer
Packages three elementary properties of the Lambda_QCD domain cost into a single certificate value: diagonal vanishing, non-negativity on positive masses and energies, and positivity of the canonical threshold. Anyone citing the RS structural Lambda_QCD construction uses this as the inhabited witness. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
The module develops a structural RS account of $\Lambda_{\mathrm{QCD}}$ (target scale near $210,\mathrm{MeV}$) built from the $J$-cost and the golden-ratio ladder. In RS-native units the sketch is $\Lambda_{\mathrm{QCD}}=J(\varphi),M_Z/\varphi^{D+3}$ (or related $\varphi$-power forms), treated as a structural identity rather than a fit.
The domain cost $C(m,e)$ is the local recognition cost comparing a mass-like scale $m$ to an energy-like scale $e$. The certificate structure demands three facts: $C$ vanishes on the diagonal away from zero, $C$ is non-negative for positive arguments, and a fixed positive threshold $T$ (the canonical threshold) sits above zero. Non-negativity of recognition cost is the same principle as the upstream observer-forcing fact that every recognition event has non-negative $J$-cost.
Sibling lemmas already prove the three fields; this definition only names the packed witness.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive $m,e$), and canonicalThreshold_pos (threshold positivity). No new algebra is performed; the definition is pure packaging into LambdaQCD_RS_v3Cert.
why it matters
Gives the inhabited certificate that the module status line advertises as a structural theorem (zero sorry, zero axiom) for the RS $\Lambda_{\mathrm{QCD}}$ construction. Downstream consumers that need a single value of type LambdaQCD_RS_v3Cert (for example the sibling inhabitedness fact) point here rather than re-proving the three cost axioms.
In the broader framework this sits under Foundation cost geometry: $J$-cost non-negativity, the $\varphi$-ladder mass/scale formulas, and the $D=3$ spatial forcing that enters the $\varphi^{D+\cdots}$ powers in the module sketch. It does not itself derive the MeV number; it only certifies the cost-side hypotheses the structural story assumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.