AggregationStage
plain-language theorem explainer
Packages the final CPT pipeline stage: a map from an intermediate type Z into the ternary decision tag {zero, nonzero, inconclusive}. Anyone composing the certified procedure PhiStar = A ∘ B ∘ P, or citing pipeline soundness and domination theorems, depends on this carrier. It is a pure structure definition with a single field and no proof obligation.
Claim. An aggregation stage on a type $Z$ is a map $A:Z\to\{\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}\}$ (the ternary CPT decision tag).
background
The CPT pipeline module formalizes certified composition in three stages: projection/neutrality preprocessing $P$, coercivity conversion $B$, and aggregation/decision $A$. The composed procedure is definitionally $\Phi^\star=A\circ B\circ P$.
The codomain of the aggregation map is the inductive ternary tag DecisionTag from CPT.Core: zero, nonzero, or inconclusive. That tag is the only decision vocabulary used by CPT-style procedures in this development.
Upstream type parameters named $Z$ elsewhere in the monolith (path-sum measures, mass anchors) are unrelated; here $Z$ is simply the intermediate type produced by the coercivity stage.
proof idea
No proof. The declaration is a one-field structure whose sole component is a function run : Z → DecisionTag. Downstream lemmas treat an inhabitant of this structure as the third arrow in the pipeline composition.
why it matters
This is the $A$ leg of the paper §5 pipeline shape. Downstream exports use it uniformly: definitional factorization (CPT_PIPELINE_factorization: $\Phi^\star=A\circ B\circ P$), zero- and nonzero-decision soundness of the composed map, procedure-space membership for $\Phi^\star$, and the optimality theorems that $\Phi^\star$ dominates any agreeing procedure on a class (paper Thm. 6.11) and on the global class.
Without a typed aggregation stage, the factorization and domination statements cannot even be stated. It does not itself encode Recognition forcing (T5–T8) or the RCL; it is verification scaffolding for certified CPT membership decisions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.