cert
plain-language theorem explainer
Packages three elementary properties of the chemistry-domain cost into a single certificate for metal–ligand complexation constants derived from J-cost. Anyone citing the structural EDTA/Ca²⁺ stability story in this module uses this bundle. The definition is a pure structure inhabitant: it wires the diagonal-vanishing, non-negativity, and positive-threshold lemmas already proved in-module.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero ratio against itself is zero, $C(r,r)=0$ for $r\neq 0$; (ii) for positive metal and ligand scales $m,e>0$ one has $C(m,e)\ge 0$; (iii) the canonical complexation threshold is strictly positive.
background
The module treats metal–ligand stability constants as recognition costs. In Recognition Science the elementary cost is the J-functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law. Domain cost here is the chemistry specialization of that J-cost to metal and ligand scale parameters.
A complexation certificate is the triple of structural facts needed before one may speak of a formation constant: the cost vanishes on matched scales (identity event), never goes negative for positive scales, and the threshold that converts cost into a dimensionless $\log K_f$ is positive. The module’s motivating check is EDTA–Ca²⁺ chelation ($n_{\mathrm{donors}}=6$), where $\log K_f\approx J(\varphi)^{-1}\times 6$ lands in the observed order of magnitude (~18–21).
Upstream, non-negativity of recognition cost is already available from ObserverForcing: every recognition event has $0\le e.\mathrm{cost}$ via $J$-cost non-negativity on positive states.
proof idea
One-line structure inhabitant. The three fields of ComplexKCert are filled by the three already-proved in-module lemmas: diagonal vanishing of domain cost, non-negativity of domain cost on positive arguments, and positivity of the canonical threshold. No further calculation occurs; the definition only packages those facts.
why it matters
Gives the module a single named witness that the J-cost specialization used for complexation constants is a legitimate cost (zero on the identity, non-negative, positive threshold). That is the structural prerequisite for the Plan-v7 claim that metal–ligand $\log K_f$ is proportional to inverse J at $\varphi$ times donor count. The module status line marks the whole development as a structural theorem (zero sorry, zero axiom); this certificate is the concrete object that status refers to.
No downstream consumers are recorded yet, so the certificate presently closes the local chemistry interface rather than feeding a larger theorem. It sits downstream of the T5 J-uniqueness / RCL cost layer and of the global cost-nonnegativity fact, and upstream of any future numerical comparison of predicted versus measured formation constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.