空間域證明包圍論 VIII

Runtime、Benchmark 與 Proof-Space Observatory

Spatial-Domain Proof Enclosure VIII: Runtime Semantics, Benchmarks, and a Proof-Space Observatory

Version: v0.1
Date: 2026-08-14
Status: Phase-I integration paper / executable reference architecture; not a complete proof assistant and not a claim of universal proof-search acceleration
Canonical source: UTF-8 Markdown; canonical mathematics uses $...$ and $$...$$ only.

摘要

前七篇空間域證明包圍論依序建立：sound survivor contraction、route representation faithfulness、global coverage / closure certificates、proof-trace compilation、Discovery–Verification cost dynamics、measure-zero exceptional-core analysis，以及 cost-aware enclosure routing。這些結果共同提出一個新的工程問題：若研究真的被視為一個持續收縮、可回滾、可重播的 counterexample survivor process，那麼其正式 runtime 狀態、authority boundaries、event history、benchmark semantics 與 observability contract 應如何設計？

本文給出 SDPE Phase I 的第一個整合 runtime。其 canonical state 為

\boxed{ \mathbb S_t = \langle \Omega_t, RouteCert_t, \mathbf G_t, GCC_t, \mathcal H_t, Compiled_t, DVI_t, SurvProf_t, RouteDecision_t, Env_t \rangle. }

本文採用 append-only event ledger 與 deterministic reducer。令

\mathcal L_t=(e_0,e_1,\ldots,e_t)

為事件序列，則 authoritative state 由

\boxed{ \mathbb S_t = \operatorname{Fold}(\mathcal R,\mathbb S_{-1},\mathcal L_t) }

重建。由此證明 Event-Sourced Replay Determinism 與 Checkpoint–Tail Equivalence：只要 reducer、schema、environment fingerprint 與 prefix checkpoint 一致，完整重播與 checkpoint 加 tail replay 產生相同 proof state。

本文進一步建立 proof-authority separation。Proposer、Router、Observatory 只可產生 proposal、policy decision 與 telemetry；它們都無權直接縮小 $\Omega_t$ 或設定 $GCC.Valid$ 。只有通過 verifier、route / representation contract、coverage、boundary、必要 gluing、dependency / version 等 gate 的 certificate，才可由 commit controller 激活並改變 authoritative survivor state。這給出 Certificate-Gated Commit Preservation：若初始 survivor sound，且每個 activated exclusion certificate 都是 counterexample-safe，則所有 committed states 永遠保持

\boxed{ \mathcal C\subseteq\Omega_t. }

本文同時把 Paper 04 的 support-aware rollback 實作成 runtime invariant。certificate 失效時，真正 reopen 的區域只包含失去最後一個 active sound support 的 states，而不是所有曾被該 theorem 觸碰的區域。

在 benchmark 層，本文採納一個更嚴格的分層：kernel proof validity、formal statement fidelity、route / coverage fidelity、runtime reproducibility 與 observatory metrics 分屬不同 authority channels。2026 年對 Lean theorem-proving benchmarks 的 audit 顯示，即使 solution kernel-check 通過，benchmark 本身仍可能包含 vacuity、錯誤 formalization、缺 hypothesis 或 unsound axiom。因此 SDPE benchmark 不允許以「Lean 編譯成功」替代 problem-fidelity audit。

本文提出八條 benchmark tracks：finite closure、representation、global coverage、rollback / replay、DVI、exceptional-core、routing，以及 domain adapter。每個 benchmark 必須 pin problem fingerprint、formalization / adapter version、runtime schema、verifier / kernel version、dependency snapshot、routing policy、model / prover version、hardware / concurrency metadata、random seed 與 audit version。Proof-Space Observatory 可以讀取並顯示 survivor geometry、DVI telemetry、gap debt、routing values、dirty replay 與 support multiplicity，但 observatory 是非權威的：任何 dashboard 指標都不能自行提交 theorem cut 或 global closure。

