CDIR v0.3 與可機器檢查的合流證書：把正典性拆成由核心自行枚舉的有限義務

Run 129 把 canonicality="certified" 改成 fail-closed——CDIR v0.2 沒有可機器檢查的合流證書模型，兩個 v0.2 驗證器都被迫拒絕該宣稱；Run 130 為一個刻意受限但真實的 profile 補上這個缺口，發佈 CDIR v0.3 與證書 profile finite_state_critical_pairs_v0.1。證明物件是 CanProof=(P, S₀, 𝒮, ℰ, ℱ, τ)：profile 識別碼、初始狀態、有限狀態集、有限轉移集、臨界分叉的匯合證書，以及嵌入該有限模型的選定軌跡；狀態形如 s=(id, Δ_s, r_s)，帶有限債務集與自然數階數。本輪的核心設計是覆蓋率由核心計算而非由產生者宣告：kernel 自行枚舉每個狀態全部外向轉移的無序配對 Pairs_kernel，並要求 Pairs_package 與之完全相等（漏掉與重複的分叉證書都被拒絕），圖上每條邊都必須攜帶證書（graph edge ≠ trusted transition），每個宣告狀態都必須自 S₀ 可達，匯合的左右兩條路徑必須落在完全相同的有限狀態，選定軌跡則必須與 rule_steps 對應並重現封包重放狀態。終止性由每步 r_t

Run 130 發佈 RCIG_CDIR_v0.3.schema.json 與 finite_state_critical_pairs_v0.1 證書 profile，把正典性從一個字串欄位改成六項可有限重放的義務（d_state、d_edge、d_term、d_cover、d_join、d_trace），其中臨界配對的覆蓋範圍由核心自行枚舉並要求與封包宣告逐一相等，終止性則由 ℕ 上的嚴格階下降取得而不需外部序數證明器。本輪自陳這不是通用解，只是「一個能把整個正典性論證完整重放一遍的小領域」：第一個 profile 是 package-local 的有限宣告改寫宇宙，採恆等語義等價（要求所有可達正規形具有完全相同的債務集，而非 Run 119 的商合流），明言並未主張已枚舉所有數學上可想像的證明，正典性仍相對於任務與封包改寫宇宙、不被提升為絕對數學真理，核心新信任的原始定理「實作必須仍被稽核」；而第一個真正被接受的 canonicality="certified" 在本輪仍只是前沿項目 QL，實際發生於下一輪 Run 131 的 K3 Canonical Kernel v0.3。

連接 · Connections

上一篇Run 129 · 合法非匯流 · 軌跡健全不等於全域匯流：第一個可執行的非匯流反例與 canonicality 失敗即關閉

下一篇Run 150 · 策略量詞 IR · 策略量詞 IR：把 max/min、公平性過濾器與策略域從一堆專用核心壓縮成單一 AST 語言

載入中…