cert
plain-language theorem explainer
Packages three proved facts about domain recognition cost into a single certificate: cost vanishes when the two arguments agree, cost is nonnegative for positive inputs, and the canonical threshold is positive. Anyone citing the J-cost ratio-symmetry structural theorem (module 7) uses this bundle. The definition is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
Module RS_PHY_Structural_007 records the structural fact that Recognition Science cost is ratio-symmetric: the J-cost satisfies $J(x)=J(1/x)$. In RS-native 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 real arguments (mass-like and energy-like scales). The certificate structure RSPHYStructural007Cert packages the three elementary properties needed downstream: vanishing on the diagonal, nonnegativity off the diagonal, and positivity of a fixed numerical threshold used as a comparison scale.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg): every recognition event has nonnegative cost because $J$ itself is nonnegative on the positive reals.
proof idea
One-line structure instance. 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 extra algebra is performed at this site.
why it matters
This certificate is the export surface of Structural Module 7: J-cost ratio symmetry $J(x)=J(1/x)$. That identity is the elementary reflection of T5 J-uniqueness (the forced cost $J(x)=\cosh(\log x)-1$) and of the Recognition Composition Law. Bundling the three properties lets later physics modules assume a single inhabited certificate rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity separately.
No downstream consumers are wired yet in the graph (used_by empty), and the sibling cert_inhabited is the natural next step that turns the definition into an inhabited Prop. The module itself is marked STRUCTURAL THEOREM with zero sorry and zero axioms, so this def closes the packaging layer rather than leaving an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.