IndisputableMonolith.Verification.CPT
Public entry module for the CPT verification layer in Recognition Science. It re-exports the citation-friendly theorem surface for window identifiability and the P→B→A composition pipeline. Auditors cite it when mapping paper Theorems 4.5/6.5 and §§5–6 to Lean. The module itself is a thin import shell with no local proofs.
claimRe-export surface for the CPT formalization: the window-identifiability family $\mathrm{WINDOW}_*$ (paper Thm.\ 4.5 / 6.5) and the composed pipeline theorems $\mathrm{CPT\_PIPELINE}_*$ (paper P$\to$B$\to$A, §§5–6), all fully proved with no axioms or sorries.
background
Recognition Science treats CPT-side claims as a verification layer over the forcing chain and the Recognition Composition Law. The concrete theorems live one level down in Verification.CPT.Exports, which packages proved aliases for two paper families: window identifiability ($\mathrm{WINDOW}*$, Thm.\ 4.5 / 6.5) and the P→B→A pipeline composition ($\mathrm{CPT_PIPELINE}*$, §§5–6).
This module is the stable import path for that export surface. It does not introduce new definitions, cost functionals, or ladder arithmetic; it only exposes the already-proved CPT layer so downstream verification and paper-mapping code can depend on a single short name.
proof idea
This is a module shell, not a theorem. Its entire content is a single import of IndisputableMonolith.Verification.CPT.Exports. All mathematical work (window identifiability and pipeline composition) is discharged in the export layer and its dependencies; nothing is proved or axiomatized here.
why it matters in Recognition Science
Gives a single citation handle for the CPT verification package inside the Recognition monolith. Downstream consumers that need paper Thm.\ 4.5/6.5 window results or the §5/§6 P→B→A pipeline should import this module rather than deep paths. The upstream export doc states that every re-exported item is fully proved (no sorry, no new axiom), so this facade preserves a clean claim status for the CPT layer. No further parent theorems are listed as direct used_by edges from this module itself.
scope and limits
- Does not prove any CPT theorem locally; all content is re-exported.
- Does not define window predicates, pipeline maps, or cost functionals.
- Does not extend the forcing chain (T0–T8) or alter RCL/J-uniqueness.
- Does not claim new numerical bounds on alpha, masses, or dimensions.