cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single RS 2026 State-3 certificate: cost vanishes on the diagonal, is nonnegative for positive mass/energy, and the canonical threshold is positive. Anyone citing the structural 2026 status snapshot uses this witness. The body is a pure structure assembly from three already-proved 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 $\tau$ obeys $\tau>0$.
background
The module freezes a 2026 "state of the art" structural certificate for Recognition Science: forcing chain T0–T8 complete, constants derived, zero sorries. The local object is a three-field structure whose fields are pure inequalities and identities on a real bivariate domain cost.
Domain cost is the cost assigned to a mass/energy pair in the recognition setting. It is built from the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique cost forced by the Recognition Composition Law. The diagonal identity $C(r,r)=0$ is the cost minimum at matched arguments; nonnegativity is the physical requirement that recognition events never carry negative cost (cf. the upstream event-level fact that every recognition event has nonnegative cost via $J\ge 0$). The canonical threshold is the positive cutoff used to separate sub-threshold from above-threshold recognition.
proof idea
One-line structure construction. Each field of the certificate is filled by a named sibling lemma already proved in the same module: diagonal vanishing by the domain-cost-at-equality lemma, nonnegativity by the domain-cost-nonnegativity lemma, and positivity of the threshold by the canonical-threshold-positivity lemma. No new arithmetic is performed.
why it matters
This is the concrete inhabitant of the RS 2026 State-3 certificate structure. The module presents it as part of the structural theorem snapshot (forcing chain T0–T8 complete, constants derived, zero code sorries). Downstream, the sibling inhabitedness fact can point at this value; no further used-by edges are recorded yet. It does not itself advance T5–T8 or the mass ladder; it only bundles the cost-side side conditions that any later 2026-status consumer can assume in one name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.