IndisputableMonolith.Verification.CPT.EpsilonCertification
Module defining the ε-meaning set of a scalar objective on a discrete candidate set in the CPT verification layer. It packages MeanEps together with stability and membership lemmas for approximate argmins. Downstream CPT export aliases import it for window-identifiability and P→B→A pipeline composition. Content is definitional plus short stability arguments, not a deep existence proof.
claimFor a scalar objective $f$ on a candidate set, the $\varepsilon$-meaning set $\mathrm{MeanEps}(f,\varepsilon)$ is the set of candidates whose value lies within $\varepsilon$ of $\inf f$. Approximate argmins are stable under small objective perturbations and belong to that mean-$\varepsilon$ set.
background
In the CPT verification stack, one often certifies not a unique exact minimizer of a scalar score on candidates, but a controlled neighborhood of near-minimizers. The $\varepsilon$-meaning set formalizes that neighborhood: every point whose objective is at most $\varepsilon$ above the global infimum is treated as "meaning-equivalent" for the certification purpose.
The module sits under Verification.CPT and is imported only by the CPT export surface. Sibling names indicate three pieces: the set constructor MeanEps, a stability statement for approximate argmins under objective noise, and a membership lemma placing approximate argmins inside the mean-$\varepsilon$ set. The surrounding CPT layer maps paper window-identifiability and pipeline composition theorems onto Lean aliases; $\varepsilon$-certification supplies the quantitative slack those aliases need when exact uniqueness fails.
proof idea
Definition module plus short lemmas, not a long tactic development. MeanEps is introduced as the sublevel set of $f$ relative to its infimum at height $\varepsilon$. Stability of approximate argmins is a standard $\varepsilon$-$\delta$ comparison of objective values under small perturbations. Membership of an approximate argmin in MeanEps is immediate from the definition once the approximation tolerance is aligned with $\varepsilon$. No deep forcing-chain or RCL argument appears here.
why it matters in Recognition Science
Feeds the CPT export surface (Verification.CPT.Exports), which re-exports citation-friendly aliases for paper Thm. 4.5 / 6.5 (window identifiability) and the P→B→A pipeline composition. Those aliases require a precise notion of "good enough" minimizer when the window or pipeline score is only approximately unique; MeanEps and the companion stability/membership facts supply that slack without introducing sorry or new axioms. Within Recognition verification, this is infrastructure for certified approximate selection rather than a landmark of the T0–T8 forcing chain.
scope and limits
- Does not prove uniqueness of the exact global minimizer.
- Does not derive physical constants, mass ladders, or forcing-chain steps T0–T8.
- Does not specify a concrete numerical $\varepsilon$ bound from experiment.
- Does not address vector-valued or multi-objective certification.
- Does not itself export the WINDOW_* or CPT_PIPELINE_* paper aliases.