approx_argmin_mem_meanEps
plain-language theorem explainer
A minimizer of a uniformly ε-perturbed cost lies in the 2ε-meaning set of the true cost. Anyone citing the CPT epsilon-certification ranking layer uses this set-level form. The proof is a one-line membership wrapper around the pointwise 2ε-suboptimality lemma.
Claim. Let $c,\hat{c}:O\to\mathbb{R}$ and $\varepsilon\in\mathbb{R}$. Suppose $|\hat{c}(o)-c(o)|\le\varepsilon$ for every $o\in O$, and $\hat{o}$ minimizes $\hat{c}$. Then $\hat{o}$ lies in the $2\varepsilon$-meaning set of $c$: for every $o'$, $c(\hat{o})\le c(o')+2\varepsilon$.
background
This module is the CPT epsilon-certification layer: a claim-honest Lean account of the paper's noise ranking setup. The three ingredients are a uniform perturbation bound $|\hat{c}-c|\le\varepsilon$, transfer of minimizers from $\hat{c}$ to $c$, and an explicit $2\varepsilon$-suboptimality guarantee.
The $\varepsilon$-meaning set of a scalar objective $c$ is the set of candidates $o$ that are within $\varepsilon$ of optimal: $\mathrm{MeanEps}(c,\varepsilon)={o\mid \forall o',, c(o)\le c(o')+\varepsilon}$. Membership is exactly the set-level packaging of $\varepsilon$-suboptimality.
The upstream pointwise result states: if $\hat{o}$ minimizes $\hat{c}$ and $|\hat{c}-c|\le\varepsilon$ everywhere, then $c(\hat{o})\le c(o)+2\varepsilon$ for all $o$. That inequality is the content that set membership rephrases.
proof idea
One-line set-membership wrapper. Unfold membership in the $2\varepsilon$-meaning set (introduce an arbitrary competitor $o$), then apply the upstream stability lemma, which already supplies $c(\hat{o})\le c(o)+2\varepsilon$ under the same hypotheses. No extra arithmetic or case splits.
why it matters
Gives the set-level packaging of approximate argmin transfer that the CPT exports surface as CPT_EPS_approx_argmin_mem_meanEps ("perturbed minimizer lies in MeanEps c (2ε)"). Downstream consumers that reason about meaning sets rather than pointwise inequalities cite this form.
In the paper's epsilon/noise ranking layer, this is the clean certificate that a noisy ranking still lands inside a controlled sublevel of the true cost. It closes the local certification story for the module: perturbation bound, minimizer transfer, and explicit $2\varepsilon$ guarantee, all in set language ready for export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.