Chemistry Complexation Constant From Jcost Complex Kcert

What the certificate proves

The declaration ComplexKCert is a formal certificate: a small package of three proved statements about the cost function J, which the framework defines as J(x) = (x + 1/x)/2 - 1. The three statements are: J(r/r) = 0 for any nonzero r; J(m/e) is nonnegative when m and e are positive; and the constant phi - 3/2 is positive. Each is a theorem in the machine-checked library of formal theorems, and each is proved from the definition of J alone.

What the certificate does not do is touch chemistry. The module defines a quantity domainCost as J(m/e), where m and e are real numbers, but it never says what m or e mean. The docstring mentions EDTA chelation and a hoped-for formula log K_f = J(phi)^(-1) × n_donors, but that paragraph is a research note, not a result. The certificate proves nothing about stability constants, donor numbers, or calcium ions.

In plain terms: the certificate establishes three general facts about a cost function, and it leaves the chemical application as an open target. The framework's own documentation says so explicitly: the module proves nothing specific to its subject, because the definition of domainCost does not reference one. A reader should take the certificate as a small, solid piece of the framework's foundation, not as a derivation of any measured stability constant.

theorem cert_inhabited : Nonempty ComplexKCert := ⟨cert⟩

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The certificate does not derive any measured stability constant. The certificate does not establish that J(phi)^(-1) × 6 equals any observed log K_f. The certificate does not prove that the golden ratio phi is the unique self-similar scaling.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/ComplexationConstantFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: