approx_argmin_stability
plain-language theorem explainer
If a candidate minimizes a uniformly ε-perturbed cost, it is at most 2ε-suboptimal for the true cost. CPT/ranking auditors cite this to transfer argmin certificates from noisy scores to exact ones. The proof is a short chain of absolute-value bounds closed by linear arithmetic.
Claim. Let $c,\hat{c}:O\to\mathbb{R}$ and $\varepsilon\in\mathbb{R}$. If $|\hat{c}(o)-c(o)|\le\varepsilon$ for every $o\in O$, and $\hat{o}$ minimizes $\hat{c}$, then for every $o\in O$ one has $c(\hat{o})\le c(o)+2\varepsilon$.
background
The CPT epsilon certification module formalizes the paper's noise/ranking layer: a uniform absolute perturbation bound $|\hat{c}-c|\le\varepsilon$, transfer of minimizers from the perturbed cost to the true cost, and an explicit $2\varepsilon$-suboptimality guarantee.
Here $O$ is an arbitrary option type, $c$ is the true real-valued cost, and $\hat{c}$ is an observed or computed surrogate. The hypothesis that $\hat{o}$ minimizes $\hat{c}$ is pointwise comparison $\hat{c}(\hat{o})\le\hat{c}(o)$ for all $o$, not a set-theoretic argmin package.
The companion set-level notion is the $2\varepsilon$-meaning set of $c$ (options whose true cost is within $2\varepsilon$ of the global minimum). This theorem is the pointwise engine behind membership in that set.
proof idea
Fix an arbitrary option $o$. Split the absolute-error hypothesis at $\hat{o}$ and at $o$ via abs_le.mp to get the one-sided bounds $c(\hat{o})\le\hat{c}(\hat{o})+\varepsilon$ and $\hat{c}(o)\le c(o)+\varepsilon$. Chain these with the minimality inequality $\hat{c}(\hat{o})\le\hat{c}(o)$ and close by linarith. No external lemmas beyond Mathlib absolute-value and linear arithmetic are required.
why it matters
This is the core transfer lemma of the CPT epsilon layer. Downstream, approx_argmin_mem_meanEps packages the same hypotheses into set membership: the perturbed minimizer lies in the $2\varepsilon$-meaning set of $c$. The verification export CPT_EPS_approx_argmin_stability re-exports the statement for the CPT API surface.
In the paper pipeline this underwrites claim-honest ranking under measurement or model noise: a certified argmin of $\hat{c}$ remains a controlled near-minimizer of $c$, with the factor $2$ sharp for uniform absolute error. It is pure verification scaffolding rather than a forcing-chain (T0–T8) step, but it is what makes epsilon-certified CPT claims machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.