ComplexKCert
plain-language theorem explainer
Certificate structure packaging three structural facts needed to read metal–ligand stability constants off Recognition Science J-cost: diagonal vanishing of the domain cost, non-negativity for positive arguments, and a strictly positive canonical threshold. Chemists or RS auditors of the EDTA/Ca²⁺ log K_f sketch cite it as the interface. Pure definitional packaging; inhabited downstream by the concrete cert bundle.
Claim. A complexation-constant certificate is a triple of facts about the 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 module derives metal–ligand formation constants from the Recognition Science cost functional $J$. In RS-native units the sketch is $\log K_f = J(\varphi)^{-1}\times n_{\mathrm{donors}}$; for hexadentate EDTA ($n=6$) this is order-of-magnitude consistent with the classical $\log K_f\approx 18$ for Ca²⁺.
Domain cost $C(m,e)$ is the local J-cost evaluated on a metal/environment (or metal/ligand) pair of positive reals. The canonical threshold $\tau$ is the positive cutoff against which that cost is compared when deciding whether a complexation channel is open. Upstream, non-negativity of recognition cost is already forced: every recognition event has $0\le e.\mathrm{cost}$, via $J$-cost non-negativity on positive states.
The certificate simply freezes the three inequalities the chemistry layer needs, without committing to a closed-form $K_f$ theorem yet.
proof idea
No proof body: this is a structure declaration. The three fields are bare propositions (diagonal vanishing of domain cost, non-negativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the chemistry layer a named, checkable interface for “J-cost is a legitimate complexation potential.” Downstream, cert assembles a concrete inhabitant and cert_inhabited records Nonempty ComplexKCert, closing the structural side of the module (status: 0 sorry, 0 axiom).
In the broader RS chain this sits under T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law: once $J$ is forced, domain cost inherits non-negativity and a unique minimum on the diagonal, which is exactly what the certificate demands. It does not yet pin the numerical EDTA band; it only licenses the cost-to-$K_f$ reading used in the module doc’s order-of-magnitude check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.