procedure_resolves_class
plain-language theorem explainer
If a CPT procedure never returns inconclusive on a class C, then C is contained in that procedure's resolved set. Class-restricted optimality arguments for PhiStar cite this to convert a ResolvesClass hypothesis into ordinary set inclusion. The proof is pure definition unfolding: apply the resolve hypothesis to any member of C.
Claim. Let $\Phi : X \to \mathrm{DecisionTag}$ be a CPT procedure and $C \subseteq X$. If $\Phi$ never returns inconclusive on $C$ (i.e., $\forall x \in C,\, \Phi(x) \neq \mathrm{inconclusive}$), then $C \subseteq \{x \in X \mid \Phi(x) \neq \mathrm{inconclusive}\}$.
background
A CPT procedure on inputs of type $X$ is simply a map $\Phi : X \to \mathrm{DecisionTag}$. The resolved set of $\Phi$ is the collection of inputs on which $\Phi$ does not return the tag inconclusive. Equivalently, a procedure resolves a class $C$ when it never returns inconclusive at any point of $C$.
This module formalizes class-restricted domination for CPT procedures and proves a clean domination theorem for the distinguished procedure PhiStar. Hypotheses are kept explicit: a competitor must resolve every input in the target class, and must agree with PhiStar on that class.
The present lemma is the dictionary between the propositional form of class resolution and the set-theoretic form used by inclusion and domination statements downstream.
proof idea
One-step unfolding. Introduce an arbitrary $x \in C$. The ResolvesClass hypothesis applied at $x$ yields $\Phi(x) \neq \mathrm{inconclusive}$, which is exactly membership of $x$ in the resolved set of $\Phi$. No auxiliary lemmas are required.
why it matters
This is the bridge lemma inside CPT Optimality. Downstream, phiStar_resolves_nondegenerate packages the same inclusion for PhiStar under a ResolvesClass hypothesis, and phiStar_dominates uses class resolution plus agreement on $C$ to conclude that PhiStar dominates any competitor $\Psi$ on that class.
Without converting ResolvesClass into $C \subseteq \mathrm{resolvedSet},\Phi$, the domination relation cannot be stated as a pure set-theoretic comparison of resolved inputs. The lemma is elementary bookkeeping, but it is the hygiene step that keeps the optimality theorem's hypotheses explicit and dischargeable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.