resolvedSetOn
plain-language theorem explainer
The resolved set of a CPT procedure restricted to a class C: inputs that lie in C and are decided (not inconclusive). Anyone comparing procedures on a subclass cites this. It is a one-line set-builder: intersection of C with the unrestricted resolved set.
Claim. For a type $X$, a class $C \subseteq X$, and a CPT procedure $\Phi : X \to \{\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}\}$, the resolved set of $\Phi$ on $C$ is $\{ x \in C \mid \Phi(x) \neq \mathrm{inconclusive} \}$.
background
The CPT verification core supplies small interfaces for ternary decision procedures: tags zero / nonzero / inconclusive, procedures as maps $X \to$ tags, and resolved-set utilities. A procedure is any such map; its unrestricted resolved set is the set of inputs where the tag is not inconclusive.
This definition restricts that set to a class $C$. The module keeps statements claim-honest and composable across WindowIdentifiability, Pipeline, Optimality, and ForcedFactorization. Class-restricted comparison is the next layer: domination on $C$ is stated in terms of these restricted resolved sets.
proof idea
Pure definition by set comprehension. No lemmas are applied: the body is the intersection of $C$ with the unrestricted resolved set of $\Phi$, written as membership in both.
why it matters
Feeds the class-restricted domination relation: $\Phi$ dominates $\Psi$ on $C$ when the resolved set of $\Psi$ on $C$ is contained in that of $\Phi$ on $C$, and the two procedures agree on every point $\Psi$ resolves inside $C$. Without the restriction, domination would be global and too strong for staged CPT arguments that only need control on a window or factor class.
In the verification stack this is scaffolding for soundness and optimality comparisons of ternary procedures, not a physics forcing step (T0–T8). It keeps A/B/C-stage wrappers honest about the domain on which resolution is claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.