cert
plain-language theorem explainer
Packages three structural facts about the domain cost and the canonical threshold into one certificate record for RS structural module 10. Anyone citing the E_coh calibration layer (parameter-free predictions after the electron-mass fix) would reference this bundle. The definition is a direct structure instance wiring three already-proved component lemmas.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 10 is the RS structural calibration layer: the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free. The local certificate type collects three real-analytic properties of a domain cost $C$ and a canonical threshold $T_*$.
The domain cost is the module's real-valued cost on pairs of positive scales (mass/energy-like arguments). Its diagonal vanishing and nonnegativity mirror the global J-cost facts from the recognition layer: upstream, cost_nonneg states that the cost of any recognition event is nonnegative, via nonnegativity of $J$. The canonical threshold is the module's fixed positive cutoff used in structural comparisons.
The certificate structure simply names the three propositions that must hold for the calibration story to be well-posed on $\mathbb{R}$.
proof idea
Direct structure instance, not a tactic proof. The three fields are filled by the sibling lemmas already in the module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the cutoff by canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the structural certificate for module 10, so downstream developments can assume the cost/threshold package as one object rather than three loose lemmas. The module status line marks this layer as a structural theorem block (zero sorry, zero axiom), aligned with the RS claim that after $E_{\mathrm{coh}}$ is set by the electron mass, the remaining predictions carry no free parameters.
No used_by edges are recorded yet; the immediate consumer in-module is the inhabitedness wrapper for the same certificate type. In the broader forcing chain this sits downstream of J-cost nonnegativity (T5-adjacent cost structure) and upstream of any numerical calibration that quotes a positive threshold and a nonnegative domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.