CCM Formal Core

文件開頭自陳定位:「從較長的基礎論文萃取出 Computational Composite Methodology 的最小形式核心。」20 個編號定義依序建立:目標與外部真理語意 $\tau$、證書語言六元組 $\mathcal C=(D,\Gamma,A,V,\sigma,K)$、正/負/總覆蓋、未解區 $U(\mathfrak C;\Omega)$、方法障礙(不直接判定 $P$ 或 $\neg P$)、證書保持的表示態射、終局路由三態語意($\mathrm{PROVED}/\mathrm{DISPROVED}/\mathrm{UNRESOLVED}$)、研究狀態十二元組 $\mathcal S_t$、狀態算子、成本向量、邊際覆蓋增益、路由增益、路由後悔、線上路由與線上更新、動態後悔、切換延遲、CCM 表現狀態六元組 $\mathcal G_t$。對應的 6 個編號定理/命題/推論把長論文的核心結果壓縮成最精簡的陳述:Theorem 1(覆蓋單調性)、Corollary 1(未解區反單調性)、Proposition 2(方法失敗不等於為假)、Theorem 3(表示態射組合封閉)、Theorem 4(驗證防火牆——只要終局驗證器健全且表示轉換保持證書語義,路由無論怎麼選都嚴謹)、Proposition 5(非負缺陷分解:$G=\sum_\alpha\lambda_\alpha D_\alpha$ 且 $\lambda_\alpha,D_\alpha\ge0$ 則 $G\ge0$)、Proposition 6(覆蓋與成本是獨立座標軸)。文件收尾用兩個方框把整套理論壓成兩句話:「真理≠覆蓋≠搜尋成功≠驗證≠成本」,以及「啟發式搜尋可以提議;已驗證的證書才能封頂」。