Pith. sign in
module module high

IndisputableMonolith.Verification.CPT.Exports

show as:
view Lean formalization →

Export barrel for the CPT verification stack: window identifiability, the P→B→A pipeline, class-restricted optimality of PhiStar, forced factorization, and rank/epsilon certification. Anyone citing the CPT formalization layer imports this module rather than the seven leaf files. No new theorems live here; it is a pure re-export surface over Core, WindowIdentifiability, Pipeline, Optimality, ForcedFactorization, RankCertification, and EpsilonCertification.

claimRe-export surface for the CPT stack: window identifiability (identifiable iff trivial kernel / full column rank), the certified pipeline $P \to B \to A$, class-restricted domination of $\Phi^\star$, forced factorization of the cost, general $(d,W)$ rank certification, and the $\varepsilon$-noise ranking layer.

background

CPT (Certified Procedure Theory) is the verification layer that turns Recognition-style cost and measurement claims into Lean-checkable procedure statements. Core supplies the shared vocabulary: decision tags (zero / nonzero / inconclusive), procedure and resolved-set utilities, a class-restricted domination relation, and thin wrappers around the CPM A/B/C closure theorems.

Window identifiability links observability of a windowed measurement map to linear-algebraic conditions (trivial kernel, full column rank). Rank certification closes the general $(d,W)$ gap: for every $d \ge 1$ and $W \ge 1$ there is a parameter witness at which the window-measurement Hankel matrix has nonzero determinant, so the identifiability locus $\Omega_{d,W}$ is nonempty (hence Zariski-open dense). The pipeline module packages the certified composition $P \to B \to A$ (projection/neutrality, coercivity conversion, aggregation/decision).

Optimality proves class-restricted domination for $\Phi^\star$ when a competitor $\Psi$ resolves every input in the class and agrees with $\Phi^\star$ there. Forced factorization states the strongest currently defensible Lean shape of the paper's factorization claims (ratio-induced canonical cost, explicit certificate hypotheses, existence of a reparametrization on the realized cost image). Epsilon certification handles the noise layer: perturbation bound $|\hat c - c| \le \varepsilon$, minimizer transfer, and an explicit $2\varepsilon$-suboptimality guarantee.

proof idea

This is an export module, not a proof module. It imports the seven CPT leaf modules and re-exports their public interfaces so downstream code can depend on a single surface. No lemmas are proved here; argument structure lives in the imported files (identifiability equivalences, pipeline soundness, PhiStar domination, forced-factorization existence/uniqueness, rank witnesses, epsilon transfer).

why it matters in Recognition Science

Feeds the Verification.CPT umbrella, which is the single entry point for the whole CPT formalization (core interfaces, window identifiability, $P \to B \to A$ pipeline, class-restricted domination/optimality, forced factorization, rank and epsilon layers). Sibling exports include the paper-facing names: identifiability iff trivial kernel / full column rank (paper Thm. 6.5), zero-detection from identifiability, pipeline factorization and soundness, PhiStar domination (local and global), and forced-factorization existence/uniqueness with state-independent reparametrization. Without this barrel, every consumer would pin seven import paths; with it, the CPT stack is one stable dependency for higher verification and paper-claim audits.

scope and limits

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (18)