cert
plain-language theorem explainer
Packages three elementary facts about the module's domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the golden-ratio J-cost structural module uses this bundle as the inhabited witness. The body is a pure structure constructor wiring 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
This module records the structural claim that the Recognition Science J-cost attains its golden-ratio minimum $J(\varphi)=\varphi-3/2\approx 0.11803$. The J-cost is the unique nonnegative cost functional forced by the Recognition Composition Law; on the positive reals it is $J(x)=(x+x^{-1})/2-1$.
Here domainCost is the local cost pairing used by the module (a two-argument form built from that J-cost). The certificate structure demands three properties of that pairing and of a fixed positive scale canonicalThreshold: diagonal vanishing, nonnegativity on the positive quadrant, and a strictly positive threshold. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: "The cost of any recognition event is non-negative").
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs.
why it matters
Gives an inhabited, sorry-free witness that the structural hypotheses of RS Mathematics Module 2 hold. The module itself is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and sits under the J-uniqueness landmark (forcing chain T5): the cost minimum at the golden ratio $\varphi$ is the self-similar fixed point forced by T6. No downstream consumers are recorded yet; the certificate is the natural handle for any later theorem that needs the diagonal-vanishing / nonnegativity / positive-threshold package in one place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.