phiStar_resolves_nondegenerate
plain-language theorem explainer
If the canonical CPT procedure Φ* never returns inconclusive on a class C, then C is contained in the resolved set of Φ*. Class-restricted optimality arguments for Φ* use this to turn a ResolvesClass hypothesis into set inclusion. The proof is a one-line application of the general procedure-resolves-class lemma to Φ*.
Claim. Let $\Phi^*$ be the CPT procedure built from a projection stage $P$, a coercivity stage $B$, and an aggregation stage $A$. If $\Phi^*$ resolves every point of a class $C\subseteq X$ (i.e., never returns inconclusive on $C$), then $C\subseteq\mathrm{resolvedSet}(\Phi^*)$.
background
The module develops class-restricted domination for CPT procedures: maps from inputs $X$ to a decision tag that may be conclusive or inconclusive. The distinguished procedure $\Phi^*$ is assembled by the pipeline from three stages (projection $P:X\to Y$, coercivity $B:Y\to Z$, aggregation $A$ on $Z$).
A procedure resolves a class $C$ when it never returns the inconclusive tag on any $x\in C$. The resolved set of a procedure is the set of inputs on which it is conclusive. The module keeps these hypotheses explicit so domination theorems can cite them without hidden structure.
Upstream, the general fact is that any procedure satisfying the ResolvesClass predicate has its class inside its resolved set; the present statement specializes that fact to $\Phi^*$.
proof idea
One-line term proof: apply the general lemma procedure_resolves_class at the class $C$ and the procedure $\Phi^(P,B,A)$, feeding the given ResolvesClass hypothesis. No extra algebraic work; the specialization is purely by substitution of $\Phi^$.
why it matters
This is the nondegeneracy bridge inside CPT optimality: before $\Phi^$ can dominate a competitor $\Psi$ on a class, one needs $C$ inside the resolved set of $\Phi^$. Sibling results (phiStar_dominates, phiStar_dominates_global) package the full domination claim under explicit resolve-and-agree hypotheses, matching the module's claim-hygiene stance.
In the broader Recognition verification layer, $\Phi^$ is the canonical pipeline procedure against which alternative decision procedures are compared. The lemma does not itself force constants or geometry (T5–T8); it only certifies that a resolve hypothesis on $\Phi^$ is set-theoretic inclusion, so later optimality statements stay clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.