Procedure
plain-language theorem explainer
A CPT procedure is any map from inputs of type X to a ternary decision tag (zero, nonzero, or inconclusive). It is the basic object of the CPT verification layer: resolved sets, domination, soundness, and procedure spaces are all defined on this type. Anyone stating optimality or domination theorems (e.g. PhiStar dominates) cites it as the ambient type of competing classifiers. The declaration is a one-line type synonym.
Claim. A CPT procedure on a type $X$ is a function $\Phi : X \to \{\mathrm{zero},\,\mathrm{nonzero},\,\mathrm{inconclusive}\}$.
background
The CPT verification core supplies small reusable interfaces for claim-honest statements about ternary classifiers. The decision alphabet is the inductive type with constructors zero, nonzero, and inconclusive: zero and nonzero are definitive answers; inconclusive means the procedure declines to decide.
A procedure is simply a function from an arbitrary input type $X$ into that alphabet. Downstream utilities build on this: the resolved set is the set of inputs not tagged inconclusive; class-restricted resolved sets and domination compare two procedures on a subset $C \subseteq X$; soundness requires that zero (resp. nonzero) only fire when a given predicate isZero (resp. isNonzero) holds.
The module imports the CPM Law of Existence and Mathlib, and is meant to stay composable across WindowIdentifiability, Pipeline, Optimality, and ForcedFactorization.
proof idea
One-line type abbreviation: Procedure X is defined to be the function type X → DecisionTag. No proof obligations; DecidableEq and Repr on DecisionTag are inherited by clients that pattern-match on tags.
why it matters
Every subsequent CPT interface is typed over this synonym: resolvedSet, resolvedSetOn, dominatesOn, SoundProcedure, and ProcedureSpace all take Procedure X arguments. Optimality exports such as CPT_OPT_phiStar_dominates and CPT_OPT_phiStar_dominates_global quantify over competing procedures Ψ : Procedure X and assert that the distinguished PhiStar procedure dominates them on a class. The abbreviation keeps theorem statements short and claim-honest while fixing the ternary decision model used throughout the verification stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.