cert
plain-language theorem explainer
Packages three structural facts on domain cost (vanishes on equal nonzero arguments, nonnegativity for positive inputs, and a positive canonical threshold) into one certificate for the J-cost ratio-symmetry module. Anyone citing the structural theorem that recognition cost is ratio-symmetric would reference this bundle. The definition is a direct field-by-field assembly of three 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 $T$ obeys $T>0$.
background
This module records a structural fact of Recognition Science: the J-cost is ratio-symmetric, $J(x)=J(1/x)$. In RS-native units the cost functional is forced by the Recognition Composition Law and the uniqueness step T5 of the forcing chain, where $J(x)=(x+x^{-1})/2-1$.
The local domain cost is the concrete cost used on mass/energy-style pairs in the Standard Model structural layer. The certificate structure bundles three elementary properties of that cost: it vanishes on the diagonal (equal nonzero arguments), it is nonnegative on the positive quadrant, and a fixed positive threshold is available for comparisons.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: the cost of any recognition event is nonnegative, via nonnegativity of $J$ on positive reals. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that picture to the domain-cost interface used here.
proof idea
One-line structure instance. Each field of RSSTDStructural007Cert is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No extra algebra or case splits.
why it matters
This certificate is the packaged witness for Structural Module 7 of the Standard Model layer: J-cost symmetry $J(x)=J(1/x)$, status structural (zero sorry, zero axiom). It sits downstream of the forced J-uniqueness (T5) and the Recognition Composition Law, and makes the three elementary cost properties available as a single object for later SM structural arguments that need a ratio-symmetric, nonnegative cost with a positive comparison threshold.
No downstream consumers are wired yet in the graph, so the declaration is presently a self-contained structural export rather than an intermediate lemma in a longer proof chain. It closes the local certificate interface for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.