cert
plain-language theorem explainer
Packages three verified properties of the ecological domain cost into a single certificate: diagonal vanishing, non-negativity on positive masses and energies, and a strictly positive canonical threshold. Ecologists or RS foundation readers cite it when treating biotic interaction costs as a recognition cost. The body is a pure structure assembly of three already-proved lemmas.
Claim. There is a certificate asserting that the ecological 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 Ecology module is a structural theorem (zero sorry, zero axiom) tying the five classical biotic interaction types (competition, mutualism, predation, amensalism, commensalism) to the five-axis configuration dimension of recognition space.
The certificate structure bundles three cost axioms for a domain cost $C:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$: vanishing on the nonzero diagonal, non-negativity for positive arguments, and positivity of a fixed canonical threshold. These mirror the global recognition cost $J$, which is nonnegative on every recognition event (ObserverForcing: "The cost of any recognition event is non-negative").
Sibling lemmas already establish the three fields for the ecological $C$ and the canonical threshold; this definition only packages them.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No new calculation occurs.
why it matters
Gives a single named witness that ecological domain cost behaves like a recognition cost, so the five biotic interaction types can sit inside the same cost calculus used elsewhere in the foundation. The module thesis is that those five types equal configDim $D=5$ in recognition space; the certificate is the cost-side handle for that claim. No downstream users are recorded yet; the natural consumer is any theorem that needs an inhabited biotic-interaction certificate (e.g. the sibling inhabitedness fact). It does not itself force $D=5$ or classify interaction signs; it only certifies the cost axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.