本文最後提供一個標準 Python prototype、JSON state / event / benchmark schemas、append-only example ledger、finite structural checker 與 Hard-Zeta case-study adapter specification。這使 SDPE Phase I 從一組概念論文轉成一個可重播、可 benchmark、可擴充的 proof-space runtime contract。

關鍵詞

空間域證明包圍；proof runtime；event sourcing；proof-space observatory；Global Closure Certificate；proof provenance；rollback；incremental replay；benchmark fidelity；formal verification；AI theorem proving；proof telemetry；survivor space

1. Phase I 的整合問題

前七篇回答的問題可以排列為：

\boxed{ \begin{aligned} &\text{P01: 如何安全縮小反例候選域？}\\ &\text{P02: 如何避免 representation 先丟失 proof-relevant fibers？}\\ &\text{P03: 如何把 local routes 關閉成 global closure？}\\ &\text{P04: 如何編譯 proof history 並做 incremental replay？}\\ &\text{P05: 如何區分 discovery acceleration 與 verification dominance？}\\ &\text{P06: 如何辨認 measure-zero / singular exceptional core？}\\ &\text{P07: 如何選擇下一個研究 action？} \end{aligned} }

但若這些對象存在於不同文件、不同 AI session、不同 theorem prover、不同 notebook 或不同版本，它們仍不能形成一個可靠長時程研究系統。

Paper 08 的問題是：

如何建立一個最小 runtime，使上述所有 proof objects 具有一致 state semantics、event provenance、authority separation、rollback、replay、benchmark 與 observability？

本文不嘗試建立完整 theorem prover。SDPE Runtime 的角色是proof-space control plane：管理證明域、證書、依賴、coverage、routing 與研究 telemetry，而底層 proof checking 可由 Lean、Coq、Isabelle、SMT/SAT certificate checker、domain-specific checker 或人工形式化 audit 承擔。

2. Fresh literature grounding

2.1 Scalable verifier infrastructure

AXLE 在 2026 年把 Lean proof verification、proof manipulation、metadata extraction、多版本支援與 per-request isolation 提升成 scalable cloud infrastructure。這說明 AI mathematics runtime 不應把 verifier 視為單一 compile 指令，而應把版本、隔離、request identity、metadata 與 strict verification 當成 first-class runtime state。

SDPE 取其工程原則：

\boxed{ \text{verification service} \neq \text{proposal service}. }

2.2 Formal proof validity is not benchmark fidelity

2026 年對五個 Lean theorem-proving benchmarks 的 audit 顯示，kernel-check 只能證明 proof term 證成了 formal statement，不能證明 formal statement 忠實對應 intended problem，也不能保證 benchmark harness 沒有 vacuity、unsound axiom、missing hypotheses 或其它 specification defects。

因此 SDPE 將 benchmark authority 拆成：

\boxed{ \text{Proof Validity} \neq \text{Statement Fidelity} \neq \text{Coverage Fidelity} \neq \text{Performance Telemetry}. }

2.3 Dependency-rich benchmark design

TheoremBench 同時發布 main theorem 與 premise-expanded theorem families，並用 theorem-level coverage / token-efficiency 描述 proof behavior。這支持 SDPE benchmark 不只記錄「最後成功或失敗」，還要保存 dependency / partial progress / closure-obligation structure。

2.4 Observable agent loops

OpenProver 將 Planner、Workers、Whiteboard / Repository 與 formal Verifier 分離，並提供 reproducible automatic verification。這與 SDPE authority separation 相容：規劃、生成、儲存與驗證不應由同一個未區分的 agent authority 承擔。

2.5 Operational state reuse

Proof-state snapshotting 顯示，重建 elaborated state 可佔 branching search 的主要成本，而直接 reuse state 可以大幅降低 wall time。SDPE 將 snapshot / checkpoint 視為 operational accelerator；它不自動繼承 theorem validity authority。

3. Canonical SDPE Runtime State

Definition 3.1 — SDPE State

定義 epoch $t$ 的 runtime state：

\boxed{ \mathbb S_t = \langle \Omega_t, RouteCert_t, \mathbf G_t, GCC_t, \mathcal H_t, Compiled_t, DVI_t, SurvProf_t, RouteDecision_t, Env_t \rangle. }

