IndisputableMonolith.Verification.CPT.Optimality
Defines class resolution for CPT decision procedures and a distinguished procedure PhiStar that lies in the admissible space, resolves every nondegenerate class, and dominates competitors classwise and globally. Cited by anyone proving uniqueness or optimality of the CPT pipeline. Arguments assemble Core resolution/domination interfaces with the certified P→B→A composition.
claimA procedure $Q$ resolves a class $C$ if it never returns inconclusive on points of $C$. There is a distinguished procedure $\Phi^*$ in the admissible procedure space such that $\Phi^*$ resolves every nondegenerate class and dominates every competing procedure both on each class and globally.
background
CPT verification treats decision procedures that tag each input as zero, nonzero, or inconclusive. Core supplies the reusable interfaces: decision tags, procedure and resolved-set utilities, and a class-restricted domination relation, plus thin wrappers around the CPM A/B/C closure theorems.
Pipeline formalizes the certified composition shape $P \to B \to A$: projection/neutrality pre-processing, coercivity conversion, then aggregation/decision. Optimality sits on top of those two layers. It asks which procedures fully resolve a class (never inconclusive on that class) and whether a single canonical procedure dominates the rest.
Sibling objects name that canonical choice $\Phi^$, the predicate that a procedure resolves a class, membership of $\Phi^$ in the procedure space, resolution of nondegenerate instances, and both classwise and global domination statements.
proof idea
Not a single theorem: a small cluster of definitions and proved lemmas. Resolution is the never-inconclusive predicate on a class. PhiStar is introduced as the distinguished procedure; membership in the procedure space and resolution of nondegenerate classes are recorded as separate facts. Domination lemmas compare PhiStar to arbitrary competitors, first restricted to a class, then lifted to a global statement, reusing Core's class-restricted domination relation and the Pipeline composition shape rather than re-proving A/B/C closure.
why it matters in Recognition Science
Closes the optimality half of the CPT formalization: once the pipeline can decide, one wants a canonical procedure that resolves nondegenerate classes and dominates alternatives. Downstream, Verification.CPT.Exports re-exports citation-friendly aliases for the whole CPT layer (WINDOW_* from paper Thm. 4.5/6.5, CPT_PIPELINE_* from the §5/§6 P→B→A composition), all fully proved with no sorry and no new axioms. This module supplies the resolution and domination facts those export aliases package for paper-to-Lean mapping.
scope and limits
- Does not define the P, B, or A stages; those live in Pipeline.
- Does not prove window identifiability (WINDOW_*); only optimality/resolution facts.
- Does not introduce new axioms or sorry-bearing stubs in the export surface.
- Does not claim PhiStar is the unique optimizer beyond the stated domination lemmas.
- Does not address physical constants, mass ladders, or forcing-chain landmarks T0–T8.