工程驗證軌跡:七角色對抗式驗證,v0.2 → v0.2.6

CLOSURE-OPAQUE-LEAF-TERMINAL-01(AI-3)——候選的規範判斷圖裡,OpaqueLeaf 是 SupportedTraversal.child_dispatch 的一個目標分支,但沒有定義它該映射到 PASS/FAIL/UNKNOWN 哪一個終態。這不是假設性問題:AI-3 在凍結測資裡找到一條真的會走到這個分支的資料,而可執行的驗證程式在此把它當 PASS 繼續執行——是「規範圖」與「實際執行」之間的介面缺口,不是 admission bypass、正確性反例,或 P/NP 結論。這其實是修好上一輪(v0.2.5)的 CLOSURE-SUPPORTED-RELATION-RESULT-01 之後,判斷圖第一次真正走到下一節點,才第一次暴露出來的下一層缺口。

ACCEPTANCE-PACKET-IMPORT-EDGE-COUNT-01(AI-5)——候選封裝裡 CURRENT-v0.2.6-candidate.md 寫「29 條 local import edges」,但同一封裝內的 machine descriptor、官方 self-check、VALIDATION-REPORT-v0.2.6-candidate.md,以及 AI-5 自己獨立用 AST 重新算出的結果全部是 31 條。單純的文件計數不一致,不是正確性錯誤,但依流程規則仍構成 promotion blocker。

「這不是一份失敗的 P/NP 證明;它目前也不是 P/NP 證明。」——AI-6,首輪盲讀。第二輪覆審維持原判:研究綱領可以繼續、比第一輪成熟,但作為 P/NP characterization theorem 投稿,「至少是 major revision」;作為已證明 P=NP、P≠NP 或已建立新複雜度類的材料,「不成立」。

「不能把工程閉合升格成數學閉合。」——AI-7,跨範式橋接報告。第二輪逐條核對 AI-6 的判斷是否被後續工程與形式化進展推翻,結論是沒有:「每一項結果只可向上移動一層……不能由多個工程綠燈的數量直接跨到 P/NP conclusion。」

兩人都特別提醒:目前沒有任何已知複雜度障礙(relativization 等)被實際碰觸過;Lean 端雖然編譯乾淨,但 zeroDebt 這類引理可能被空洞代入而失去意義,不宜過度解讀「編譯成功」本身的份量;GLC 的「robust」語義目前只在單一 deterministic run 上測過,不等於已驗證一般容錯/非決定性語義。

v0.2 到 v0.2.6 共 7 個版本標籤,至少 12 個互不相同命名的 blocker ID(PROV-DERIVE-01、REF-TYPE-01、CLOSURE-CLASS-01、CLOSURE-EDGE-SCOPE-01、ORACLE-DECL-FAMILY-01、CLOSURE-JUDGMENT-COMPLETENESS-01、ADVICE-DECL-LEDGER-01,加上 v0.2.5、v0.2.6 各自的新 blocker),無一重複命名。v0.2.3 曾一度標記 PASS,隨後被 ADDENDUM 更正為 FAIL。整體讀起來像是逐輪修掉舊缺口、審查深度也逐輪加深後再挖出新缺口的持續 hardening 過程,而不是同一缺陷反覆出現,也不是驗證方對工程方照單全收。