ResolvesClass
plain-language theorem explainer
A CPT procedure resolves a class C when it never returns the inconclusive tag on any point of C. Optimality and domination theorems cite this predicate as the explicit hypothesis that the competitor procedure is decisive on the target class. The body is a one-line universal quantification over membership in C.
Claim. A procedure $\Phi$ resolves a class $C \subseteq X$ when for every $x \in C$, the output $\Phi(x)$ is not the inconclusive decision tag (so $\Phi(x)$ is either zero or nonzero).
background
In the CPT verification stack, a procedure on inputs of type $X$ is a map $\Phi : X \to {\mathrm{zero},,\mathrm{nonzero},,\mathrm{inconclusive}}$. The ternary tag is the DecisionTag inductive: zero and nonzero are decisive answers; inconclusive means the procedure declines to decide.
This module studies class-restricted domination for CPT procedures built from a projection–coercivity–aggregation pipeline. The standing setup keeps hypotheses explicit: a competitor $\Psi$ must resolve every input in the target class, and must agree with the distinguished procedure $\Phi^\star$ on that class, before domination is claimed.
Resolved inputs are those on which the procedure is not inconclusive. The present predicate packages that condition uniformly over a set $C$, so later theorems can state “$\Psi$ resolves $C$” without repeating the quantifier.
proof idea
Definition, not a proved theorem. The body is the Prop $\forall x,, x\in C \Rightarrow \Phi(x)\neq\mathrm{inconclusive}$. No lemmas are applied; the predicate is the named packaging of that universal statement for use as a hypothesis.
why it matters
Class resolution is the gate hypothesis for the CPT optimality theorems in this module and their export wrappers. Downstream, phiStar_dominates states that if $\Psi$ resolves $C$ and agrees with $\Phi^\star$ on $C$, then $\Phi^\star$ dominates $\Psi$ on $C$ (paper Thm. 6.11 via the export CPT_OPT_phiStar_dominates). The global specializations replace $C$ by the universe and keep the same resolve hypothesis.
Sibling uses include showing $\Phi^\star$ itself resolves nondegenerate classes, and the inclusion that a resolving procedure’s class sits inside its resolved set. Without this predicate, domination would either quantify over all of $X$ or bury the decisiveness assumption inside the proof, violating the module’s claim-hygiene design.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.