CoercivityStage
plain-language theorem explainer
The middle stage of the CPT pipeline is a pure map from an intermediate type Y to a decision-ready type Z, encoding coercive conversion between projection and aggregation. Anyone citing the certified factorization of the composed procedure, or the zero/nonzero soundness and domination theorems, packages that stage through this type. It is a one-field structure definition with no proof obligations.
Claim. A coercivity stage from type $Y$ to type $Z$ is a map $B:Y\to Z$ (the $B$ stage of the CPT composition $P\to B\to A$).
background
The CPT verification module formalizes a certified three-stage composition shape: projection/neutrality pre-processing ($P$), coercivity conversion ($B$), and aggregation/decision ($A$). The composed procedure is definitionally $A\circ B\circ P$.
This declaration is the type of the middle stage alone. It carries only a single field, the conversion map from the post-projection intermediate type $Y$ into the pre-aggregation type $Z$. No numerical constants, gap factors, or ledger normalizers are fixed here; those live in other modules and are not part of the stage interface.
Sibling stage types play the same role for $P$ and $A$. Downstream theorems quantify over all three stages and prove factorization, soundness, and optimality for the composed map.
proof idea
No proof. This is a structure definition: a single field run of type $Y\to Z$. There are no axioms, no tactics, and no lemmas applied. Instantiation is by supplying any function of that type.
why it matters
This stage type is the $B$ slot in every certified CPT pipeline theorem. Downstream exports use it for definitional factorization (paper §5: the composed procedure equals $A\circ B\circ P$), zero- and nonzero-decision soundness of the composition, and the optimality claims that the composed procedure dominates any agreeing procedure on a class (paper Thm. 6.11), including the global-class specialization.
It also appears in the Optimality module as a parameter of the composed procedure abbreviation and of the domination lemmas. Without a typed $B$ stage, the pipeline cannot be stated as a uniform composition, and the soundness/optimality chain has nothing to quantify over for the coercive conversion step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.