cert
plain-language theorem explainer
Packages three elementary facts about the domain recognition cost into a single certificate: zero cost on the diagonal, nonnegativity off the diagonal, and a strictly positive canonical threshold. Anyone citing the structural J-cost symmetry module (ratio symmetry J(x)=J(1/x)) uses this bundle as the inhabited witness. The definition is a pure structure constructor that wires three already-proved sibling lemmas.
Claim. There exists a certificate recording that (i) the domain recognition cost vanishes on equal positive arguments, $\mathrm{cost}(r,r)=0$ for $r\neq 0$; (ii) $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; and (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_007 records the structural theorem that Recognition Science cost is ratio-symmetric: the J-cost satisfies $J(x)=J(1/x)$. In RS units the cost functional is the unique continuous solution of the Recognition Composition Law forced at T5, namely $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), which is nonnegative and vanishes only at $x=1$.
The domain cost here is the two-argument lift of that J-cost to a measured value $m$ and an expected value $e$. The certificate structure simply packages the three elementary properties needed downstream: diagonal vanishing, nonnegativity, and a positive decision threshold. Upstream, ObserverForcing already proves that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states.
proof idea
One-line structure constructor. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional reasoning occurs inside the definition.
why it matters
Gives an inhabited, zero-sorry certificate that the structural cost facts of module 7 are available as a single object. The parent module status line marks this as a STRUCTURAL THEOREM (0 sorry, 0 axiom) supporting J-cost ratio symmetry $J(x)=J(1/x)$, which is the elementary reflection identity implied by T5 J-uniqueness. Downstream consumers that need a bundled witness of diagonal vanishing, nonnegativity, and a positive threshold can take this certificate rather than re-proving the three facts. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.