PhiStar
plain-language theorem explainer
PhiStar is the canonical CPT decision procedure obtained by composing a projection stage, a coercivity stage, and an aggregation stage. Anyone citing the CPT optimality or pipeline soundness theorems uses this name for that composed map. The declaration is a thin abbreviation of the pipeline constructor, so equality and factorization results apply immediately.
Claim. Given a projection stage $P : X \to Y$, a coercivity stage $B : Y \to Z$, and an aggregation stage $A$ on $Z$, write $\Phi^\star = A \circ B \circ P$ for the induced CPT procedure $X \to$ decision. This abbreviation names that composed procedure.
background
The CPT Optimality module studies class-restricted domination among procedures: a procedure resolves a class $C \subseteq X$ when it never returns inconclusive on $C$, and one procedure dominates another on $C$ when it is at least as decisive wherever they are compared under agreement hypotheses.
A CPT pipeline is factored into three stages. Projection maps raw inputs in $X$ to an intermediate space $Y$. Coercivity maps $Y$ into a space $Z$ where a quantitative gap or threshold can be enforced. Aggregation turns the $Z$-valued intermediate into a final decision. The module treats these stages as explicit parameters so optimality claims stay hypothesis-clean.
Upstream, the pipeline layer already defines the composed runner and proves it equals $A \circ B \circ P$ definitionally. Soundness theorems for zero and nonzero decisions are stated for that same composition. This abbreviation is the local name used by the optimality theorems for that runner.
proof idea
Definitional one-line wrapper: PhiStar P B A is definitionally Pipeline.PhiStar P B A. No tactics or lemmas are invoked; downstream proofs inherit factorization and soundness from the pipeline module by unfolding this abbrev.
why it matters
This name is the subject of the module's domination theorems. Locally, phiStar_dominates and phiStar_dominates_global state that if another procedure $\Psi$ resolves a class $C$ and agrees with $\Phi^\star$ on $C$, then $\Phi^\star$ dominates $\Psi$ on $C$ (and the global case $C = X$).
Exported parents restate the same facts for the verification surface: CPT_OPT_phiStar_dominates is paper Theorem 6.11; CPT_OPT_phiStar_dominates_global is the universe-class specialization. Pipeline exports (CPT_PIPELINE_factorization, zero/nonzero soundness) identify $\Phi^\star$ with $A \circ B \circ P$ and certify its decision rules.
In the broader Recognition stack this is the verified CPT runner against which alternative procedures are compared, not a new physical constant. It sits in the verification layer that packages the forcing and measurement pipeline into a single named procedure for optimality claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.