pipeline_nonzero_sound
plain-language theorem explainer
Nonzero-decision soundness for the composed CPT pipeline certifier Φ* = A∘B∘P. If every input tagged nonzero is already marked excluded, that implication is recorded as a theorem. Cited by the CPT exports bundle and by anyone assembling certified membership checks. Proof is a pure identity: the conclusion is exactly the supplied hypothesis.
Claim. Let $P:X\to Y$ be a projection stage, $B:Y\to Z$ a coercivity stage, and $A:Z\to\{\mathrm{zero},\mathrm{nonzero}\}$ an aggregation stage, and write $\Phi^*=A\circ B\circ P$. Given a predicate $\mathrm{excluded}$ on $X$, if $\Phi^*(x)=\mathrm{nonzero}$ implies $\mathrm{excluded}(x)$ for every $x\in X$, then the same implication holds for every $x\in X$.
background
The CPT pipeline module fixes a three-stage composition shape used for certified membership checks: projection/neutrality preprocessing $P$, coercivity conversion $B$, and aggregation/decision $A$. Each stage is a structure carrying a single map (run). The composed certifier is defined by $\Phi^*(x)=A(B(P(x)))$ and lands in a two-valued decision tag (zero vs nonzero).
The module's stated goals are definitional factorization $\Phi^=A\circ B\circ P$, zero/nonzero soundness under explicit assumptions, and procedure-space membership for $\Phi^$ once soundness and a finite-data predicate are in hand. The present result is the nonzero half of that soundness interface: it packages the assumption that a nonzero tag forces the input into an excluded class.
Sibling material includes the dual zero-soundness statement and the procedure-space bundling theorem that consumes both.
proof idea
Term-mode identity proof. Introduce an arbitrary input $x$ and a hypothesis that $\Phi^*$ tags it nonzero; discharge by applying the given nonzero-soundness assumption at that same $x$. No lemmas are invoked; the conclusion is definitionally the hypothesis.
why it matters
Records nonzero-decision soundness for the composed CPT pipeline so the export layer can re-export a stable name (CPT_PIPELINE_nonzero_sound) without depending on local stage binders. Downstream, that export is the public handle for "nonzero tag implies excluded" when assembling certified CPT checks.
Together with factorization and the zero-soundness twin, it fills the module's soundness bullet: zero/nonzero soundness under explicit assumptions. It does not itself derive exclusion from physics; it freezes the logical shape that later stages (procedure-space membership, window identifiability) rely on when they treat $\Phi^*$ as a certified decision procedure.
In the broader Recognition verification stack this is bookkeeping, not a forcing-chain step: it keeps the $P\to B\to A$ interface honest so certified claims about nonzero decisions stay auditable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.