MeanEps
plain-language theorem explainer
The ε-meaning set of a scalar cost c on candidates O is the set of points within ε of global optimality: c(o) ≤ c(o')+ε for every o'. CPT epsilon-certification and ranking-stability arguments cite it as the set-level target of 2ε-suboptimality. The body is a one-line set comprehension, not a proof.
Claim. For a cost $c : O \to \mathbb{R}$ and tolerance $\varepsilon \in \mathbb{R}$, the $\varepsilon$-meaning set is $\{ o \in O \mid \forall o' \in O,\; c(o) \le c(o') + \varepsilon \}$.
background
The CPT epsilon certification module formalizes the paper's noise/ranking layer: if a perturbed cost $\hat c$ stays within uniform absolute error $|\hat c - c| \le \varepsilon$ of the true cost $c$, then a minimizer of $\hat c$ is $2\varepsilon$-optimal for $c$.
In Recognition Science the scalar objectives that play the role of $c$ are recognition costs built from the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), including event costs, multiplicative-recognizer derived costs, and rung-coarsened multiset sums. The meaning set is the abstract set-level packaging of near-minimality for any such objective on a candidate type $O$.
Sibling results then transfer argmin statements into membership in this set at tolerance $2\varepsilon$.
proof idea
Definition only: MeanEps c ε is the set comprehension of candidates $o$ that beat every rival up to additive $\varepsilon$. No lemmas or tactics; the downstream theorems instantiate this set at $\varepsilon \mapsto 2\varepsilon$.
why it matters
This is the set-level carrier for the CPT epsilon layer's $2\varepsilon$-suboptimality guarantee. Downstream, approx_argmin_mem_meanEps states that a perturbed minimizer under $|\hat c-c|\le\varepsilon$ lies in MeanEps c (2ε); the Exports re-exports that fact and the pointwise stability form as CPT_EPS_approx_argmin_mem_meanEps and CPT_EPS_approx_argmin_stability.
In the broader framework it lets ranking or selection arguments over recognition costs (J-cost on ratios, rung ladders, observer costs) survive bounded measurement or model noise without claiming exact uniqueness of the argmin. It does not itself invoke T5–T8 or the RCL; it is verification scaffolding around whatever cost those layers supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.