IndisputableMonolith.Verification.CPT.Pipeline
Assembles the CPT verification map as a three-stage pipeline (projection, coercivity, aggregation) and packages the end-to-end procedure PhiStar with soundness lemmas. Cited by anyone using the paper's P→B→A composition (§5/§6). Argument is definitional factorization plus zero/nonzero tag checks against the Core decision interface.
claimThe module defines the CPT pipeline as a composition $P\to B\to A$ of a projection (preprocessing) stage, a coercivity stage, and an aggregation stage, yielding a distinguished procedure $\Phi^*$ in the procedure space, together with soundness statements that $\Phi^*$ correctly returns the zero and nonzero decision tags on inputs resolved by the pipeline.
background
CPT verification lives in the Recognition Science Verification layer. Upstream Core supplies the reusable interfaces: decision tags (zero / nonzero / inconclusive), procedure and resolved-set utilities, class-restricted domination, and thin wrappers around the CPM A/B/C closure theorems.
WindowIdentifiability supplies the matrix-level core used by window arguments: injective reconstruction from finite window measurements, equivalence with trivial kernel of the measurement map, and a full-column-rank predicate identified with injectivity.
This module sits between those ingredients and the export/optimality layer. It names the three stages of the paper pipeline, with the $P$ stage as the preprocessing/projection map, then builds the composite procedure and records that it lands in the procedure space.
proof idea
Definitional assembly module, not a deep analytic proof. It introduces stage carriers (ProjectionStage, CoercivityStage, AggregationStage), constructs PhiStar as the composite procedure, and records factorization plus soundness facts (pipeline_factorization, pipeline_sound, pipeline_nonzero_sound, phiStar_in_procedureSpace). Soundness is checked against Core decision tags and resolved-set utilities imported from the CPT core; window injectivity is used only as an upstream interface, not re-proved here.
why it matters in Recognition Science
Feeds the citation surface in Exports: the CPT_PIPELINE_* aliases map to the paper's P→B→A pipeline (§5 / §6 composition), alongside the WINDOW_* family from Thm. 4.5 / 6.5. Also imported by Optimality, which proves class-restricted domination for PhiStar once a competing procedure Psi resolves every input in the class and agrees with PhiStar there. Without this module there is no single named end-to-end CPT procedure for those export aliases and domination theorems to attach to.
scope and limits
- Does not prove window identifiability or measurement injectivity (upstream).
- Does not prove class-restricted domination or optimality of PhiStar (downstream).
- Does not add RS forcing-chain steps (T0–T8), constants, or mass-ladder claims.
- Does not claim soundness outside the Core decision-tag and resolved-set interface.
- Does not introduce new axioms; export layer asserts fully proved aliases only.