cert
plain-language theorem explainer
Packages three elementary properties of the solvent-extraction domain cost into one certificate: diagonal vanishing, nonnegativity for positive arguments, and positivity of the canonical threshold. Chemists or RS auditors citing the liquid-liquid extraction claim (optimal distribution ratio D = φ) use this witness. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost of equal nonzero arguments vanishes, $\mathrm{domainCost}(r,r)=0$ for $r\neq 0$; (ii) for positive $m,e$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical extraction threshold is strictly positive.
background
The module treats liquid-liquid extraction in Recognition Science units. The distribution ratio is $D=[\mathrm{analyte}]{\mathrm{org}}/[\mathrm{analyte}]{\mathrm{aq}}$. RS predicts the efficient operating point $D_{\mathrm{optimal}}=\varphi\approx 1.618$, where the J-cost $J(D)=J(\varphi)\approx 0.118$ leaves about 11.8% of analyte in the aqueous phase (88.2% extracted).
Domain cost is the local cost functional on the two concentration (or phase) arguments; the certificate demands it be zero on the diagonal and nonnegative off it. The canonical threshold is the positive cutoff used to mark efficient extraction. Upstream, nonnegativity of recognition cost is the standard J-cost fact: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals.
proof idea
One-line structure instance. The three fields of SolventExtractionCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No new algebra is performed; the definition only packages those three results.
why it matters
Gives a single named witness that the cost side of the solvent-extraction story is well-formed: zero self-cost, nonnegative mismatch cost, and a positive efficiency threshold. That is the structural prerequisite for reading off $D_{\mathrm{optimal}}=\varphi$ from the J-cost minimum and for the numerical claim $J(\varphi)\approx 0.118$. It sits in the chemistry layer fed by the foundation cost facts (J-nonnegativity from ObserverForcing / Cost) and by the forcing-chain landmarks T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point). No downstream consumers are recorded yet; the sibling cert_inhabited is the natural next step that turns the definition into an inhabited Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.