IndisputableMonolith.Chemistry.ComplexationConstantFromJCost
Defines complexation equilibrium constants from the Recognition Science J-cost on concentration ratios, with a domain cost, a positive canonical threshold, and a certificate type ComplexKCert. RS chemists predicting binding affinities from the cost functional would cite it. The module is mostly definitions plus elementary nonnegativity and positivity lemmas over the imported Cost and Constants layers.
claimOn concentration (or activity) ratios $x>0$, the domain cost is built from the RS cost $J(x)=(x+x^{-1})/2-1$. A canonical positive threshold is fixed from that cost, and a complexation certificate packages the resulting equilibrium constant $K$ together with the cost identities that justify it.
background
Recognition Science measures mismatch by the unique cost $J$ forced in the T5 step of the unified forcing chain: $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The Cost import supplies that functional and its basic calculus; Constants supplies the RS-native units (including the tick $\tau_0$).
In a chemical complexation setting the natural dimensionless argument of $J$ is a concentration or activity ratio. The module introduces a domain cost on that ratio, records that the cost vanishes at equilibrium equality and is nonnegative, and fixes a canonical positive threshold against which binding is judged.
The certificate bundle ComplexKCert (with an inhabited instance) is the module's main packaging object: it ties a numerical complexation constant to the J-cost identities rather than to a fitted free parameter.
proof idea
Definition-first module, not a deep proof development. domainCost is introduced from J; domainCost_at_eq and domainCost_nonneg are short algebraic or order facts about J at $x=1$ and for $x>0$. canonicalThreshold and canonicalThreshold_pos fix and certify a positive cutoff. ComplexKCert, cert, and cert_inhabited assemble those pieces into an inhabited certificate type. No multi-step forcing argument lives here; the work is wiring Cost/Constants into a chemistry-facing API.
why it matters in Recognition Science
Gives chemistry a direct bridge from the RS cost functional to complexation constants, so binding $K$ is read off J-cost structure instead of being an external Arrhenius or mass-action fit. Downstream used-by edges are empty in the current graph, so this is a leaf API module for later affinity, speciation, or ladder-mass chemistry results rather than a step inside T0-T8.
It sits in the Chemistry domain beside the phi-ladder mass formula and the same J that obeys the Recognition Composition Law. Anyone deriving equilibrium constants, coordination thresholds, or certified numerical $K$ values inside the monolith is expected to consume ComplexKCert rather than re-derive domain cost inequalities.
scope and limits
- Does not derive a numerical experimental $K$ for a named ligand or metal.
- Does not prove uniqueness of $J$; that is upstream in the forcing chain (T5).
- Does not treat kinetics, activation barriers, or temperature dependence beyond the static cost.
- Does not connect complexation $K$ to the phi-ladder mass formula or to $\alpha$.
- Does not supply solvent, ionic-strength, or activity-coefficient models.