# 空間域證明包圍論 V ## Discovery–Verification Inversion：編譯證明空間、Frontier Drift 與驗證主導相位 ### Spatial-Domain Proof Enclosure V: Discovery–Verification Inversion, Compiled Proof Space, Frontier Drift, and Verification-Dominated Regimes **Version:** v0.1 **Date:** 2026-08-14 **Status:** theorem / hypothesis / benchmark framework; not a claim that mathematical discovery generically accelerates **Canonical source:** UTF-8 Markdown; canonical mathematics uses ` $...$ ` and `$$...$$` only. --- ## 摘要 空間域證明包圍論前四篇依次建立：sound survivor envelope、route representation faithfulness、global coverage / closure certificate，以及 proof trace compilation / incremental replay。Paper 04 因而第一次使「已證歷史不必每輪重算」成為一個可驗證的計算命題，但它刻意沒有證明更強的直覺： > 當 survivor domain 持續收縮、proof trace 持續累積並被編譯後，後續 theorem discovery 是否真的會越來越便宜，而研究成本逐步轉移到 verification、coverage、gluing 與 maintenance？ 本文正式研究此現象，稱為 **Discovery–Verification Inversion**，簡稱 DVI。 本文首先證明必須區分兩種 discovery cost。第一種是**已知域／例行查詢解析成本** $$ D_t^{\mathrm{resolve}}, $$ 即候選 route state 是否已被 active certificates、closure basis 或 compiled pruning state 解決。第二種是**frontier discovery cost** $$ D_t^{\mathrm{frontier}}, $$ 即找到下一個真正改變 survivor envelope、typed gap、RouteCert 或 Global Closure Certificate 的非冗餘 theorem cut 所需成本。 對固定 query distribution，若 compiled region 單調擴張且 compiled-hit cost 不高於 full resolution cost，本文證明 $$ \boxed{ D_{t+1}^{\mathrm{resolve}} \le D_t^{\mathrm{resolve}}. } $$ 這是一個真正的 compilation monotonicity theorem。但若研究 query distribution 本身向剩餘 frontier 漂移，成本差可精確分解為 $$ \boxed{ \Delta D_t^{\mathrm{resolve}} = -G_t^{\mathrm{compile}} + P_t^{\mathrm{drift}}, } $$ 其中 $G_t^{\mathrm{compile}}$ 是新增 compiled region 帶來的節省，而 $P_t^{\mathrm{drift}}$ 是研究重心向更難 survivor frontier 移動造成的分布漂移項。只有當 $$ G_t^{\mathrm{compile}}>P_t^{\mathrm{drift}} $$ 時，例行 query-resolution 才保證加速。 本文進一步證明一個重要 no-go：若 query distribution 被嚴格限制在 unresolved frontier 上，則 compiled-hit 的直接收益為零。故 $$ \boxed{ \text{known-region acceleration} \not\Rightarrow \text{frontier theorem discovery acceleration}. } $$ 因此本文把 DVI 分為弱式與強式。**Weak DVI** 只要求例行解析成本下降且 verification share 上升；**Strong DVI** 則要求每個非冗餘 frontier theorem cut 的 discovery cost 也呈下降趨勢。後者不是本文定理，而是可否證研究假說。 令 $$ W_t = C_t^{\mathrm{verify}} +C_t^{\mathrm{coverage}} +C_t^{\mathrm{glue}} +C_t^{\mathrm{maintain}} +C_t^{\mathrm{replay}} $$ 為 verification bundle，定義 verification share $$ \boxed{ \sigma_t = \frac{W_t}{D_t+W_t}. } $$ 本文證明：若 $D_t$ 下降且 $W_t$ 上升，則 $\sigma_t$ 必定上升。更進一步，如果 discovery savings 大於 verification growth，則可以同時出現 $$ \boxed{ \text{total cost 下降} \quad+ \text{verification share 上升}. } $$ 這正是「研究整體越來越快，但最後主要時間花在驗證」的數學上可一致情形。 本文最後提出一套 **DVI Benchmark Protocol**，要求固定模型／工具版本、 paired cold-vs-compiled runs、隨機化 task order、完整計入 build / indexing / maintenance 成本、把 routine-resolution 與 frontier discovery 分開計量，並以 formal checker / proof kernel 驗證所有 accepted proof artifacts。只有在此類 longitudinal benchmark 中觀察到可重現趨勢，才可聲稱 DVI 發生。 本文因此得到的最強結論不是「後期研究必然越來越快」，而是： $$ \boxed{ \textbf{SDPE 中的速度反轉可以被精確分解、測量、證偽，並與單純 cache speedup 嚴格區分。} } $$ --- ## 關鍵詞 空間域證明包圍；Discovery–Verification Inversion；proof compilation；frontier drift；verification dominance；proof reuse；incremental verification；survivor space；frontier hardening；amortization；AI theorem proving；longitudinal benchmark --- # 1. 前四篇留下的正式狀態 考慮全域命題 $$ \forall d\in D,\;P(d), $$ 真實反例集合為 $$ \mathcal C = \{d\in D:\neg P(d)\}. $$ Paper 01 維持 sound survivor invariant： $$ \boxed{ \mathcal C\subseteq\Omega_t. } $$ Paper 02 要求 route representation 不得把 proof-relevant counterexample fibers 靜默壓掉。 Paper 03 建立 Global Closure Certificate： $$ \mathsf{GCC} = \langle Master,Atlas,CoverCert,LocalCerts,BoundaryCert,LiftCerts, GlueMode,GlueCert,DepDAG,Version,Replay \rangle. $$ Paper 04 把已驗證歷史編譯為 dependency DAG、closure basis、support index 與 incremental replay state。對 route state $x$， $$ \kappa_t(x) = \#\{v\in A_t:x\in E_v\} $$ 表示 active exclusion support multiplicity；若 $$ \kappa_t(x)>0, $$ 則至少一張 active sound certificate 已排除 $x$。 Paper 04 因而證明： $$ \boxed{ \text{verified proof history} \to \text{compiled pruning state} } $$ 可以是 sound 的。 但它沒有證明： $$ \boxed{ \text{compiled proof state} \Longrightarrow \text{frontier theorem discovery 越來越容易}. } $$ 這正是本文要處理的區分。 --- # 2. Fresh literature grounding ## 2.1 Proof-state snapshotting：加速 reconstruction，不等於加速 discovery Shen 與 Shi 2026 年的 Lean 4 proof-state snapshotting 工作指出，portfolio tactic search 的大量 wall time 可能來自每個 branch 重複載入 import 與重新 elaborating theorem context，而非 tactic 本身。其 48 個 miniF2F-v2 benchmark 中報告 5.6--50 倍 wall-time speedup。 該研究同時清楚區分：其主要 benchmark 測量的是 tactic-search infrastructure speed，而非一般 theorem discovery difficulty。 本文因此採用： $$ \boxed{ \text{reconstruction avoidance} \neq \text{frontier discovery acceleration}. } $$ ## 2.2 Proof-certificate recycling：verification 也可以被攤銷 Kaufmann 與 Hofstadler 2025 年的 algebraic proof certificate recycling 把重複 algebraic proof fragments 提煉成可再 instantiate 的 proof rules，並在其 checker 中降低 proof size 與 verification time。 因此 verification 不必被模型化成只能單調增加；它本身也可以受到 compilation / pattern reuse 影響。 這一點對 DVI 很重要： $$ \boxed{ \text{verification share 上升} \not\Rightarrow \text{verification absolute cost 必然上升}. } $$ ## 2.3 Accumulated proof knowledge：已有領域性 reuse evidence CircuitProver 2026 在 63 個 hardware theorem-proving tasks 上累積 proving traces 與 verified theorems。其 ablation 報告 accumulated proof knowledge 減少 proof construction redundancy，降低 proof length 與 verification time。 LeanAgent 則從 lifelong theorem proving 角度研究持續擴張的 formal knowledge base 與 backward transfer。 這些工作支持「累積 verified proof knowledge 可改善後續任務」的可能性，但都不能推出一般數學研究中的 Strong DVI。 ## 2.4 Dependency closure 也可能使 frontier 變難 VeriSoftBench 2026 收集 500 個 repository-scale Lean proof obligations，發現 success 與 transitive repository dependence 有顯著關聯：需要較大、多跳 dependency closure 的任務更難成功；只提供 curated dependency closure 比暴露整個 repository 好，但仍留有顯著困難。 這為本文的 **frontier-hardening counterforce** 提供直接外部背景： $$ \boxed{ \text{knowledge base 變大} \not\Rightarrow \text{remaining theorem 變簡單}. } $$ ## 2.5 Scalable strict verification 是獨立工作負擔 AXLE 2026 把 strict proof verification、metadata extraction、multi-version support 與 per-request isolation 作為大規模 Lean infrastructure 的核心功能，顯示在 AI theorem-proving workflow 中，verification 本身已是一個需要獨立 scale 的系統層。 本文不把 AXLE 的 throughput 當作 DVI evidence；它只支持 verification workload 應被獨立計量，而不能隱藏在「prover succeeded」一個 bit 裡。 --- # 3. 第一個關鍵區分：Routine Resolution 與 Frontier Discovery ## Definition 3.1 — Routine Resolution Cost 設 route-state space 為 $X$。時刻 $t$ 的 compiled-known region 定義為 $$ \boxed{ K_t := \{x\in X:\kappa_t(x)>0\} \cup K_t^{\rm reusable}, } $$ 其中 $K_t^{\rm reusable}$ 可以包含已有 active RouteCert / verified pattern 能直接處理的 states。 對 query $x$，若 $x\in K_t$，使用 compiled path 的成本為 $$ c_H(x), $$ 若 $x\notin K_t$，完整展開成本為 $$ c_F(x), $$ 並假設 $$ 0\le c_H(x)\le c_F(x). $$ 令研究 query distribution 為 $\mu_t$，定義例行解析成本： $$ \boxed{ D_t^{\rm resolve} := \int_X \left[ \mathbf 1_{K_t}(x)c_H(x) + \mathbf 1_{X\setminus K_t}(x)c_F(x) \right] \,d\mu_t(x). } $$ 這個量測的是「面對當前 query stream，已編譯證明空間替我們省掉多少重複展開」。 ## Definition 3.2 — Frontier Discovery Cost 定義一個 theorem cut 為 **nonredundant**，若它至少改變下列之一： $$ \Omega_t, \qquad \mathbf G_t, \qquad \mathsf{RouteCert}_t, \qquad \mathsf{GCC}_t, $$ 且該改變通過相應 checker / coverage / representation obligations。 令 $$ \boxed{ D_t^{\rm frontier} } $$ 表示從進入 active unresolved frontier，到得到下一個 accepted nonredundant theorem cut 所需的完整 discovery resources。 可以用： - model calls； - tokens； - CPU / GPU time； - explored proof states； - rejected theorem proposals； - failed route branches； - human mathematical review time； - symbolic / numerical experiment cost； 等向量或加權 scalar 表示。 ## No-Go 3.3 — 兩種 discovery cost 不可混淆 $$ \boxed{ D_t^{\rm resolve}\downarrow \not\Rightarrow D_t^{\rm frontier}\downarrow. } $$ proof cache、snapshot、compiled support index 首先直接影響的是前者。 後者只有在 survivor geometry、route branching、premise structure、proof distance 或 theorem interaction 真正變簡單時才會下降。 --- # 4. Fixed-Distribution Compilation Monotonicity ## Theorem 4.1 — Fixed-Distribution Compilation Monotonicity 假設： 1. query distribution 固定： $$ \mu_{t+1}=\mu_t=\mu; $$ 2. compiled region 單調擴張： $$ K_t\subseteq K_{t+1}; $$ 3. hit / miss costs 在兩輪間不變； 4. 對所有 $x$： $$ c_H(x)\le c_F(x). $$ 則： $$ \boxed{ D_{t+1}^{\rm resolve} \le D_t^{\rm resolve}. } $$ ### Proof 兩輪唯一可能改變成本的 points 位於 $$ K_{t+1}\setminus K_t. $$ 對這些 points，成本由 $c_F(x)$ 降為 $c_H(x)$。故 $$ D_t^{\rm resolve} - D_{t+1}^{\rm resolve} = \int_{K_{t+1}\setminus K_t} (c_F-c_H) \,d\mu \ge0. $$ $\square$ ## Corollary 4.2 — Strict acceleration condition 若 $$ \mu(K_{t+1}\setminus K_t)>0 $$ 且在一個 positive-measure subset 上 $$ c_HP_t^{\rm drift}. } $$ 這把「越來越快」第一次拆成兩個可量化的競爭項： $$ \boxed{ \text{Compilation Gain} \quad\text{vs}\quad \text{Frontier Drift}. } $$ --- # 6. Frontier Cache Nullity ## Proposition 6.1 — Direct Compiled-Hit Nullity on a Strict Frontier 若時刻 $t$ 的工作 distribution 完全支撐於 unresolved frontier： $$ \mu_t(K_t)=0, $$ 則： $$ \boxed{ D_t^{\rm resolve} = \int_X c_F(x)d\mu_t(x). } $$ 即 compiled-hit 在此 distribution 下的直接收益為零。 ### Interpretation 這不是說歷史 theorem 對 frontier 沒有幫助。 它仍可能透過： - 降低 branching factor； - 提供 reusable lemmas； - 縮短 proof distance； - 改善 route selection； - 產生 stronger invariant； - 排除 spurious subroutes； 間接幫助 frontier。 但這些是**結構性 discovery acceleration**，不是單純 cache hit。 因此： $$ \boxed{ \text{Strong DVI} } $$ 是一個非平凡研究假說。 --- # 7. Verification Bundle Paper 04 已提供多種 verification-side cost primitives。本文將其合併為： $$ \boxed{ W_t := C_t^{\rm verify} + C_t^{\rm coverage} + C_t^{\rm glue} + C_t^{\rm maintain} + C_t^{\rm replay}. } $$ 其中： - $C^{\rm verify}$：local theorem / certificate checking； - $C^{\rm coverage}$：route / branch / boundary completeness audit； - $C^{\rm glue}$：constructive mode 的 overlap / cocycle / global compatibility audit； - $C^{\rm maintain}$：dependency metadata、versioning、support index、storage； - $C^{\rm replay}$：dirty closure / target basis incremental replay。 總 discovery cost 定義為： $$ \boxed{ D_t := D_t^{\rm resolve} + D_t^{\rm frontier}. } $$ 總成本： $$ \boxed{ C_t^{\rm total} = D_t+W_t. } $$ --- # 8. Verification Share 與 Dominance ## Definition 8.1 — Verification Share $$ \boxed{ \sigma_t := \frac{W_t}{D_t+W_t}. } $$ 若 $$ \sigma_t>\frac12, $$ 則稱當前 epoch 為 **verification-dominated**。 ## Theorem 8.2 — Verification-Share Monotonicity 若 $$ D_{t+1}\le D_t $$ 且 $$ W_{t+1}\ge W_t, $$ 則： $$ \boxed{ \sigma_{t+1}\ge\sigma_t. } $$ 至少一個 inequality 嚴格時，verification share 嚴格上升。 ### Proof 需要證： $$ \frac{W_{t+1}}{D_{t+1}+W_{t+1}} \ge \frac{W_t}{D_t+W_t}. $$ 等價於 $$ W_{t+1}D_t \ge W_tD_{t+1}. $$ 由 $$ W_{t+1}\ge W_t $$ 及 $$ D_t\ge D_{t+1} $$ 立即成立。 $\square$ ## Corollary 8.3 — Eventual relative verification dominance 若 $$ D_t\to0 $$ 且存在 $w_0>0$ 使充分大 $t$ 均有 $$ W_t\ge w_0, $$ 則： $$ \boxed{ \sigma_t\to1. } $$ 注意：這只表示**相對 share** 趨近驗證主導，不表示 $W_t$ 必須絕對增加。 --- # 9. Productive Inversion：整體更快但驗證比重更高 原始直覺最有意思的形式不是「verification 變慢」，而是： > 整體研究成本下降，但 discovery 下降得更快，因此 verification 成為主要成本。 ## Theorem 9.1 — Productive Absolute Inversion Condition 假設： $$ D_{t+1}W_t, $$ 且 discovery savings 大於 verification growth： $$ \boxed{ D_t-D_{t+1} > W_{t+1}-W_t. } $$ 則同時有： $$ \boxed{ C_{t+1}^{\rm total}\sigma_t. } $$ 因此： $$ \boxed{ \text{overall acceleration} + \text{verification-share growth} } $$ 在數學上完全可以同時發生。 這正是本文稱為 **productive inversion** 的 regime。 --- # 10. DVI 的分級定義 為避免一個模糊名稱承擔過多主張，本文定義四層現象。 ## Definition 10.1 — Reuse Acceleration 若在可比 task distribution 上： $$ \boxed{ D_t^{\rm resolve} \text{ 呈顯著下降趨勢}, } $$ 則稱為 reuse acceleration。 這是目前最容易由 compilation 理論與工程實驗支持的一層。 ## Definition 10.2 — Verification-Dominance Transition 若存在 $t_*$ 使 $$ \sigma_t<\frac12 $$ 在 $t\frac12 $$ 在 $t>t_*$ 的一個穩定區間成立，稱發生 verification-dominance transition。 ## Definition 10.3 — Weak Discovery–Verification Inversion 若同一 longitudinal window 內： $$ \boxed{ D_t^{\rm resolve}\downarrow } $$ 且 $$ \boxed{ \sigma_t\uparrow, } $$ 稱為 **Weak DVI**。 Weak DVI 不要求 frontier theorem discovery 變容易。 ## Definition 10.4 — Strong Discovery–Verification Inversion 若同一 longitudinal window 內除了 verification share 上升，還觀察到每個 accepted nonredundant theorem cut 的： $$ \boxed{ D_t^{\rm frontier}\downarrow, } $$ 則稱為 **Strong DVI**。 Strong DVI 是本文的主要 open empirical hypothesis。 ## Definition 10.5 — Productive DVI 若 DVI window 同時滿足： $$ \boxed{ C_t^{\rm total}\downarrow, } $$ 則稱為 Productive DVI。 這排除了「只是 verification system 變得非常低效，所以 verification share 上升」的假象。 --- # 11. Discovery–Verification Inversion Hypothesis ## Hypothesis 11.1 — Weak DVI Hypothesis 在以下條件下的長時程、相關 theorem family 中： 1. route representation 穩定； 2. proof trace 被完整編譯； 3. compiled pruning hit rate 提高； 4. one-time build / maintenance cost 已完整記帳； 5. benchmark difficulty ordering 受控； 存在可重現 window，使： $$ \boxed{ D_t^{\rm resolve}\downarrow \quad\text{且}\quad \sigma_t\uparrow. } $$ 此 hypothesis 已獲現有 proof-reuse / snapshot literature 的間接支持，但本文不宣稱其對任意數學 domain 成立。 ## Hypothesis 11.2 — Strong DVI Hypothesis 若 SDPE survivor contraction 不只增加 known-region hits，而真正降低： - effective branching； - proof route distance； - premise ambiguity； - candidate theorem freedom； - unresolved constraint dimension； 則可能存在 regime： $$ \boxed{ D_t^{\rm frontier}\downarrow } $$ 同時 $$ \boxed{ \sigma_t\uparrow. } $$ 這是「跨過某個全域量詞障礙後，後面的研究本身開始越算越快」的正式強版本。 它目前仍是 hypothesis。 --- # 12. Frontier Hardening：DVI 的主要反向力 Survivor space 變小不代表剩餘問題變容易。 可能出現： $$ \Omega_{t+1}\subsetneq\Omega_t, $$ 但所有容易 cases 都已排除，剩下的是： - singular cases； - measure-zero exceptional families； - high dependency-depth states； - large-parameter extremal configurations； - representation singular fibers； - global gluing obstructions。 因此： $$ \boxed{ D_{t+1}^{\rm frontier}>D_t^{\rm frontier} } $$ 完全可能。 本文稱此現象為： $$ \boxed{ \textbf{Frontier Hardening}. } $$ VeriSoftBench 中 transitive dependency closure 越大、proof success 越低的觀察，是這種 counterforce 的一個 formal-software domain 例子。 --- # 13. Phase Diagram 本文建議至少區分四種 proof-space regime。 ## Phase A — Exploration-Dominated - compiled hit rate 低； - survivor space 大； - routine / frontier discovery 均昂貴； - verification share 較低。 ## Phase B — Compilation-Dominated - known region 快速累積； - $D^{\rm resolve}$ 明顯下降； - frontier cost 未必下降； - proof trace / closure basis 開始回本。 ## Phase C — Discovery–Verification Inversion - routine discovery 已高度編譯； - 若 Strong DVI 成立，frontier discovery 也下降； - verification / coverage / maintenance 成為主要 share； - total cost 可以繼續下降。 ## Phase D — Frontier-Hardening / Exceptional-Survivor Regime - survivor domain 非常小； - 但剩餘結構極端、奇異或 global； - $D^{\rm frontier}$ 重新上升； - verification 也可能高昂。 因此 DVI 不必是最終永久相位。 Paper 06 的 measure-zero / exceptional survivor 理論會直接研究 Phase D 的可能性。 --- # 14. Linear Hit-Rate Phase Model 為了給出最小可解析模型，假設 compiled hit rate 為 $$ h\in[0,1]. $$ routine discovery cost： $$ \boxed{ D(h) = c_F-h\Delta c, } $$ 其中 $$ \Delta c=c_F-c_H>0. $$ 假設 verification / maintenance bundle 近似： $$ \boxed{ W(h) = W_0+\lambda h, } $$ 其中 $\lambda\ge0$。 ## Proposition 14.1 — Linear Verification-Dominance Threshold 當 $$ \Delta c+\lambda>0 $$ 時，verification dominance $$ W(h)>D(h) $$ 等價於： $$ \boxed{ h>h_*} $$ 其中 $$ \boxed{ h_* = \frac{c_F-W_0}{\Delta c+\lambda}. } $$ 若 $$ 0