cert
plain-language theorem explainer
Packages three elementary facts about domain cost into a single certificate for the J-cost symmetry module: cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is positive. Anyone citing the structural theorem that recognition cost is ratio-symmetric will pull this bundle. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_007 records the structural fact 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$.
Domain cost is the in-module specialization of that cost to a pair of positive reals (model and evidence scales). The certificate structure bundles three elementary properties of that specialization: vanishing when the two arguments coincide, nonnegativity on the positive orthant, and positivity of a fixed canonical threshold used as a comparison scale.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on $(0,\infty)$.
proof idea
One-line structure instance. The three fields of RSMTHStructural007Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new arithmetic is performed; the definition only packages those proofs into the certificate record.
why it matters
Gives a single named inhabitant of the structural certificate for module 7, so downstream consumers can depend on one object rather than three separate lemmas. The module itself is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and encodes the J-cost identity $J(x)=J(1/x)$, which is the ratio-symmetry half of the T5 uniqueness story for the cost functional. No used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer that witnesses non-emptiness of the certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.