IndisputableMonolith.Verification.CPT.EpsilonCertification
Defines the ε-meaning set of a scalar objective on a finite candidate set: the candidates whose cost is within ε of the minimum. Supplies stability of approximate argmins and membership of those argmins in the mean-ε set. Cited by the CPT export surface when packaging window-identifiability and pipeline theorems that tolerate numerical slack.
claimFor a scalar objective $f$ on a finite candidate set $C$ and tolerance $\varepsilon \ge 0$, the $\varepsilon$-meaning set is $\mathrm{MeanEps}(f,\varepsilon) = \{ c \in C : f(c) \le \inf_{c'} f(c') + \varepsilon \}$. Approximate argmins are stable under small perturbations and lie in this set.
background
In the CPT verification layer one often minimizes a scalar cost over a discrete candidate set (windows, matchings, or discrete parameters). Exact uniqueness of the minimizer is too brittle for formal certificates that must survive floating-point or model slack, so one works with an $\varepsilon$-neighborhood of the minimum.
The module introduces $\mathrm{MeanEps}$, the set of candidates whose objective value lies within $\varepsilon$ of the global infimum, together with elementary membership and stability facts for approximate argmins. The surrounding CPT export surface packages fully proved window-identifiability and pipeline results; this module supplies the $\varepsilon$-tolerant vocabulary those certificates use when the exact argmin is not required.
proof idea
Definition module plus short stability lemmas. MeanEps is introduced as the sublevel set of the objective relative to its infimum plus $\varepsilon$. The companion facts (approximate-argmin stability and membership in MeanEps) are elementary unfoldings of that definition: if a candidate is within $\varepsilon$ of the minimum, it belongs to MeanEps; small perturbations of the objective keep approximate argmins inside a slightly enlarged MeanEps. No deep arithmetic or Recognition-specific forcing is used.
why it matters in Recognition Science
Feeds the CPT export surface (IndisputableMonolith.Verification.CPT.Exports), which exposes citation-friendly aliases for the window-identifiability family (paper Thm. 4.5 / 6.5) and the P→B→A pipeline composition (§5 / §6). Those theorems need a clean notion of “good enough” candidates when exact uniqueness fails; MeanEps and its stability lemmas are that notion. Without an $\varepsilon$-meaning set, the export layer would have to restate sublevel-set reasoning at every call site.
scope and limits
- Does not prove uniqueness of the exact global minimizer.
- Does not construct or enumerate the candidate set C.
- Does not bound ε from Recognition constants (phi, eight-tick, etc.).
- Does not address continuous parameter spaces or infinite C.
- Does not itself export WINDOW_* or CPT_PIPELINE_* theorems.