dominatesOn
plain-language theorem explainer
Class-restricted domination for CPT procedures: on a set C, procedure Φ resolves every input that Ψ resolves and returns the same decision tag on those inputs. Optimality theorems cite it to state that the forced PhiStar pipeline dominates any competitor that agrees on C. The body is a two-clause set-theoretic definition, not a proved claim.
Claim. For a type $X$, a class $C \subseteq X$, and procedures $\Phi,\Psi : X \to \{\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}\}$, say $\Phi$ dominates $\Psi$ on $C$ when the resolved set of $\Psi$ inside $C$ is contained in that of $\Phi$, and $\Phi(x)=\Psi(x)$ for every $x\in C$ that $\Psi$ resolves.
background
The CPT verification core supplies small interfaces for claim-honest statements across WindowIdentifiability, Pipeline, Optimality, and ForcedFactorization. A procedure on $X$ is a map to a ternary decision tag: zero, nonzero, or inconclusive. The resolved set of a procedure is the set of inputs that are not inconclusive.
Resolved-on-class restricts that set to a subclass $C$: inputs that lie in $C$ and are resolved. Domination on $C$ compares two procedures only inside that class, so global and local optimality statements can share one relation.
Upstream, the zero/nonzero tags connect to the choice-free structural zero test on PRC rationals (numerator balances the zero signed orbit). The present definition stays purely set-theoretic on procedures and does not invoke Hamiltonian or self-reference structure.
proof idea
Definitional, not a proof. The predicate is the conjunction of (i) inclusion of resolved-on-$C$ sets, $\mathrm{resolvedOn}(C,\Psi)\subseteq\mathrm{resolvedOn}(C,\Phi)$, and (ii) pointwise agreement of decision tags on every point of $\mathrm{resolvedOn}(C,\Psi)$. No lemmas are applied; consumers unfold or rewrite with this Prop.
why it matters
This is the comparison relation for CPT optimality. Downstream, phiStar_dominates and its global specialization state that if a competitor resolves a class and agrees with PhiStar there, then PhiStar dominates it on that class (paper Thm. 6.11 in the Exports layer as CPT_OPT_phiStar_dominates). The same relation feeds the univ-class variants used when the whole input type is the class.
In the Recognition stack, PhiStar is the forced recognition cost fixed point from the forcing chain (T5 J-uniqueness, T6 phi). Domination packages the claim that no alternative ternary procedure beats that forced pipeline on resolved decisions, keeping Optimality and ForcedFactorization statements composable and claim-honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.