其中：

$\Omega_t$ ：authoritative survivor envelope；
$RouteCert_t$ ：active route / representation contracts；
$\mathbf G_t$ ：typed closure gaps；
$GCC_t$ ：Global Closure Certificate state；
$\mathcal H_t$ ：proof-history dependency DAG；
$Compiled_t$ ：closure basis、support index、snapshots、dirty / reopen state；
$DVI_t$ ：Paper 05 cost telemetry；
$SurvProf_t$ ：Paper 06 survivor geometry profile；
$RouteDecision_t$ ：Paper 07 routing decision / policy provenance；
$Env_t$ ：runtime / checker / dependency / model / hardware fingerprints。

3.2 Authoritative vs diagnostic fields

將 state fields 分成兩類。

Proof-authoritative

\boxed{ \Omega_t, RouteCert_t, \mathbf G_t, GCC_t, \mathcal H_t^{\rm active}, Compiled_t^{\rm support}. }

Diagnostic / policy

\boxed{ DVI_t, SurvProf_t, RouteDecision_t, \text{predicted values}, \text{dashboard metrics}. }

後者可以改變研究排序，不能直接改變數學真值或 closure bit。

4. Proof Authority Separation

Definition 4.1 — Authority channels

SDPE Runtime 至少區分：

Proposer：產生 theorem / refinement / repair candidate；
Router：排序或選擇 action；
Verifier：驗證 local certificate；
Coverage Auditor：驗證 route / branch cover；
Boundary Auditor：驗證 equality / singular / degenerate strata ownership；
Glue Auditor：只在 ConstructiveGluing mode 驗證 compatibility / gluing；
Compiler：建立 proof index / closure basis / snapshot / support map；
Commit Controller：在 gates 通過後激活 certificate；
Observatory：只讀 telemetry / visualization。

Proposition 4.2 — Proposal Non-Authority

若 runtime mutation contract 規定只有 Commit / Invalidate 類 authority events 能改變 authoritative survivor state，則任意 proposal 或 route-value prediction 都不能單獨推出：

\Omega_{t+1}\subsetneq\Omega_t.

這是系統規格命題，不是數學 theorem：它必須由 runtime enforcement 實作。

No-Go 4.3 — Model Confidence as Proof Authority

以下都不能激活 theorem cut：

LLM confidence；
route score；
retrieval similarity；
sampled empirical support；
observatory anomaly score；
benchmark historical success rate。

只有 registered proof / audit certificate 可進 commit gate。

5. Event-Sourced Proof State

Definition 5.1 — Event Ledger

令 append-only event ledger 為：

\boxed{ \mathcal L_t=(e_0,e_1,\ldots,e_t). }

每個 event 至少帶有：

\langle seq, kind, payload, actor, version, fingerprint \rangle.

Definition 5.2 — Deterministic reducer

令

\mathcal R: \mathbb S\times\mathcal E\to\mathbb S

為 deterministic reducer。

狀態定義為：

\boxed{ \mathbb S_t = \operatorname{Fold}(\mathcal R,\mathbb S_{-1},\mathcal L_t). }

Theorem 5.3 — Event-Sourced Replay Determinism

若：

initial state 相同；
event ledger byte-equivalent / canonically equivalent；
reducer version 相同；
reducer deterministic；

則 full replay 的 final state 唯一。

Proof

對 event sequence length induction。零事件時 state 相同。若前 $k$ 個 events 後 state 唯一，由 deterministic $\mathcal R$ ，第 $k+1$ 個 event 對相同 state 產生唯一 successor。故成立。 $\square$

Corollary 5.4 — State fingerprint

若 state 使用 canonical serialization，可定義：

\boxed{ F_t = H(\operatorname{Canon}(\mathbb S_t)). }

不同 machine / session replay 應得到相同 fingerprint，否則 runtime / environment drift 必須被視為 verification event。

6. Checkpoint–Tail Replay

