cert
plain-language theorem explainer
Packages three well-posedness facts for the XPS domain cost (vanishes on the diagonal, nonnegative off it, positive canonical threshold) into one certificate record. Anyone citing the RS model of XPS chemical shifts as a J-cost defect would point here as the inhabited witness. Construction is a structure literal wiring three local lemmas.
Claim. There is an XPS binding certificate: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$ the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The module treats XPS binding-energy chemical shifts (typically 0–5 eV) as a Recognition-Science cost defect. The working ansatz is that a shift scales like $J(\varphi)$ times a characteristic energy; with $J(\varphi)\approx 0.118$, a raw $E_{\mathrm{binding}}\sim 285,\mathrm{eV}$ (C 1s) overshoots, while a per-oxidation-state yardstick of $\sim 10,\mathrm{eV}$ yields $\sim 1.18,\mathrm{eV}/\mathrm{state}$, in the observed band.
The domain cost is the local cost functional comparing a measured scale to an expected scale. The certificate structure XPSBindingCert packages the three structural axioms that cost must satisfy before any numerical shift claim: diagonal vanishing, nonnegativity, and a positive detection threshold. Upstream, nonnegativity of recognition cost is the standard $J$-cost fact that $J(x)\ge 0$ for $x>0$ (ObserverForcing / Cost).
proof idea
One-line structure constructor. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra; the def is pure packaging.
why it matters
Gives the chemistry layer a single inhabited certificate that the XPS cost model is structurally sound before any shift-magnitude claim is stated. Sits under the module's structural theorem status (0 sorry, 0 axiom) for Plan v7 XPS binding shifts. Downstream use is not yet wired (used_by empty), but the sibling cert_inhabited and any later shift bounds will consume this record rather than re-prove the three axioms. Framework link: cost nonnegativity and the diagonal minimum are the local shadow of T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$), with $\varphi$ entering only through the numerical prefactor $J(\varphi)$ in the module narrative, not in this certificate itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.