resolvedSet
plain-language theorem explainer
The resolved set of a CPT procedure is the collection of inputs on which the procedure returns a decisive tag (zero or nonzero), excluding inconclusive outcomes. Anyone stating class-resolution, domination, or optimality for CPT pipelines cites this set as the basic support of a procedure. The definition is a one-line set comprehension from the ternary decision tag.
Claim. For a type $X$ and a CPT procedure $\Phi : X \to \{\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}\}$, the resolved set is $\{ x \in X \mid \Phi(x) \neq \mathrm{inconclusive} \}$.
background
The CPT verification core supplies small reusable interfaces for claim-honest statements across WindowIdentifiability, Pipeline, Optimality, and ForcedFactorization. A procedure on inputs of type $X$ is simply a map $\Phi : X \to$ DecisionTag, where DecisionTag is the ternary output ${\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}}$.
Resolution is the non-inconclusive case: the procedure has committed to a definite zero/nonzero answer. This module keeps that notion as a plain set so later definitions (class-restricted resolution, domination) and the lightweight wrappers around CPM A/B/C closure can quantify over the same support without re-encoding the tag inequality each time.
proof idea
Pure definition: the set comprehension ${x \mid \Phi(x) \neq \mathrm{inconclusive}}$. No lemmas or tactics; it is the canonical support extracted from the DecisionTag codomain of a Procedure.
why it matters
This is the base support object for the CPT optimality layer. resolvedSetOn intersects it with a class $C$. The theorem procedure_resolves_class rewrites class-resolution as the inclusion $C \subseteq$ resolved set. Downstream, phiStar_resolves_nondegenerate and phiStar_dominates compare the canonical pipeline procedure PhiStar against competitors by how they resolve and agree on classes, so every domination/optimality claim bottoms out on this set.
In the broader Recognition verification stack it is scaffolding language, not a physics forcing step (T0–T8): it makes procedure comparison composable so A/B/C-stage closure can be stated without ad hoc tag bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.