對長時程研究，不應每次從 event 0 完整重播。

令 prefix ledger：

\mathcal L_{0:k}

產生 checkpoint：

\widehat{\mathbb S}_k.

Theorem 6.1 — Checkpoint–Tail Equivalence

若 checkpoint 經完整 prefix replay 驗證，且 reducer / schema / environment fingerprint 未變，則：

\boxed{ \operatorname{Fold}(\mathcal R,\mathbb S_{-1},\mathcal L_{0:t}) = \operatorname{Fold}(\mathcal R,\widehat{\mathbb S}_k,\mathcal L_{k+1:t}). }

Proof

由 fold associativity 與 checkpoint 定義立即成立。 $\square$

No-Go 6.2 — Snapshot Equals Certificate

checkpoint 只證明：「在指定 reducer / environment 下可以重建這個 state」。

它不證明 checkpoint 內每個 theorem / route / coverage certificate 的數學正確性。certificate authority 仍由其原始 checker / dependency provenance 承擔。

7. Certificate-Gated Commit

Definition 7.1 — Commit gate

令 candidate certificate $c$ 要進 active state，至少要求：

\boxed{ \begin{aligned} &\mathsf{ProposalExists}(c),\\ &\mathsf{LocalVerify}(c)=\mathrm{pass},\\ &\mathsf{DepsActive}(c),\\ &\mathsf{VersionMatch}(c),\\ &\mathsf{RouteLiftValid}(c),\\ &\mathsf{RequiredAuditsValid}(c). \end{aligned} }

若 conclusion 要提交 global closure，還需要 Paper 03 的 GCC obligations。

Theorem 7.2 — Certificate-Gated Survivor Preservation

設初始 state 滿足：

\mathcal C\subseteq\Omega_0.

若每一個 committed exclusion certificate $c$ 排除的 region $E_c$ 都已 soundly 證明：

E_c\cap\mathcal C=\varnothing,

且 committed survivor update 為：

\Omega_{t+1} = \Omega_t\setminus \bigcup_{c\in A_t}E_c,

則所有 committed epochs 保持：

\boxed{ \mathcal C\subseteq\Omega_t. }

Proof

若 $x\in\mathcal C$ ，由 induction hypothesis $x\in\Omega_t$ 。又對所有 committed $c$ ， $x\notin E_c$ 。故 $x\in\Omega_{t+1}$ 。 $\square$

7.3 GCC bit 的語義

GCC.Valid = true 本身不是 proof artifact。它只是一個 runtime result bit，其可置信性來自：

\boxed{ \text{event replay} + \text{active certificate basis} + \text{cover / boundary / glue obligations} + \text{environment fingerprints}. }

因此最終 publication / submission 應附 closure basis / proof artifacts，而不是只附一個 runtime JSON flag。

8. Invalidation, Dirty State, and Precise Reopening

Paper 04 定義 support multiplicity：

\kappa_t(x) = \#\{c:x\in E_c,\;c\text{ active}\}.

certificate 失效後：

\boxed{ R = \{x:\kappa_{\rm old}(x)>0,\;\kappa_{\rm new}(x)=0\}. }

Proposition 8.1 — Precise support-aware reopen

若 support index complete，則 certificate invalidation 後：

$\kappa_{\rm new}(x)>0$ 的 point 仍有 sound active exclusion support，不需 reopen；
$\kappa_{\rm new}(x)=0$ 且 previously excluded 的 point 必須 reopen。

這是 stale theorem 局部化修復的 runtime realization。

8.2 Dependency dirty closure

對失效 proof node $v$ ：

Dirty(v) = \{v\}\cup\operatorname{Desc}(v).

只有 dirty closure 與其受影響 coverage / GCC nodes 需要 incremental replay。

9. Typed Gap API

Paper 03 / 06 / 07 的 gaps 在 runtime 中至少分為：

\boxed{ \mathbf G = (G_D,G_B,G_{\partial},G_C,G_G,G_R,G_{\rm core},G_{\rm repr}). }

典型 API：

