cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single certificate: vanishing on the diagonal, non-negativity for positive arguments, and positivity of the canonical threshold. Anyone citing the v3 J-cost monotonicity bundle uses this inhabitant. The body is a pure structure assembly of three already-proved 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
The module records structural properties of the Recognition Science cost $J$. As stated in the module header, $J$ is strictly convex on $(0,\infty)$, with $J'(x)=(1-x^{-2})/2$ changing sign at $x=1$ and $J''(x)=x^{-3}>0$, so $J$ has a unique minimum $J(1)=0$.
Domain cost is the two-argument cost used in the monotonicity session: it vanishes when the two arguments agree (off zero) and stays non-negative on the positive quadrant. The canonical threshold is a fixed positive scale against which cost comparisons are made.
Upstream, ObserverForcing.cost_nonneg already asserts that every recognition event has non-negative cost via $J\ge 0$ on positive states. The three field lemmas of this certificate specialize that non-negativity and the diagonal vanishing to the domain-cost interface.
proof idea
One-line structure inhabitant. The three fields of JCostMono3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work; the certificate is just the packaged triple.
why it matters
Gives a single named witness that the domain-cost interface used by the J-cost monotonicity v3 session is well-formed: zero on the identity, non-negative off it, and compared against a positive threshold. That matches the forcing-chain picture in which $J$ (T5 uniqueness, $J(x)=(x+x^{-1})/2-1$) is the unique admissible cost with minimum zero at the fixed point $x=1$.
No downstream consumers are wired yet in the graph, so this is a terminal packaging step inside the Foundation layer rather than a lemma on a longer proof path. It closes the certificate side of the structural theorem status claimed by the module (0 sorry, 0 axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.