phiStar_in_procedureSpace
plain-language theorem explainer
Under explicit soundness and finite-data hypotheses, the canonical CPT pipeline procedure Φ* belongs to the corresponding procedure space. Domination theorems that compare Φ* to rival procedures on a class cite this packing step. The proof is a one-line wrapper of the Pipeline-level membership lemma.
Claim. Let $P$, $B$, $A$ be projection, coercivity, and aggregation stages, and let $\Phi^*$ be the CPT procedure they define. Fix predicates $\mathrm{isZero}$, $\mathrm{isNonzero}$ on the input type and a finite-data predicate on procedures. If $\Phi^*(x)=\mathrm{zero}$ implies $\mathrm{isZero}(x)$, $\Phi^*(x)=\mathrm{nonzero}$ implies $\mathrm{isNonzero}(x)$, and $\Phi^*$ satisfies finite data, then $\Phi^*$ is an element of the procedure space determined by those three predicates.
background
The CPT Optimality module studies class-restricted domination among decision procedures built from a three-stage pipeline: a projection stage $P:X\to Y$, a coercivity stage $B:Y\to Z$, and an aggregation stage $A$ on $Z$. The composite procedure is abbreviated $\Phi^*$ (PhiStar); it returns a decision tag (zero, nonzero, or inconclusive) on each input.
A procedure space packages three requirements: soundness on the zero tag, soundness on the nonzero tag, and a finite-data constraint. Membership is the hygiene gate before any domination comparison: one only ranks procedures already certified as sound and finitely presented.
The module keeps those hypotheses explicit rather than baking them into definitions, matching the claim-hygiene style of the Verification layer. Upstream, the same packing statement lives in Pipeline; this declaration re-exports it into the Optimality namespace.
proof idea
One-line wrapper. The body applies Pipeline.phiStar_in_procedureSpace to the same stages $P,B,A$, the same predicates, and the three hypotheses $h_{\mathrm{zero}}$, $h_{\mathrm{nonzero}}$, $h_{\mathrm{finite}}$, returning the ProcedureSpace witness with no extra reasoning.
why it matters
This is the entry ticket for Φ* into the Optimality development. Sibling results (phiStar_resolves_nondegenerate, phiStar_dominates, phiStar_dominates_global) compare Φ* against other procedures on a class; they need Φ* already seated in the procedure space under the same soundness and finite-data assumptions.
The module doc frames the goal as class-restricted domination: if a rival Ψ resolves every point of a class and agrees with Φ* there, then Φ* dominates on that class. Packing Φ* first keeps the domination theorem free of hidden structure. In the broader Recognition verification stack this is bookkeeping rather than a forcing-chain step (T0–T8), but it is the hygiene lemma that lets CPT optimality claims stay fully explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.