ProcedureSpace
plain-language theorem explainer
A procedure-space element is a ternary decision map that is sound for a zero/nonzero partition and satisfies an abstract finite-data predicate. Optimality and pipeline theorems cite this package to state that a candidate classifier lives in the admissible class. The declaration is a two-field Prop structure bundling soundness with finite data; there is no proof body.
Claim. Fix a type $X$, predicates $\mathrm{isZero},\mathrm{isNonzero}:X\to\mathrm{Prop}$, and a finite-data predicate $F$ on procedures $X\to\{\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}\}$. A procedure $\Phi$ lies in the procedure space when (i) $\Phi(x)=\mathrm{zero}$ implies $\mathrm{isZero}(x)$ and $\Phi(x)=\mathrm{nonzero}$ implies $\mathrm{isNonzero}(x)$, and (ii) $F(\Phi)$ holds.
background
The CPT verification core supplies small reusable interfaces for claim-honest statements across WindowIdentifiability, Pipeline, Optimality, and ForcedFactorization. A procedure on inputs of type $X$ is a map to a ternary decision tag: zero, nonzero, or inconclusive. The resolved set is the subset of inputs that are not inconclusive.
Soundness for such a ternary map means the zero tag only fires on inputs satisfying $\mathrm{isZero}$, and the nonzero tag only on $\mathrm{isNonzero}$. Inconclusive answers carry no certificate. The finite-data predicate is left abstract so downstream stages can plug in whatever resource bound (window size, bit budget, stage complexity) the pipeline needs.
This package sits above the CPM Law-of-Existence bridge wrappers in the same module and is the ambient class in which optimality compares candidate procedures.
proof idea
Definition only: a Prop-valued structure with two fields. The first field is an instance of the soundness structure (zero-sound and nonzero-sound implications). The second is a single hypothesis that the abstract finite-data predicate holds of $\Phi$. No tactics or lemmas are invoked; inhabitants are built by supplying those two proofs at use sites.
why it matters
Procedure space is the ambient class for CPT optimality. Both Pipeline and Optimality prove that the composed classifier $\Phi^*$ (projection, then coercivity, then aggregation) inhabits this space once soundness and finite-data hypotheses are given. Downstream doc-comment: "Bundle PhiStar as a procedure-space element under explicit finite-data and soundness hypotheses."
That membership lets optimality theorems compare $\Phi^*$ against any other sound finite-data procedure without restating the two constraints inline. It keeps the CPT formalization claim-honest: domination and uniqueness statements quantify over this package rather than over raw maps. No forcing-chain landmark (T5–T8) is discharged here; the structure is verification scaffolding for the CPT pipeline, not a physics derivation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.