register_gap(type, scope, witness, mandatory, dependencies)；
resolve_gap(gap_id, certificate_id)；
reopen_gap(gap_id, stale_dependency)；
query_persistent_gaps()；
query_starvation_age(gap_id)。

Gap priority 是 routing policy；gap closure 是 certificate semantics。二者不得混淆。

10. Route API

每個 route 至少帶有：

\boxed{ RouteCert = \langle Scope, Representation, FiberPolicy, Lift, Boundary, Dependencies, Version, Replay \rangle. }

runtime 應提供：

register_route_cert；
invalidate_route_cert；
refine_representation；
query_singular_fibers；
query_route_coverage。

任何 route representation 改版都應使依賴舊 representation fingerprint 的 certificates 進 dirty state。

11. Proof DAG and Closure-Basis API

proof DAG node 至少保存：

\boxed{ \langle Stmt, Scope, Deps, Route, Version, Fingerprint, Checker, Payload, Region, Status \rangle. }

runtime API：

add_verified_certificate；
active_ancestors；
closure_basis(target)；
invalidate_certificate；
dirty_closure；
incremental_replay；
support_index(region)。

12. Proof-Space Observatory

Definition 12.1 — Observatory

Proof-Space Observatory 是 state / event 的只讀 projection：

\boxed{ \mathsf{Obs}_t = \Psi(\mathbb S_t,\mathcal L_t). }

其輸出可以包括：

D_t^{\rm resolve}, \quad D_t^{\rm frontier}, \quad W_t, \quad \sigma_t, \quad h_t, \quad \chi_t, \quad |Dirty_t|, \quad |R_t|,

以及：

SurvProf_t, \quad \mathbf G_t, \quad RouteValue_t, \quad support\ multiplicity, \quad certificate\ debt.

Theorem 12.2 — Observatory Non-Authority

若 runtime mutation rules 不接受 observatory output 作 proof-authoritative event，則 observatory telemetry 的任意改變不能單獨改變：

\boxed{ \Omega_t \quad\text{或}\quad GCC_t.Valid. }

這是安全架構原則：

\boxed{ \text{measurement} \neq \text{mathematical authority}. }

13. Runtime Pipeline

Phase-I reference pipeline：

\boxed{ \begin{aligned} &\mathsf{Detect}\\ &\to\mathsf{Profile}\\ &\to\mathsf{GapExtract}\\ &\to\mathsf{ActionGenerate}\\ &\to\mathsf{Route}\\ &\to\mathsf{Propose}\\ &\to\mathsf{Verify}\\ &\to\mathsf{CoverageAudit}\\ &\to\mathsf{BoundaryAudit}\\ &\to\mathsf{GlueAudit}\\ &\to\mathsf{Compile}\\ &\to\mathsf{Commit}. \end{aligned} }

這不是強迫所有 domain 逐步執行每一 stage。RefutationOnly problem 可以讓 GlueAudit 返回 not-required certificate；沒有 representation change 的 epoch 可以略過 refine action；但所有被略過的 authority gate 必須有明確的 not-applicable semantics，不能靠 silent omission。

14. Benchmark Authority Separation

Formal theorem benchmark 至少有四層 correctness：

14.1 Proof validity

底層 kernel / checker 接受 proof artifact。

14.2 Statement fidelity

formal statement 是否忠實代表 intended mathematical problem。

14.3 Closure / route fidelity

local cases 是否真正 cover domain、representation 是否 sound、boundaries 是否有 ownership。

14.4 Evaluation fidelity

metric / harness 是否沒有 leakage、vacuity、shortcut、version mismatch 或不公平 cost accounting。

因此：

\boxed{ \text{proof checks} \not\Rightarrow \text{benchmark is sound}. }

這一點不是理論上的杞人憂天；2026 benchmark audit 已在現有 Lean benchmarks 中機械發現多種問題。

15. SDPE Benchmark Tracks

本文定義八條最小 tracks。

Track A — Finite Closure

有限 universe 有 hidden oracle。測：

survivor soundness；
theorem cut；
cover certificate；
GCC；
false closure rejection。

