cert
plain-language theorem explainer
Packages three structural facts about domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive measure and evidence, and the canonical threshold is strictly positive. Anyone citing the golden-ratio J-cost minimum (J(φ)=φ−3/2) can point here for the packaged hypotheses. The body is a pure structure constructor wiring three already-proved lemmas.
Claim. There is a certificate asserting: (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; (iii) the canonical threshold is strictly positive.
background
This module records structural facts about the Recognition Science J-cost near the golden ratio. The classical cost is $J(x)=(x+x^{-1})/2-1$, forced unique by the Recognition Composition Law; its self-similar fixed point is $\phi$, with $J(\phi)=\phi-3/2\approx 0.11803$.
Domain cost is the two-argument cost used when a measure $m$ is compared to evidence $e$. The certificate structure demands three properties: vanishing when $m=e\neq 0$, nonnegativity for positive arguments, and a strictly positive canonical threshold that separates the identity minimum from nontrivial recognition events.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on the positive reals.
proof idea
One-line structure constructor. The three fields of RSFDNStructural002Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive measure and evidence), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site.
why it matters
Gives a single named inhabitant of the structural certificate for Module 2 of the foundation layer: the golden-ratio recognition-cost package. Downstream consumers can assume the three properties at once rather than re-importing the three lemmas. It sits under the STRUCTURAL THEOREM status of the module (zero sorry, zero axiom) and supports the T5/T6 story that $J$ is unique and $\phi$ is the forced self-similar fixed point where the cost minimum lives. No used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.