SoundProcedure
plain-language theorem explainer
Soundness for a ternary CPT procedure: a zero tag may issue only on inputs satisfying isZero, and a nonzero tag only on inputs satisfying isNonzero. Inconclusive outputs are unconstrained. Optimality and domination arguments cite this as the honesty side of a procedure-space package. It is a pure Prop structure with two universal implications; no proof body.
Claim. Fix a type $X$, predicates $\mathrm{isZero},\mathrm{isNonzero}:X\to\mathrm{Prop}$, and a procedure $\Phi:X\to\{\mathrm{zero},\mathrm{nonzero},\mathrm{inconclusive}\}$. Soundness means: $\Phi(x)=\mathrm{zero}$ implies $\mathrm{isZero}(x)$, and $\Phi(x)=\mathrm{nonzero}$ implies $\mathrm{isNonzero}(x)$.
background
The CPT verification core supplies small reusable interfaces so claim statements stay honest across WindowIdentifiability, Pipeline, Optimality, and ForcedFactorization. A decision tag is ternary: zero, nonzero, or inconclusive. A procedure on $X$ is simply a map $X\to$ decision tag.
Soundness is the one-way certification rule for the two decisive tags. Zero may be emitted only when the input really meets the zero predicate; nonzero only when it meets the nonzero predicate. Inconclusive is free: it neither asserts nor denies either class. The predicates themselves are parameters (e.g. structural zero tests from the primitive recognition calculus), so the same interface covers many concrete zero/nonzero splits.
Upstream, the module sits next to CPM Law-of-Existence imports and lightweight A/B/C closure wrappers; this structure does not invoke those closures, it only packages the honesty side of a procedure.
proof idea
Definitional structure, not a proved theorem. The body is two fields of type Prop: universal implications from the procedure's decisive outputs to the corresponding predicates. No tactics, no lemmas, no sorry. Instantiation is by supplying those two implications (or by constructing a larger ProcedureSpace that embeds this structure as its sound field).
why it matters
ProcedureSpace packages soundness together with an abstract finite-data predicate and is the object optimality theorems quantify over. Without this structure, domination and resolved-set comparisons would have no claim-honest notion of a procedure that never lies on decisive tags.
In the broader Recognition verification stack, CPT-style procedures are the discrete decision layer used to state identification and factorization results cleanly. The ternary tag (including inconclusive) matches the need for partial resolution under finite data, while soundness keeps every zero/nonzero certificate tied to the mathematical predicates under study. This is scaffolding for composable optimality, not a physics forcing step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.