pipeline_factorization
plain-language theorem explainer
The CPT membership certifier built from three stages equals the ordinary function composition of those stages. Anyone citing the certified CPT pipeline shape (paper §5) uses this equality. The proof is pure definitional reflexivity: the certifier is defined as that composition.
Claim. For stages $P:X\to Y$ (projection), $B:Y\to Z$ (coercivity), and $A:Z\to\mathrm{DecisionTag}$ (aggregation), the canonical CPT certifier $\Phi^*$ formed from $(P,B,A)$ satisfies $\Phi^*=A\circ B\circ P$ as maps $X\to\mathrm{DecisionTag}$.
background
The CPT pipeline module fixes a three-stage composition used throughout certified CPT verification. Projection is a preprocessing map $X\to Y$; coercivity is a conversion $Y\to Z$; aggregation is a decision map $Z\to\mathrm{DecisionTag}$.
The canonical certifier $\Phi^$ is defined by feeding an input through those three maps in order: $\Phi^(x)=A(B(P(x)))$. A procedure here is simply a map from the input type to a decision tag. The module's job is to pin the composition shape, then prove zero/nonzero soundness and procedure-space membership under explicit hypotheses.
This factorization is the definitional backbone for those later soundness theorems and for the exported paper-facing statement that the pipeline equals $A\circ B\circ P$.
proof idea
One-line rfl. Unfolding $\Phi^*$ yields $\lambda x.,A.\mathrm{run}(B.\mathrm{run}(P.\mathrm{run},x))$, which is definitionally $A.\mathrm{run}\circ B.\mathrm{run}\circ P.\mathrm{run}$. No lemmas are applied.
why it matters
This pins the certified CPT composition shape used by the verification stack: projection, then coercivity, then aggregation. The export CPT_PIPELINE_factorization re-states the same equality for paper §5 ("Pipeline is definitionally equal to $A\circ B\circ P$").
Sibling results in the module build on that shape: zero-decision soundness, nonzero soundness, and the claim that $\Phi^*$ lies in the procedure space (soundness plus a finite-data predicate). Without definitional factorization, those soundness statements would have to reason about an opaque composite rather than staged maps.
In the broader Recognition verification layer this is scaffolding hygiene rather than a physics forcing step: it locks the interface so later CPT certificates compose cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.