Track B — Representation

測：

fiber saturation；
mixed-fiber retention；
route refinement；
lift certificate。

Track C — Global Coverage

測：

branch union；
boundary omission；
overlap；
RefutationOnly / ConstructiveGluing mode。

Track D — Rollback / Replay

測：

stale dependency；
dirty closure；
support-aware reopen；
full vs incremental replay；
checkpoint equivalence。

Track E — DVI

沿用 Paper 05：

Queue A known / replay；
Queue B near-frontier transfer；
Queue C true frontier；
cold vs compiled；
build / maintenance / replay cost。

Track F — Exceptional Core

測：

measure-zero survivor；
singleton localization；
theorem-language irreducible core；
representation-singular residue。

Track G — Routing

測：

volume greedy；
gap-aware；
bridge-aware；
Pareto routing；
fairness；
time-to-GCC。

Track H — Domain Adapter

將真實數學研究映射成 SDPE objects，例如：

Hard-Zeta / Collatz；
SAT / cube-and-conquer；
finite graph classification；
repository-scale Lean verification。

Domain adapter benchmark 不應假裝 hidden oracle 存在；它主要測 provenance、state reconstruction、routing、certificate integration 與 research telemetry。

16. Benchmark Fingerprints

每次 run 至少 pin：

\boxed{ \begin{aligned} &ProblemHash,\\ &StatementHash,\\ &AdapterVersion,\\ &RuntimeSchema,\\ &ReducerVersion,\\ &VerifierVersion,\\ &DependencySnapshot,\\ &RoutePolicyVersion,\\ &ModelVersion,\\ &HardwareProfile,\\ &Seed,\\ &AuditVersion. \end{aligned} }

定義 benchmark identity：

\boxed{ BenchID = H( ProblemHash\Vert EnvHash\Vert SchemaHash\Vert PolicyHash\Vert Seed ). }

若這些 fingerprint 不同，runtime 可以比較結果，但不得把它們默認當成同一 experimental condition。

17. Benchmark Metrics

17.1 Correctness metrics

false exclusion count；
false GCC count；
missed reopen count；
stale certificate activation count；
route / boundary omission count。

在 sound benchmark 中，proof-authoritative false-positive 應要求：

\boxed{0.}

17.2 Replay metrics

full replay time；
checkpoint-tail replay time；
dirty replay fraction；
state fingerprint mismatch rate。

17.3 Compilation metrics

compiled hit rate $h$ ；
closure-basis compression $\chi$ ；
support multiplicity；
reopen precision；
build / maintenance cost。

17.4 Closure metrics

active mandatory gap count；
boundary debt；
certificate debt；
time-to-GCC；
accepted nonredundant cut count。

17.5 DVI metrics

沿用：

D^{\rm resolve}, D^{\rm frontier}, W, \sigma, G^{\rm compile}, P^{\rm drift}.

17.6 Routing metrics

nonredundant closure yield；
action cost；
routing regret；
mandatory-gap starvation age；
bridge unlock rate。

18. Runtime Replay Theorems and Their Boundaries

Event-sourced determinism 證明的是：

\boxed{ \text{same validated history} \to \text{same runtime state}. }

它不證明：

\boxed{ \text{the history itself is mathematically valid}. }

同樣：

\boxed{ \text{incremental replay = full replay} }

只在 dependency metadata、checker determinism、version fingerprints 完整的 runtime contract 下成立。

因此 runtime theorem 與 mathematical theorem 必須分層記帳。

19. Benchmark-Fidelity Gate

在正式 benchmark acceptance 前，至少要求：

statement fidelity audit；
proof-kernel / checker version pinned；
banned axioms / shortcuts policy declared；
dependency graph audited；
test harness replayable；
environment fingerprint complete；
hidden oracle 只在 toy / synthetic track 使用；
metric authority 不超過其定義範圍。

No-Go 19.1 — Kernel-Checked Means Benchmark-Correct

錯。

kernel 只回答：

這個 proof term 是否證成這個 formal statement？

它不回答：

