CCM Formal Core

The document opens by stating its own position: ‘extracts the minimal formal core of the Computational Composite Methodology from the longer foundational paper.’ 20 numbered definitions build up in sequence: target and external truth semantics $\tau$, the certificate-language sextuple $\mathcal C=(D,\Gamma,A,V,\sigma,K)$, positive/negative/total coverage, the unresolved region $U(\mathfrak C;\Omega)$, method obstruction (which does not directly decide $P$ or $\neg P$), certificate-preserving representation morphisms, final-routing three-state semantics ($\mathrm{PROVED}/\mathrm{DISPROVED}/\mathrm{UNRESOLVED}$), the research-state twelve-tuple $\mathcal S_t$, the state operator, cost vectors, marginal coverage gain, routing gain, routing regret, online routing and online updates, dynamic regret, switching delay, and the CCM performance-state sextuple $\mathcal G_t$. The corresponding 6 numbered theorems/propositions/corollaries compress the long paper's core results into their most minimal statements: Theorem 1 (coverage monotonicity), Corollary 1 (unresolved-region anti-monotonicity), Proposition 2 (method failure ≠ falsity), Theorem 3 (representation-morphism composition closure), Theorem 4 (verification firewall — as long as the final verifier is sound and representation transformations preserve certificate semantics, routing remains rigorous however it is chosen), Proposition 5 (nonnegative-defect decomposition: $G=\sum_\alpha\lambda_\alpha D_\alpha$ with $\lambda_\alpha,D_\alpha\ge0$ implies $G\ge0$), Proposition 6 (coverage and cost are independent axes). The document closes with two boxed lines compressing the whole theory into two sentences: ‘truth ≠ coverage ≠ search success ≠ verification ≠ cost,’ and ‘heuristic search may propose; only verified certificates may close.’