CPT_PIPELINE_factorization
plain-language theorem explainer
The CPT pipeline functional equals the ordinary composition of its three stage maps: aggregation after coercivity after projection. Anyone citing paper §5 (P→B→A composition) uses this export. The proof is a one-line re-export of the core pipeline factorization lemma.
Claim. For types $X,Y,Z$ and stages $P$ (projection $X\to Y$), $B$ (coercivity $Y\to Z$), and $A$ (aggregation on $Z$), the pipeline functional $\Phi^\star(P,B,A)$ equals $A.\mathrm{run}\circ B.\mathrm{run}\circ P.\mathrm{run}$.
background
This module is the CPT export surface: citation-friendly aliases for a fully proved formalization layer (no sorry, no new axioms). The CPT_PIPELINE_* family maps to the paper’s P→B→A pipeline in §§5–6.
A pipeline is three typed stages. Projection $P$ maps raw observations in $X$ to an intermediate space $Y$. Coercivity $B$ tightens $Y$ into $Z$. Aggregation $A$ collapses $Z$ to the scalar (or decision) output. The star functional $\Phi^\star$ is the named composite of those stages.
The claim is definitional factorization: running the pipeline is exactly running $P$, then $B$, then $A$. Downstream exports in the same file handle soundness and nonzero soundness of that composite; forced-factorization and optimality live in sibling CPT_FACTOR_* and CPT_OPT_* aliases.
proof idea
Term-mode one-line wrapper. It applies Pipeline.pipeline_factorization to the three stage witnesses $P$, $B$, and $A$, discharging the equality $\Phi^\star(P,B,A)=A.\mathrm{run}\circ B.\mathrm{run}\circ P.\mathrm{run}$ by the core lemma already proved in the Pipeline module. No extra rewriting or case analysis.
why it matters
Paper §5 states that the CPT pipeline is $A\circ B\circ P$. This export makes that equality a stable, citable name on the verification surface so later soundness and optimality statements can quote a single factorization fact rather than unfold stage definitions.
It anchors the CPT_PIPELINE_* block beside window-identifiability (WINDOW_*), forced factorization (CPT_FACTOR_*, paper Thm. 5.1), and domination (CPT_OPT_*, paper Thm. 6.11). In the broader Recognition stack it is bookkeeping for the measurement/decision layer, not a forcing-chain step (T5–T8), but it is what lets composed CPT claims stay aligned with the paper’s P→B→A narrative.
No downstream dependents are recorded yet; sibling soundness aliases are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.