ProjectionStage
plain-language theorem explainer
The first stage of the CPT certified pipeline is a typed projection map from raw inputs X to a neutral intermediate space Y. Anyone citing pipeline factorization, zero/nonzero soundness, or PhiStar optimality needs this carrier. It is a one-field structure: just the run map, with no extra axioms.
Claim. A projection stage from type $X$ to type $Y$ is a structure consisting of a single map $\mathrm{run}\colon X\to Y$ (the preprocessing/neutrality projection $P$ in the CPT pipeline $P\to B\to A$).
background
The CPT pipeline module fixes a three-stage composition shape used throughout certified procedure theory: projection $P$, coercivity conversion $B$, then aggregation/decision $A$. The module theorems target definitional factorization $\Phi^\star=A\circ B\circ P$, zero and nonzero soundness under explicit assumptions, and procedure-space membership for $\Phi^\star$.
ProjectionStage is the typed carrier for the first leg. Its only data is a function $X\to Y$; neutrality and preprocessing content live in how instances are chosen, not in extra fields here. Sibling stages CoercivityStage and AggregationStage play the same role for $B$ and $A$.
Upstream naming collisions (the cosmology bichromatic edge set $B$, RS-native measurement map) are unrelated imports; this structure is local to the verification pipeline and does not inherit their semantics.
proof idea
No proof: this is a structure definition. It packages a single field run : X → Y as the $P$ stage. Downstream abbreviations such as PhiStar and the factorization theorem simply compose P.run with the run maps of the $B$ and $A$ stages.
why it matters
Every exported CPT pipeline and optimality result is parameterized by a ProjectionStage. CPT_PIPELINE_factorization states definitional equality $\Phi^\star=A\circ B\circ P$ (paper §5). CPT_PIPELINE_sound and CPT_PIPELINE_nonzero_sound give zero- and nonzero-decision soundness of the composed map. CPT_OPT_phiStar_dominates and its global specialization (paper Thm. 6.11) quantify over any such $P$ when proving that $\Phi^\star$ dominates agreeing procedures on a class.
In the Recognition verification stack this is scaffolding for certified composition, not a physics forcing step (T0–T8). It exists so optimality and soundness theorems can treat the projection leg uniformly without hard-coding a particular preprocessing map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.