這個 formal statement 是否忠實翻譯 intended problem？

也不回答：

benchmark route / coverage / cost protocol 是否公平？

20. Hard-Zeta Adapter as a Case-Study Interface

SDPE Runtime 不重新證明 Hard-Zeta 的任何 theorem。adapter 只規定如何映射已存在的研究 artifacts。

可將 B-side frontier branches 映射成：

G_B

與 route nodes；把每個 theorem / no-go / reduction 放入 proof DAG；把 survivor parameter inequalities 存成 symbolic constraint payload；把 checker / JSON / literature provenance 綁到 certificate nodes；把 Sparse / Huge-PQ / structured survivor ladder 等 branch frontier 當作 typed gaps / route obligations。

任何 numerical exponent、checker PASS 或 paper statement 都只有在其 upstream proof certificate 被正式接入 runtime 後，才可對 authoritative survivor state 產生作用。

因此 adapter 不是「把聊天紀錄直接變 proof」，而是：

\boxed{ \text{research artifacts} \to \text{typed candidates} \to \text{verification} \to \text{certificate nodes} \to \text{committed SDPE state}. }

21. Reference Prototype

本 bundle 提供：

sdpe_runtime.py：deterministic event reducer；
SDPE_State_Schema_v1.json；
SDPE_Event_Schema_v1.json；
SDPE_Benchmark_Schema_v1.json；
example_finite_closure_run.jsonl；
example_final_state.json；
verify_SDPE_Paper08_runtime.py；
Hard-Zeta adapter specification。

prototype 刻意保持簡單：finite explicit survivor universe 用於 structural checker；真正 infinite / symbolic mathematics 必須由 domain adapter 與外部 proof checker 提供 sound symbolic region semantics。

22. Structural Checker Results

companion checker 驗證：

reference ledger replay 到 empty survivor + valid GCC；
$1500$ 組 random event histories deterministic replay；
$1500$ 組 checkpoint-tail equivalence；
$1500$ 組 hidden-oracle survivor soundness；
proposal non-authority；
telemetry non-authority；
unverified-certificate commit rejection；
redundant-support rollback precision；
GCC authority separation。

checker 只驗證 finite runtime semantics，不驗證 arbitrary mathematical certificate 的內容真偽。

23. No-Go Ledger

No-Go 23.1 — Runtime State Equals Mathematical Truth

runtime 只能攜帶 certificate-backed belief state；真理不由 database bit 創造。

No-Go 23.2 — Proposer Can Commit Its Own Result

proposal / verification / commit 必須 authority-separated。

No-Go 23.3 — Observatory Metric Can Close Proof

telemetry 沒有 proof authority。

No-Go 23.4 — Kernel Acceptance Guarantees Statement Fidelity

formal proof validity 與 intended-problem fidelity 是不同 obligations。

No-Go 23.5 — Checkpoint Is a New Proof

checkpoint 是 replay accelerator，不是新增 theorem。

No-Go 23.6 — Event Replay Repairs Missing Dependencies

若 dependency metadata 本身不完整，deterministic replay 只能穩定重現錯誤 state。

No-Go 23.7 — JSON Schema Proves Semantics

schema 只保證 shape；route / theorem / coverage soundness 需要各自 certificate。

No-Go 23.8 — A Benchmark Score Is a Proof-Space Law

benchmark 只能支持被其 design / controls 覆蓋的 empirical claim。

No-Go 23.9 — Domain Adapter Imports Proof Automatically

adapter 只做 typed mapping；原 artifacts 必須驗證後才能 commit。

No-Go 23.10 — Phase-I Runtime Is a Complete Proof Assistant

不是。它是 proof-space orchestration / audit layer。

24. Theorem / System-Assumption / External-Input Ledger

24.1 Internal runtime theorems / propositions

Event-Sourced Replay Determinism；
Checkpoint–Tail Equivalence；
Proposal Non-Authority under enforced mutation rules；
Certificate-Gated Survivor Preservation；
Precise Support-Aware Reopen under complete support index；
Observatory Non-Authority；
Benchmark Identity under canonical fingerprints。

