BioticInteract4Cert
plain-language theorem explainer
Certificate structure packaging three analytic properties of the ecological domain cost: vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Ecologists and RS foundation readers cite it as the interface that a concrete cost model must satisfy before biotic interaction types are read off. It is a pure structure definition; inhabitation is discharged elsewhere by the sibling `cert` bundle.
Claim. A certificate consists of three facts about the ecological domain cost $C$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for every nonzero real $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The Ecology module frames biotic interaction types (competition, mutualism, predation, amensalism, commensalism) as the five axes of the RS configuration dimension, so configDim $D=5$. The local cost model is a two-argument real function (domain cost) that scores a pair of positive recognition parameters; the diagonal condition says a self-matched pair carries zero cost, matching the J-cost minimum at identity.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via the standard J-cost nonnegativity lemma. The present structure lifts that spirit to the ecological domain cost and adds a positive threshold against which interaction regimes can be cut.
Sibling lemmas in the same file prove the three fields for the concrete domain-cost and threshold definitions; this declaration only names the Prop bundle those lemmas inhabit.
proof idea
No proof body: this is a structure definition whose three fields are propositions. Inhabitation is not claimed here. Downstream, the noncomputable definition cert fills the fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited wraps that instance as Nonempty.
why it matters
Gives the Ecology layer a single named interface for the cost-and-threshold hypotheses used when reading five biotic interaction types off configDim $D=5$. Downstream, cert builds a concrete inhabitant and cert_inhabited records nonemptiness, closing the structural theorem status of the module (0 sorry, 0 axiom). Ties the ecological story to the broader recognition-cost calculus (nonnegative J-type costs, identity at cost zero) without yet invoking the forcing chain T0–T8 or the mass ladder. It is scaffolding for ecology-as-configDim, not a derivation of the five named interaction labels from first principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.