Pith. sign in
module module moderate

IndisputableMonolith.Verification.CPT.Core

show as:
view Lean formalization →

Core vocabulary for CPT verification: ternary decision tags, procedures as input-to-decision maps, resolved sets, classwise domination, sound procedures, and A/B stage interfaces tied to the coercive projection method. Cited by anyone using window identifiability, the P→B→A pipeline, or PhiStar optimality. Purely definitional over Law of Existence A/B/C; no standalone theorems live here.

claimIntroduces ternary tags $D\in\{\mathrm{accept},\mathrm{reject},\mathrm{undecided}\}$, procedures $\Psi$ mapping inputs to $D$, the resolved set where $\Psi$ is decisive, domination $\Phi\succeq_S\Psi$ on a class $S$, sound procedures, a procedure space, and stage interfaces for forward/reverse coercivity (B-stage) and aggregation (A-stage) used by CPT pipelines.

background

CPT builds on the Coercive Projection Method formalized in Law of Existence as three domain-agnostic pieces: A (projection-defect inequality), B (coercivity factorization: an energy gap controls defect), and C (aggregation: local tests imply membership). This module supplies the decision-theoretic language layered on that factorization.

A procedure maps a measurement or certificate space into a ternary tag. The resolved set is the locus where the tag is not undecided. Domination on a class means one procedure agrees with another wherever the latter resolves, so optimality can be stated classwise without global uniqueness. Soundness packages correctness of accept/reject tags relative to a target predicate.

B-stage interfaces encode forward and reverse coercivity conversion; the A-stage interface encodes aggregation of local tests into a global decision. These are the typed hooks that Pipeline, Optimality, and ForcedFactorization instantiate.

proof idea

Definition module only. It declares DecisionTag, Procedure, resolved-set operators, domination on a class, SoundProcedure, ProcedureSpace, and the named A/B stage predicates (forward/reverse coercivity, aggregation). No free-standing proof obligation at module scope; downstream modules discharge concrete instances of these interfaces against the CPM A/B/C lemmas.

why it matters in Recognition Science

Every CPT verification submodule imports Core. Exports re-exports citation aliases for window identifiability (paper Thm. 4.5/6.5) and the P→B→A pipeline. Pipeline composes projection/neutrality (P), coercivity conversion (B), and aggregation (A) on the stage interfaces defined here. Optimality proves class-restricted domination for PhiStar once Psi resolves the class and the two agree on it. ForcedFactorization states certificate hypotheses and reparametrizations on the realized cost image in this vocabulary. RankCertification and WindowIdentifiability reuse the same decision and resolution language for Hankel-rank and injective reconstruction. Without Core, the CPT layer has no shared types for procedures or stage contracts.

scope and limits

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)