phiStar_dominates
plain-language theorem explainer
On any input class that a competing CPT procedure fully resolves, if that competitor agrees pointwise with the canonical pipeline procedure, the pipeline procedure dominates it on the class. Optimality exports and the global-class specialization cite this lemma. The proof is a two-goal constructor: transfer resolution along the agreement hypothesis, then quote agreement for values.
Claim. Let $P$, $B$, $A$ be projection, coercivity, and aggregation stages of a CPT pipeline, and let $\Phi^\star$ be the induced procedure on inputs $X$. For a class $C\subseteq X$ and any procedure $\Psi$, if $\Psi$ never returns inconclusive on $C$ and $\Phi^\star(x)=\Psi(x)$ for every $x\in C$, then $\Phi^\star$ dominates $\Psi$ on $C$.
background
This module treats CPT optimality as class-restricted domination among decision procedures. A procedure maps inputs to a decision tag (including an inconclusive outcome). The canonical procedure is the three-stage pipeline composite: project $X\to Y$, apply a coercivity stage $Y\to Z$, then aggregate $Z$ to a decision.
A procedure resolves a class $C$ when it never returns inconclusive on points of $C$. Domination on $C$ is the Core relation that packages two facts: the dominator resolves (at least) the class-restricted resolved set of the competitor, and the two procedures agree as functions on that set.
Hypotheses are kept fully explicit, matching the module's claim-hygiene stance: resolution of $C$ by the competitor, and pointwise agreement with the pipeline procedure on $C$. No hidden uniqueness or global coverage is smuggled in.
proof idea
Tactic proof by constructor on the two conjuncts of domination-on-a-class.
First goal: take $x$ in the class-restricted resolved set of $\Psi$. From the sibling lemma that resolution of $C$ implies membership in the resolved set, obtain that $\Psi$ resolves $x$. Agreement on $C$ rewrites the pipeline value to $\Psi$'s value, so $x$ is likewise in the pipeline's resolved set; pack $\langle x\in C,,\text{pipeline resolves }x\rangle$.
Second goal: on that same restricted set, values agree by the pointwise agreement hypothesis on $C$ (projecting out the class membership component).
No arithmetic or pipeline internals are unfolded; the argument is pure set/function transfer along agreement.
why it matters
This is the local optimality engine for CPT verification: once a competitor resolves a class and matches the pipeline procedure there, the pipeline dominates on that class. The export CPT_OPT_phiStar_dominates re-exports it as paper Theorem 6.11 ("PhiStar dominates any agreeing procedure on the class"). The sibling phiStar_dominates_global specializes to $C=\mathrm{univ}$.
In the broader Recognition stack this sits in the Verification domain rather than the T0–T8 forcing chain: it certifies that the assembled CPT pipeline is optimal among procedures that already agree with it on the inputs of interest. It closes the class-restricted half of the domination story; global coverage is the one-line specialization that follows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.