Chemistry Solvation Free Energy From Jcost

Solvation and the cost function

In physical chemistry, the solvation free energy is the change in Gibbs free energy when a solute is transferred from a vacuum into a solvent. The classic Born model describes the charging of a spherical ion of radius a and charge q in a solvent of dielectric constant ε: ΔG_solv = −q²/(8πε₀a)(1 − 1/ε). The factor (1 − 1/ε) measures how much the solvent screens the ion; for water at ε ≈ 80, that factor is about 0.9875, so the model predicts strong solvation.

In Recognition Science, a framework that derives physical structure from a forced cost of recognition events, the same screening factor is identified with the cost function J evaluated at the ratio ε/1. The cost function is defined as J(x) = (x + 1/x)/2 − 1. For water, J(80) ≈ 38.5, a large positive value that the research note associates with strong solvation. This identification is a research note, not a theorem; the library defines domainCost as J(m/e) without specifying what m and e are in chemical terms.

What the machine-checked library of formal theorems actually proves about domainCost is three general facts, none specific to chemistry. First, the cost vanishes when the two inputs are equal: for any nonzero r, domainCost r r = 0. Second, the cost is nonnegative for positive inputs: if m > 0 and e > 0, then 0 ≤ domainCost m e. Third, the constant phi − 3/2, called the canonical threshold, is positive; since phi is the golden ratio ≈ 1.618, this threshold is about 0.118. The library packages these three facts into a structure named SolvationFECert and proves that this structure is inhabited, meaning the certificate exists.

The library's own docstring states plainly: it proves nothing specific to the subject of solvation, because the definition of domainCost does not reference any chemical quantity. To make this library a theorem about solvation, one would need a definition of m and e in the subject's own terms, for example identifying m with the solvent's dielectric constant and e with the vacuum permittivity. Without that step, the three proved facts are universal properties of the cost function, not chemical predictions.

The practical consequence is a clear division of labor. The framework's forced cost function supplies a candidate measure of screening, and the formal library certifies that this measure has the right basic shape: zero when nothing differs, nonnegative when inputs are positive, and a positive threshold tied to the golden ratio. Whether that shape matches real solvation energies remains an empirical question, not a proved result.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

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

What this page does not claim

The library does not prove any specific solvation free energy value. The identification of the screening factor with J(ε) is a research note, not a theorem. No claim is made that the cost function matches measured solvation energies.

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/SolvationFreeEnergyFromJCost.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: