IndisputableMonolith.Verification.CPT.Pipeline
Assembles the CPT verification pipeline as the staged composition projection → coercivity → aggregation, and introduces the distinguished procedure Φ*. Proves factorization through those stages and soundness (including nonzero soundness) relative to the Core decision tags. Export aliases and the class-restricted optimality layer cite this module. Argument shape is staged definitions plus soundness lemmas over the procedure interface.
claimThe CPT pipeline factors as a composition $P \to B \to A$ of a projection (preprocessing) map, a coercivity stage, and an aggregation stage. The resulting procedure $\Phi^*$ lies in the procedure space and is sound for zero and nonzero decisions on the resolved sets of the Core interface.
background
CPT verification sits on the Core interfaces: decision tags (zero / nonzero / inconclusive), procedure and resolved-set utilities, and a class-restricted domination relation, with thin wrappers around the CPM A/B/C closure theorems. Window identifiability supplies the matrix-level backbone: injective reconstruction from finite window measurements, equivalent to a trivial kernel of the measurement map and to a full-column-rank (injectivity) predicate.
This module packages those pieces into an explicit pipeline. Sibling objects name the stages—ProjectionStage (the $P$ preprocessing/projection map), CoercivityStage, AggregationStage—and the composite procedure PhiStar, together with factorization and soundness statements (pipeline_factorization, pipeline_sound, pipeline_nonzero_sound, phiStar_in_procedureSpace).
Notation follows Core: procedures act on measurement windows and emit decision tags; resolved sets are those inputs on which the tag is conclusive. The pipeline is the paper’s $P \to B \to A$ composition (§5 / §6), not a new measurement model.
proof idea
Definition-and-soundness module, not a single deep proof. Stages are introduced as named maps (projection, coercivity, aggregation); PhiStar is their composite, with a membership lemma placing it in the procedure space. Factorization is an equality of composites. Soundness lemmas reduce zero and nonzero tags along the stages to Core decision utilities and the window-identifiability injectivity/kernel facts, without re-proving matrix rank from scratch.
why it matters in Recognition Science
Feeds the citation surface in CPT.Exports: paper-to-Lean aliases CPT_PIPELINE_* are exactly the $P \to B \to A$ pipeline composition from §§5–6, re-exported with no sorry and no new axioms. Also imported by CPT.Optimality, which proves class-restricted domination for PhiStar once a competitor Psi resolves every input in the class and agrees with PhiStar there. Without this module there is no named Φ* or staged factorization for those export and domination theorems to quote. Landmark link is organizational: it is the verification spine that turns window identifiability and Core tags into a single citeable procedure, not a forcing-chain (T0–T8) step.
scope and limits
- Does not prove window identifiability; that lives in WindowIdentifiability.
- Does not establish class-wide domination; Optimality owns that theorem.
- Does not introduce new decision tags or alter Core resolved-set semantics.
- Does not claim optimality without the explicit agree-and-resolve hypotheses.
- Does not address physical constants, mass ladders, or forcing-chain landmarks.