cert
plain-language theorem explainer
Packages three structural facts about the domain cost and the canonical threshold into one certificate for RS Physics Structural Module 10. Anyone citing the module's parameter-free calibration would point at this bundle. The definition is a pure field-wiring of three already-proved sibling lemmas into the certificate structure.
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 a structural physics certificate in Recognition Science: $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free. The local certificate type records three algebraic properties of a real-valued domain cost $C$ and a positive threshold used as a cutoff.
The domain cost is the module's specialization of the RS cost functional (the $J$-cost family forced by the Recognition Composition Law). Upstream, recognition-event cost is already known to be nonnegative: any recognition event $e$ satisfies $0\le e.\mathrm{cost}$ via nonnegativity of $J$. The certificate lifts that spirit to the two-argument domain cost on positive reals, plus a diagonal-vanishing identity and a positive threshold.
Sibling lemmas supply each field: equality of cost at equal positive arguments, nonnegativity for positive mass/energy-style inputs, and positivity of the canonical threshold.
proof idea
Not a proof: a structure inhabitant. Each field of RSPHYStructural010Cert is filled by the matching sibling lemma: diagonal vanishing by the domain-cost-at-equality lemma, nonnegativity by the domain-cost nonnegativity lemma, and threshold positivity by the canonical-threshold positivity lemma. No extra tactics or algebraic work.
why it matters
Gives Module 10 a single named certificate object that the rest of the physics layer can treat as the structural package for domain-cost calibration. The module claims status STRUCTURAL THEOREM (0 sorry, 0 axiom); this definition is the concrete inhabitant that makes that claim checkable as a bundled Prop triple rather than three loose lemmas.
In the broader RS chain, nonnegative cost and a positive threshold sit under the $J$-uniqueness forcing (T5) and the self-similar scale $\varphi$ (T6): cost minima and cutoffs must be pinned before mass-ladder or coupling predictions are read off. No downstream consumers are recorded yet; the immediate sibling is the inhabitedness wrapper that exposes this certificate as a default instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.