CPT_EPS_approx_argmin_stability
plain-language theorem explainer
Under uniform absolute error at most ε between a true cost and a perturbed cost, any minimizer of the perturbed cost is 2ε-optimal for the true cost. CPT verifiers and ε-noise certification cite this export. The proof is a one-line re-export of the EpsilonCertification stability lemma.
Claim. Let $c,\hat{c}:O\to\mathbb{R}$ and $\varepsilon\in\mathbb{R}$. If $|\hat{c}(o)-c(o)|\le\varepsilon$ for every candidate $o$, and $\hat{o}$ minimizes $\hat{c}$, then for every $o$ one has $c(\hat{o})\le c(o)+2\varepsilon$.
background
This lives on the CPT export surface: citation-friendly aliases for the fully proved CPT formalization layer. The CPT_EPS_* family maps to the paper's ε-noise layer (§5 ε-optimal certification).
The scalar objective $c$ is the true cost on a candidate type $O$; $\hat{c}$ is a uniformly $\varepsilon$-close perturbation. The set-level companion is the $\varepsilon$-meaning set $\mathrm{MeanEps}(c,\varepsilon)={o\mid \forall o',, c(o)\le c(o')+\varepsilon}$, so the claim is that a perturbed minimizer lies in $\mathrm{MeanEps}(c,2\varepsilon)$.
Upstream, approx_argmin_stability in EpsilonCertification states the same bound: if $\hat{o}$ minimizes perturbed costs and $|\hat{c}-c|\le\varepsilon$, then $\hat{o}$ is $2\varepsilon$-optimal for the true cost $c$.
proof idea
One-line term wrapper. It applies EpsilonCertification.approx_argmin_stability to the same $c$, $\hat{c}$, $\varepsilon$, error hypothesis, candidate $\hat{o}$, and minimality hypothesis, and returns the $2\varepsilon$-optimality conclusion unchanged. No extra algebraic work occurs at the export layer.
why it matters
Gives the public CPT name for the basic stability fact in the paper's ε-noise certification layer (§5): noisy argmins remain controlled for the true objective. Downstream used-by edges are empty at present; siblings on this surface cover window identifiability, the P→B→A pipeline, φ-star domination, and forced factorization. In the Recognition verification stack this is the elementary noise lemma that justifies treating approximate cost oracles as $2\varepsilon$-optimal selectors, without touching the forcing chain (T0–T8) or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.