24.2 Inherited SDPE theorems

P01 survivor soundness；
P02 representation faithfulness；
P03 global cover / GCC；
P04 closure basis / rollback / incremental replay；
P05 DVI cost architecture；
P06 exceptional-core semantics；
P07 enclosure routing。

24.3 Runtime correctness assumptions

event ledger append-only / tamper-evident；
reducer deterministic；
canonical serialization stable；
certificate checker identity / version pinned；
dependency metadata complete；
support index complete；
authority boundaries enforced；
benchmark formalization audit honest and versioned。

24.4 External grounding

AXLE scalable strict Lean infrastructure；
2026 formal benchmark fault audit；
TheoremBench dependency-rich benchmark structure；
OpenProver Planner / Worker / Verifier runtime；
Lean proof-state snapshotting；
testing-style semantic evaluation of formal statements。

25. Phase-I Closure

八篇形成第一階段完整 stack：

\boxed{ \begin{aligned} &\text{P01 Survivor Soundness}\\ &\downarrow\\ &\text{P02 Representation Faithfulness}\\ &\downarrow\\ &\text{P03 Global Coverage / Closure}\\ &\downarrow\\ &\text{P04 Trace Compilation / Incremental Replay}\\ &\downarrow\\ &\text{P05 Discovery--Verification Dynamics}\\ &\downarrow\\ &\text{P06 Exceptional-Core Geometry}\\ &\downarrow\\ &\text{P07 Cost-Aware Enclosure Routing}\\ &\downarrow\\ &\text{P08 Runtime / Benchmark / Proof-Space Observatory}. \end{aligned} }

Phase I 現在不再只是「一套想法」；它具有：

proof-space semantics；
closure obligations；
representation contracts；
event provenance；
certificate / dependency state；
rollback / replay；
cost telemetry；
routing semantics；
benchmark protocol；
executable finite prototype。

26. Final Status

Paper 08 的核心原則可以壓縮成五句。

第一：

\boxed{ \text{SDPE state 應由可重播 event history 重建，而不是依賴聊天記憶。} }

第二：

\boxed{ \text{proposal、prediction、telemetry 都沒有 proof commit authority。} }

第三：

\boxed{ \text{verified certificate + global obligations 才能改變 authoritative survivor state。} }

第四：

\boxed{ \text{benchmark 必須同時驗證 proof、statement、coverage 與 environment fidelity。} }

第五：

\boxed{ \text{proof-space observability 應提高研究可理解性，但不能反過來成為數學真理來源。} }

因此，空間域證明包圍第一階段現在形成一個完整迴圈：

\boxed{ \text{Detect} \to \text{Enclose} \to \text{Route} \to \text{Propose} \to \text{Verify} \to \text{Audit} \to \text{Compile} \to \text{Commit} \to \text{Observe} \to \text{Detect again}. }

它仍然不能保證任意猜想會被證明；但它把「長期 AI 輔助數學研究如何留下可驗證痕跡、如何安全收縮反例域、如何避免局部正確冒充全域閉合、如何重用歷史、如何辨認 exceptional hard core、如何選下一刀、如何 benchmark 整個過程」統一成了一個可執行的 proof-space architecture。

References

Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, Jannis Limperg, AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities, arXiv:2606.26442, 2026.
Pawan Sasanka Ammanamanchi, Siddharth Bhat, Stella Biderman, Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving, arXiv:2606.29493, 2026.
QuocViet Pham, Elvir Karimov, Andrey Galichin, Ivan Oseledets, TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics, arXiv:2606.09450, 2026.
Matěj Kripner, Milan Straka, OpenProver: Agentic and Interactive Theorem Proving with Lean 4, arXiv:2607.09217, 2026.
Austin Shen, Yunong Shi, Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4, arXiv:2605.25556, 2026.
Jongyoon Kim, Hojae Han, Seung-won Hwang, Benchmarking Testing in Automated Theorem Proving, arXiv:2604.23698, 2026.
Prior SDPE artifacts: Papers 01--07.