Certified enclosures of the CO2 uptake per unit alkalinity in seawater equilibrium chemistry (a model computation; the value ~0.8 is long known)

For seawater in equilibrium with a fixed fugacity of CO2, adding one mole of alkalinity raises dissolved inorganic carbon by η = ∂DIC/∂TA moles. We compute interval-arithmetic enclosures of η over the box T in [0,30] °C, S in [30,38], fCO2 in [280,560] µatm, TA = (S/35)·TA35 with TA35 in [2200,2400] µmol/kg, in a carbonate–borate–water model on the total pH scale with constants as printed in the Dickson–Sabine–Christian Guide. With the constants exactly as printed, η lies in [0.7036, 0.9557] over the whole box (Tier C, given the constants); the true range contains a value ≥ 0.94428 and a value ≤ 0.74271. An independent AI audit certifies this interval and a tighter one, [0.7410, 0.9455]. The algebra (closed form, 0 < η < 1, monotone delay formula) is checked in Lean (Tier A, statement lock owed). Also reported: a dilute-water pH scan (Tier X) and a partial reproduction of the alkalinity-front retardation arithmetic of Jessen et al., whose printed numbers are not all mutually consistent. The value η ≈ 0.8 and its dependence on temperature, salinity and pCO2 are long known; what is added is an enclosure with stated constants and a monotone closed form. What this is NOT. No tonnes of CO2 removed, no climate effect, no statement on ecological or biogeochemical safety, no deployment advocacy for ocean alkalinity enhancement or enhanced weathering. Equilibrium thermodynamics of a model only: no gas-exchange kinetics, no CaCO3 saturation, no mixing, no organic alkalinity, surface pressure only. Limitations. Independently audited by a different AI agent instance (AUDIT.md, ACCEPT_WITH_CORRECTIONS, ten corrections applied); no human audit and no Lean statement lock (owed). The primary papers for the constants (Weiss 1974, Lueker 2000, Dickson 1990, Millero 1995, Uppstrom 1974) were not read: the constants rest on the Guide's transcription and PyCO2SYS. No second CO2SYS package and no independent interval library (mpmath.iv in both producer and auditor). The U0 enclosure is sound but loose (branch-and-bound stopped at its evaluation cap); the U1/U2 widening is mostly interval overestimation. Lean proves algebra only (hand-supplied derivatives, nothing about constants or enclosures). The Elenchus ledger gate exits with code 1 (0 blocking findings, 2 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row).