← Lebesgue 萬有覆蓋問題 / Round 18 · 生產分片檢查點
Round 18（AMRAL-LUC-FC-R18，2026-09-19）把 Round 17 留下的兩層 proof stack——theorem-critical 的 D₃ canonical wedge，與 performance-only 的 Official default split／Tail-Window CPG override——落實成一個可保存、可獨立 replay 的 production-style shard checkpoint format，並在 seed depth 3（S=2³=8 個 shard root，每個 shard 獨立跑到 global depth 16）的固定切分下，回答 topology 編碼（preorder tree、每 node 1 bit）、leaf tag 編碼（2 bit 區分 00=SYM／01=CERT／10=PENDING／11=RESERVED）、非 default split axis 如何 sparse encode、verifier 是否需要重跑 CPG、Tail-Window 多花的 emitter cost 何時能回收，以及 checkpoint 能否真正獨立 replay 等六個介面問題。SYM 不是面積下界，而是 y₃,min>√3·x₃,max 這條 root-domain quotient 幾何條件本身，由 verifier 直接重算，不算 search heuristic；CERT 則由 independent verifier 不信任 emitter 的 T_search=0.8350002 pruning buffer，改對 current proof target 0.835 重新獨立算 APR／REP／CORE 三條 one-sided route，任一成功即接受；PENDING 只能出現在 depth 16，且只要 PENDING>0 就令 theorem_ready=false。佔多數的 default split axis（MISHRA-FIRST-ORDER，取 h_x3、h_y3、R5·h_φ5、h_x5、h_y5 中最大者）不必寫入 certificate，由 verifier 自行重建，只有約一成的非 default override 才需編碼——本輪捨棄逐 internal node 存一個 override flag（仍是 O(N_internal)）的作法，改用 event coding：每個 override 只記距上一個 override index 的 gap（以 Rice 參數 k∈{0,…,6} 編碼，g_j=2^k·q_j+r_j，unary 商加 k-bit 餘數，每個 shard 自選最短 k）與 2-bit 的非 default axis rank；verifier 端則明文定義為不重現 CPG——不需 b3=0.025、啟用深度 10、child scoring、tie-break 或 expected prune model，只讀 implicit default split、override event 給的 explicit axis，以及 midpoint children 是否覆蓋 parent，即「scheduler intelligence 不屬於 proof premise」。實測上，Official production checkpoint 為 N_O=12350、L_O=6179（SYM 109、CERT 3304、PENDING 2766，3304 個 CERT 全數由 verifier 以 CORE route 重證）；Tail-Window production checkpoint 為 N_T=10086、L_T=5047（SYM 106、CERT 2893、PENDING 2048，同樣全數 CORE 重證），573 個 override event、4983 個 internal node，override 密度 11.37%，相對 Official 節點數減少 18.33%、PENDING 減少 25.96%（即少 718 個下一階段 continuation obligation）。若逐 internal node 明寫 3-bit axis 需 15117 bit，Rice-coded sparse override 實際只需 3823 bit（佔 25.29%）；原始 binary stream 上 Official 為 3094 bytes、Tail+Rice 為 3011 bytes（小 2.68%）——但若只把各 stream 直接串接後跑 zlib-9，Tail（1782 bytes）反而比 Official（1660 bytes）大 7.35%（override event entropy 較高），完整 shard 目錄（manifest、pending path、stream 全部算入）的實際 ZIP 卻是 Official 25045 bytes、Tail 22263 bytes，Tail 反而小 11.11%，主因是節點數少、pending frontier 短、manifest／path 資料也少。independent verifier 只用手寫 monotone-chain hull 加 shoelace 面積與獨立 stream parser 重播，不用 SciPy ConvexHull、CPG 分數／gate 或 emitter 的 split-choice 邏輯，Official replay 2.3140s、Tail replay 1.9887s，快 14.06%；兩者最差 accepted CERT slack 分別為 6.15×10⁻⁶ 與 1.14×10⁻⁵、均為正，但本輪仍用 pilot 級 FP_PAD=10⁻⁹，未升格為 publication-grade 浮點定理。相對地，emitter 成本上 Tail（E_T≈17.32s）比 Official（E_O≈6.98s）慢約 2.48 倍，這是稀疏 lookahead 換樹縮小的直接代價。為此本輪把排程目標從單純的一次性 E，換成 lifetime cost model C=E+RV+κP+μB（E 為一次 emit 成本、V 為一次 independent replay 成本、R 為預期 replay／audit 次數、P 為 pending leaves、κ 為每個 pending obligation 的未來 continuation 成本、B 為 artifact bytes、μ 為 storage/network 權重）：取 κ=μ=0 的 replay-only break-even 解得 R*≈31.79，即「emit 一次、驗一次就丟掉」時 Official 較省；取 R=μ=0 的 continuation-aware break-even 則解得 κ>0.0144s（約 14.4 ms）／pending leaf，即只要每個被 Tail 省掉的 pending leaf 未來平均需要超過約 14.4 ms 的 continuation work，Tail 在此 pilot 的長期成本就已回本——本輪明言這只是 empirical break-even，不是數學 theorem。工程結論因此是：long-running checkpoint 首選 Tail-Window、one-shot emitter benchmark 首選 Official，排程器不再有單一靜態贏家，真正目標是 min E[lifetime proof cost]，而非單純 min 節點數或 max 剪枝。本輪另外記錄一個 proof-mode audit：depth-16 accepted 的 CERT leaves（Official 3304、Tail 2893）全數只靠 CORE route 關閉，APR／REP 在這批 leaf 上並未派上用場，此觀察留給 Round 19 的 lazy proof-mode evaluation 使用。8 個 shard 目前全部仍有 PENDING，shard status 因此是 EXPANDED 而非 COMPLETE，但其 pending leaf path 已直接輸出，可餵給既有的 checkpoint／scheduler／capacity planner；本輪產出的是「certified leaves + explicit pending frontier」的機器可驗證 checkpoint 而非 search log，沒有 hidden abandoned branch，中止於 depth 16 不破壞 coverage。距真正 final 0.8350 certificate 仍缺：封閉全部 PENDING frontier、把 pilot FP policy 換成 publication-grade 算術定理、必要時的 B7／fallback witness、final A1 replay，以及 global theorem-ready merge 共五項——但 checkpoint 格式本身已不再是 blocker。Round 18 狀態總表：production shard grammar CLOSED、D₃ root replay VERIFIED、Rice-coded sparse override IMPLEMENTED + VERIFIED、Official／Tail-Window checkpoint replay 均 PASS、pending frontier preservation PASS、lifetime cost model FORMALIZED + EMPIRICALLY CALIBRATED，final 0.8350 theorem 則仍是 COMPUTE-DEFERRED。全局界 a_Leb≥0.835 本輪未獲證，也未被本輪動搖。研究方向與方法論來源為 Neo.K；本輪 AI 協力研究者與主要執行者為 Aletheia / ChatGPT, GPT-5.6 Sol。
載入中…