phiStar_dominates_global
plain-language theorem explainer
If a CPT procedure resolves every input and agrees pointwise with the canonical pipeline procedure PhiStar, then PhiStar dominates it on the whole domain. Verification and CPT-export consumers cite this as the global (unrestricted-class) domination corollary. The proof is a one-line specialization of the class-restricted domination theorem to the universal set.
Claim. Let $P$, $B$, $A$ be the projection, coercivity, and aggregation stages of a CPT pipeline, and let $\Phi^\star = \mathrm{PhiStar}(P,B,A)$. Let $\Psi$ be any procedure on $X$. If $\Psi$ never returns inconclusive on any $x \in X$, and $\Phi^\star(x) = \Psi(x)$ for every $x \in X$, then $\Phi^\star$ dominates $\Psi$ on the full domain $\mathrm{Set.univ}$.
background
The CPT Optimality module studies class-restricted domination among decision procedures built from a three-stage pipeline: projection $P : X \to Y$, coercivity $B : Y \to Z$, and aggregation $A$ on $Z$. The canonical composite is written $\Phi^\star = \mathrm{PhiStar}(P,B,A)$.
A procedure resolves a class $C \subseteq X$ when it never returns the inconclusive tag on points of $C$. Domination on $C$ (the relation dominatesOn) compares two procedures that both resolve $C$: the dominating one is preferred wherever they differ, under the module's fixed preference order on decision tags.
The parent result is the class-restricted theorem: if $\Psi$ resolves $C$ and $\Phi^\star$ agrees with $\Psi$ on $C$, then $\Phi^\star$ dominates $\Psi$ on $C$. The present statement is the specialization $C = \mathrm{Set.univ}$.
proof idea
One-line term wrapper. Apply the class-restricted domination lemma phiStar_dominates at $C = \mathrm{Set.univ}$, feeding the global resolve hypothesis unchanged and turning the pointwise global agreement hypothesis into the restricted agreement proof by ignoring the membership side-condition (intro x _hx; exact hAgreeGlobal x).
why it matters
Closes the global case of CPT optimality hygiene: once a competing procedure is total (resolves everywhere) and coincides with the pipeline composite, the composite is dominant on the full input type. Downstream, CPT_OPT_phiStar_dominates_global in the CPT Exports module re-exports this fact as the named global-class domination specialization for external consumers.
Inside Recognition verification, this is bookkeeping rather than a new physical law: it packages the unrestricted-class instance so export and audit layers can cite a single global theorem instead of threading Set.univ through the class-restricted statement. It does not itself invoke the forcing chain (T5–T8), RCL, or the mass ladder; those enter only if the pipeline stages $P,B,A$ are later instantiated from RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.