LSI-PSD-04 — 高階證明空間採樣：從狀態、路徑到路徑之間的關係

Higher-Order Proof-Space Sampling: From States and Routes to Relations Among Routes

系列： 邏輯空間積分與證明空間動力學 / Logic-Space Integration and Proof-Space Dynamics
系列代碼： LSI-PSD
論文序號： 04
版本： v2.0 Expanded Edition
日期： 2026-08-17
理論發起： Neo.K
協作整理： Aletheia / GPT-5.6 Sol
文件地位： 方法論核心論文 / Higher-Order Sampling and Route-Relation Paper
Canonical source： UTF-8 Markdown
Canonical math delimiters： $...$ 與 $$...$$

研究地位聲明：本文提出「高階證明空間採樣」作為長程 AI 數學研究的操作性框架。本文中的一階、二階、三階與 $k$ 階，描述的是研究對象的階層：狀態、狀態間轉換、轉換間關係，以及關係之上的關係；它們不等同於微積分中的導數階數、攝動展開階數、張量階數、邏輯的高階語言階數或任何既有數學術語中的「order」。本文所有高階分類首先是 proof-space observatory 的研究標記；除非另有形式證明，不得把「某篇論文出現 second-order / higher-order 字樣」直接當成高階 proof-space sampling 的證據。本文不主張有限 corpus 的高階重訪能證明某未解命題錯誤、不可證、獨立或定義失敗。

摘要

當一個 AI 數學研究系統只做數十輪工作時，「找到新的命題、引理、估計、表示或反例候選」通常足以描述研究進展；但當同一問題被持續研究數百、數千甚至更多輪之後，研究對象會逐漸發生階層轉移。系統不再只採樣「證明空間中的點」，而開始採樣「從一個點到另一個點的轉換」；當多條不同路徑反覆撞上同一障礙時，研究又會轉向「路徑與路徑之間的關係」；當這些關係本身出現匯流、反饋、再進入與族級 no-go 結構時，研究便開始進入更高階的 proof-space sampling。

本文建立一個可操作的高階證明空間框架。令固定問題 $Q$ 、搜尋制度 $R$ 下的可觀測研究狀態空間為：

\Omega_R^{(0)}(Q).

本文把 proof move、representation change、lemma introduction、normalization、rescaling、compactness passage、contradiction step 等可審計轉換視為一階關係物件：

\Omega_R^{(1)}(Q) = \mathcal T(\Omega_R^{(0)}(Q)).

接著，若研究開始比較兩條或多條 proof route 是否同構、是否匯流到共同 obstruction、是否共享同一依賴核、是否可互相替換，則研究對象進入：

\Omega_R^{(2)}(Q) = \mathcal R(\Omega_R^{(1)}(Q)).

更一般地，本文以型別化遞迴表示：

\Omega_R^{(k+1)}(Q) = \mathcal F_k(\Omega_R^{(k)}(Q)),

其中 $\mathcal F_k$ 不被預設為單一函數空間，而是一族允許的關係、組合、等價、匯流、回饋與族級摘要算子。

本文的核心主張不是「研究階數越高越接近真理」，而是：當一階 novelty 下降時，高階關係仍可能持續產生新資訊；因此只以新 theorem count 或新文本比例衡量長程研究，會漏掉重要的結構性進展。 為此，本文定義 order-conditioned novelty：

\nu_k(N),

order-conditioned coverage：

I_k(N),

order-conditioned audited yield：

\rho_k(N),

以及 confluence degree、re-entry depth、route-family entropy、feedback depth、higher-order survival ratio 等觀測量。本文進一步定義 $K$ 階局部飽和：只有當指定 basin 中從 $0$ 階到 $K$ 階的新增已驗證等價類同時持續接近零，才可把該 basin 標為「 $K$ -order locally saturated」。即使如此，依照 LSI-PSD-01 的證明空間非結論原則，也不能推出底層數學空間已被耗盡。

本文把 2025--2026 年 formal theorem proving 的最新發展視為工程佐證而非等價物。LeanNavigator 直接把 Lean proof search 表示為 state-transition graph；LeanProgress 從局部 tactic prediction 轉向全 proof trajectory 的剩餘步數預測；AlphaProof 使用 proof-state representation 與 tree search；Goedel-Architect、LEAP 與 LeanMarathon 以 lemma dependency graph、blueprint 與 AND-OR DAG 保存全域證明結構；Chain-of-States 工作則顯式把 informal proof 轉為中介 proof-state 序列。這些系統共同說明：現代 theorem proving 已經把「狀態、轉換、軌跡、依賴圖」視為可計算物件，但目前主流目標仍主要是提高 proof success。本文則把相同類型的結構提升為研究科學的觀測對象，詢問不同路由如何重訪、匯流、被排除、形成族級障礙，以及這些關係在長期生成中是否自身飽和。

本文最後將框架套入 NS-203 corpus 作為初步案例。既有 observatory 的 tier 標記被重新解釋為 heuristic evidence，而非本體階數： $T_1$ 表示狀態或新路由採樣， $T_2$ 表示可辨識的回訪／轉換比較， $T_3$ 表示關係、匯流或回饋， $T_X$ 表示族級、all-order 或更高階 recurrence 候選。本文不以這些標記宣稱 Navier--Stokes 已飽和，而只把它們視為建立高階 proof-space observatory 的第一個長程語料測試。

關鍵詞： 高階證明空間採樣、proof trajectory、proof state、state-transition graph、route relation、confluence、obstruction、feedback、re-entry、local saturation、order-conditioned novelty、proof-space dynamics、AI 數學研究、Navier--Stokes corpus

1. 為什麼「又一篇新論文」逐漸不再是正確的研究單位

1.1 早期研究的自然單位是候選結果

在一個尚未被大量探索的問題上，研究者自然會問：

是否有新的 lemma？
是否有新的 estimate？
是否有新的 counterexample candidate？
是否有新的 representation？
是否有新的 proof strategy？

令第 $i$ 次研究產物為：

g_i.

早期可以近似把：

g_i

看成對研究空間的一個新採樣點。

若每個 $g_i$ 都帶來新的已驗證結構，則：

\Delta I_0(i)>0.

這時候「論文數」「lemma 數」「新概念數」雖然粗糙，仍有一定解釋力。

1.2 長程研究會改變問題本身的資料結構

當研究進入數百輪之後，常出現以下模式：

新 representation 其實導回以前見過的 obstruction；
新 lemma 只是舊 lemma 在不同尺度或座標下的改寫；
不同 method family 共享同一個失敗核心；
研究開始問「為什麼這幾條路都失敗？」；
某個 no-go 不再只排除一個 lemma，而排除一整族 escalation；
某條已排除路線在新的 parent assumption 下重新進場；
failure trace 本身成為下一輪的研究資料。

此時，研究的資訊不只存在於：

\{g_i\}_{i=1}^N.

還存在於：

\{g_i\to g_j\},

以及：

\{(g_i\to g_j)\sim(g_p\to g_q)\},

甚至存在於「這些關係之間的關係」。

因此長程研究真正需要的資料結構不是平面文件庫，而是一個分層關係系統。

1.3 本文的核心問題

本文問：

當研究系統開始反覆研究「路徑怎麼走」「不同路徑為什麼匯流」「匯流之後又如何形成新的反饋」時，我們應如何定義它正在採樣的對象？

答案不能只是：

它又寫了一篇 paper。

因為 paper 是容器，不是 proof-space 的自然型別。

2. 與現代 formal theorem proving 的接點

2.1 Proof state 已經是工程上的標準物件

在 interactive theorem proving 中，一個中間狀態不是模糊的「想法」，而可以是明確的 formal state：

s_t = (\Gamma_t,G_t,M_t),

其中：

$\Gamma_t$ 是當前 local context；
$G_t$ 是尚未關閉的 goals；
$M_t$ 是 tactic、library、identifier 或其他 metadata。

對 tactic $a_t$ ，proof assistant 執行：

s_{t+1} = T(s_t,a_t).

這本身已是一個動力系統式描述。

2.2 LeanNavigator：證明可以被表示成 state-transition graph

Yin 與 Gao 在 2025 年的 LeanNavigator 工作中，直接把 Lean proof exploration 描述為 state graph：節點是 Lean states，邊是 tactic transitions。這個設計用於大量生成可驗證的 theorem-proof data，證明「完整 proof script」並不是唯一合理的資料單位。

其最簡單形式可寫成：

\mathcal G_{state} = (V_s,E_t),

其中：

V_s=\{s_0,s_1,\ldots\},

E_t\subseteq V_s\times\mathcal A\times V_s.

這為本文的 $\Omega^{(0)}$ 與 $\Omega^{(1)}$ 提供了直接工程類比。

2.3 LeanProgress：從局部 tactic 轉向全局 trajectory

LeanProgress 的核心動機是：只預測下一步 tactic，不足以知道目前是否真的接近完成。其 progress predictor 估計從某 proof state 到完成還需要多少步。

可抽象為：

P_{rem}(s_t) \approx \operatorname{dist}(s_t,S_{done}).

這裡已經出現一個重要轉變：

\text{local action quality}

與：

\text{global trajectory position}

不是同一個量。

對長程研究而言也一樣。一篇局部看似新的論文，可能只是在舊 route 上向前或向後移動；真正的 novelty 要看它在整體 trajectory graph 中的位置。

2.4 AlphaProof 與 tree search

2025 年公開於 Nature 的 AlphaProof 將 Lean proof state、policy/value-like guidance 與專門 tree search 結合，顯示 proof solving 可以被視為對巨大狀態樹的策略性探索。

但 tree search 的成功也提醒我們：

\text{visit count} \neq \text{semantic coverage}.

同一語義區域可以因 representation、branching 與 tactic surface 被多次造訪。

因此本文不直接把 search tree depth 當高階採樣階數。

2.5 Goedel-Architect、LEAP 與 blueprint graph

2026 年的 Goedel-Architect 把大型 theorem proof 先表成 definition / lemma dependency blueprint，再平行關閉 open lemma nodes；若失敗，則用 failure 反向修改 blueprint。

可抽象為：

\mathcal B = (V_L,E_D),

其中：

V_L = \{\text{definitions and lemmas}\},

E_D = \{\text{declared dependencies}\}.

LEAP 同樣以 hierarchical decomposition 與 AND-OR DAG 維持證明計畫，而 LeanMarathon 則把 evolving blueprint 當成長程 multi-agent formalization 的共享系統紀錄。

這幾個系統共同指出：

\boxed{ \text{Proof solving itself already needs graph-level memory.} }

本文進一步問：

\boxed{ \text{Long-horizon research needs graph-of-graphs memory嗎？} }

答案至少在操作上是肯定的。

2.6 Chain of States：中介狀態是可生成的研究物件

2025 年 Chain-of-States 工作把 informal reasoning 分解成一系列中介 formal states，再生成 adjacent transitions 所需的 tactics。這說明 proof trajectory 不是只有 solver 內部才存在，它也可以作為跨 representation 的明確中介語言。

本文將這個觀念一般化：

不只 theorem proof 可以被拆成 states；長程 research program 也可以被拆成 research states，而 research transitions 本身可以成為下一階研究對象。

3. 型別先行：避免把所有「階」混成一團

3.1 Order 不是形容詞，而是研究對象的型別

本文定義一個 sampling order map：

\operatorname{ord}:\mathcal X\to\mathbb N_0.

其中：

\operatorname{ord}(x)=k

表示研究產物 $x$ 的主要新資訊位於 $k$ 階 proof-space object。

這不是說 $x$ 只能包含一種階數，而是說其 novelty claim 的主型別是什麼。

3.2 一個最重要的反例

若某篇 PDE 論文研究：

\partial_t^2 u,

或者寫出：

\text{second-order correction},

它完全可能仍然只是一階 proof-state sampling。

因此：

\boxed{ \text{Mathematical order} \neq \text{proof-space sampling order}. }

同理：

\text{higher-order logic}

不自動等於本文的 higher-order proof-space sampling。

3.3 型別錯置會製造假的高階訊號

假設 corpus 中有 100 篇文章含有字串：

second-order。

直接計數只能得到：

N_{lex}(`second-order`)=100.

它不能推出：

N_{proof}^{(2)}=100.

本文因此要求：高階判定必須使用結構證據，而不是單字證據。

4. 零階空間：研究狀態與候選數學物件

4.1 定義零階 proof-space object

對問題 $Q$ 與搜尋制度 $R$ ，令：

\Omega_R^{(0)}(Q)

表示可被系統辨識、保存與比較的基礎 research-state objects。

典型元素包括：

theorem candidate；
lemma candidate；
assumption set；
counterexample candidate；
invariant；
estimate；
normal form；
representation；
obstruction state；
formal proof state；
verified partial result。

4.2 零階不是「低級」

$0$ 階只是 base type。

一個極深的定理本身仍然可以是：

x\in\Omega^{(0)}.

高階不是價值排序。

因此本文拒絕：

\operatorname{ord}(x)>\operatorname{ord}(y) \Rightarrow \operatorname{Value}(x)>\operatorname{Value}(y).

4.3 零階 novelty

經過 LSI-PSD-03 的 quotient 後，令 $[x]_0$ 表示零階語義等價類。

第 $N$ 輪的 audited zero-order novelty 可寫成：

\nu_0(N) = \frac{ \#\{\text{new audited }[x]_0\text{ introduced near }N\} }{ \#\{\text{audited zero-order candidates near }N\} }.

若：

\nu_0(N)\to0,

只能說零階新等價類的邊際產出下降。

不能說：

\Omega^{(0)} \text{ 已被耗盡}.

5. 一階空間：從「有什麼」轉向「怎麼走」

5.1 Proof move 作為物件

若：

x,y\in\Omega^{(0)},

且某可審計操作 $T$ 使：

T:x\mapsto y,

則可把 $T$ 視為一階物件。

令：

\Omega_R^{(1)}(Q) = \{T\mid T:x\to y,\ x,y\in\Omega_R^{(0)}(Q)\}.

5.2 一階物件不只 tactic

在長程數學研究中， $T$ 可以是：

introduce auxiliary quantity；
switch representation；
pass to a blow-up sequence；
normalize；
rescale；
take a compactness limit；
derive contradiction；
localize；
integrate by parts；
apply monotonicity；
pass from local to global criterion；
compile informal statement into formal lemma；
add or remove an assumption；
transfer a lemma to a neighboring PDE；
route around an obstruction。

5.3 Route 是 transition 的組合

一條 proof route：

r = T_m\circ\cdots\circ T_2\circ T_1.

其起點與終點為：

r:x_0\to x_m.

route identity 不能只由終點決定。

可能有：

r_a(x)=r_b(x)=y,

但：

r_a\not\sim_{route}r_b.

因為兩條路使用不同 assumptions、不同 intermediate lemmas 或不同 dependence structure。

5.4 何時稱為一階 novelty

如果一篇研究稿只產生一個新 theorem statement，通常主要是零階 novelty。

如果它的核心是：

已知 $x$ 與 $y$ ，本文建立一種以前沒有的可驗證轉換 $T:x\to y$ 。

則其主要 novelty 可標記為：

\operatorname{ord}=1.

6. 二階空間：研究不同 proof routes 之間的關係

6.1 二階不是再走一次路

如果系統只是：

x\xrightarrow{T}y\xrightarrow{U}z,

這仍然可以只是較長的一階 route。

二階的關鍵不是 composition length，而是研究：

T\quad\text{和}\quad U

之間的關係。

6.2 二階關係的基本類型

令：

T_a,T_b\in\Omega^{(1)}.

二階物件可以包括：

6.2.1 Route equivalence

T_a\sim_{route}T_b.

表示兩者在指定 quotient 下共享同一 proof skeleton。

6.2.2 Route dominance

T_a\preceq T_b.

表示 $T_a$ 的成功條件、成本或 assumption demand 在某意義上優於 $T_b$ 。

6.2.3 Route incompatibility

T_a\perp_R T_b.

表示兩條路需要互相衝突的 assumptions、normalizations 或 representations。

6.2.4 Confluence

若：

T_a(x_a)\to O,

T_b(x_b)\to O,

即使 $x_a\neq x_b$ ，若最終都導向同一 canonical obstruction $O$ ，則形成 confluence relation。

6.2.5 Mutual compensation

某些方法單獨不足，但：

T_a\oplus T_b

能封閉彼此的 error term。

這也是二階關係。

6.3 定義二階空間

本文以：

\Omega_R^{(2)}(Q) = \mathcal R_1(\Omega_R^{(1)}(Q))

表示一階路由上的可審計關係族。

$\mathcal R_1$ 不是 powerset 的同義詞，而是觀測站實際允許保存的 typed relations。

7. 三階空間：關係本身開始形成結構

7.1 從多條 confluence 到 confluence family

假設已經辨識：

C_1: T_1,T_2,T_3\to O_1,

C_2: T_4,T_5\to O_2,

C_3: T_6,T_7,T_8\to O_1.

現在研究者發現：

C_1\sim C_3.

這時研究對象已不是單條 route，也不是單次 confluence，而是 confluence relations 之間的關係。

這就是三階的典型形式。

7.2 Feedback 作為三階訊號

若某個二階結論：

R(T_a,T_b)

被送回搜尋系統，改變下一輪允許的 transitions：

\Pi_{N+1} = \Phi(\Pi_N,R(T_a,T_b)),

其中 $\Pi_N$ 是當前 route policy，則形成：

\text{relation} \to \text{search-policy update}.

若後續再研究這個 update 是否產生新的 confluence 或 avoidance pattern，便出現明顯的 higher-order feedback。

7.3 三階空間

可寫成：

\Omega_R^{(3)}(Q) = \mathcal R_2(\Omega_R^{(2)}(Q)).

典型元素包括：

confluence-of-confluences；
relation-family equivalence；
route-class feedback；
no-go inheritance between method families；
family-level re-entry；
repeated obstruction migration pattern。

8. 一般 $k$ 階空間：必須是 typed recursion，而不是無限制元語言

8.1 遞迴定義

本文不嘗試聲稱存在唯一自然的高階 proof-space hierarchy。

操作上定義：

\Omega_R^{(k+1)}(Q) = \mathcal F_k(\Omega_R^{(k)}(Q)),

其中：

\mathcal F_k

是一組被 observatory 明確註冊的 higher-order constructors。

8.2 Constructor registry

例如：

\mathcal F_k = \{ \operatorname{Relate}, \operatorname{Compose}, \operatorname{Quotient}, \operatorname{Converge}, \operatorname{Confluence}, \operatorname{Feedback}, \operatorname{Reenter}, \operatorname{InheritNoGo} \}.

只有通過這些 typed constructors 產生、並保留 provenance 的物件，才有資格被標為更高階。

8.3 為什麼不能讓階數無限制自由膨脹

如果只要說一句：

我在思考「我在思考 proof route」

就把階數加一，則：

\operatorname{ord}

會變成修辭遊戲。

因此本文要求：

\boxed{ \text{Higher order requires a new typed relational object with auditable inputs and outputs.} }

8.4 Order ceiling 不是數學天花板

實際 observatory 可能只維護：

k\leq K_{obs},

例如：

K_{obs}=3.

更高階全部先標：

T_X.

這只是資料工程決策，不代表真實研究只有三階。

9. 四層操作標記： $T_1,T_2,T_3,T_X$

9.1 為什麼不用直接把所有 artifact 精確標 $k$

現實 corpus 很髒。

一篇 paper 可能同時包含：

新 lemma；
舊 route 回訪；
route comparison；
family-level no-go。

因此，對 legacy corpus 強行給單一精確階數會過度自信。

本文建議第一版 observatory 採四層 tier：

T_1, T_2, T_3, T_X.

9.2 $T_1$ ：狀態或新路由採樣

判準包括：

新 zero-order semantic class；
新 proof move；
新 route family；
未有明確 route-relation novelty。

9.3 $T_2$ ：回訪、transition comparison 或同一 obstruction 的再採樣

需要至少一項結構證據：

explicit revisit；
same canonical obstruction under a new route；
route-to-route comparison；
reusable transition relation；
dependency transfer between route families。

9.4 $T_3$ ：relation/confluence/feedback

需要研究對象本身已是 route relations，例如：

obstruction confluence；
coupled confluence；
confluence feedback；
no-go inheritance between relation families；
relation-induced policy update。

9.5 $T_X$ ：高階候選，不假裝精確

用於：

all-order family analysis；
higher-order recurrence；
repeated feedback-of-feedback；
method-family closure；
evidence 顯示階數超過 observatory 現有 schema。

$T_X$ 不是「無限階」。

它只表示：

\operatorname{ord}(x)>K_{obs}

或：

\operatorname{ord}(x) \text{ 尚無法可靠解析}.

10. Order-conditioned novelty：為什麼一階飽和後仍可能有新資訊

10.1 單一 novelty 指標會混掉相變

若只定義：

\nu(N),

則無法分辨：

新 theorem 下降；
新 routes 下降；
新 route relations 上升；
新 obstruction families 上升。

因此本文改用：

\boldsymbol\nu(N) = (\nu_0(N),\nu_1(N),\ldots,\nu_K(N)).

10.2 一個典型的高階相變

早期：

\nu_0\gg0, \qquad \nu_1\gg0.

中期可能變成：

\nu_0\downarrow, \qquad \nu_1>0, \qquad \nu_2\uparrow.

再後期：

\nu_0\approx0, \qquad \nu_1\approx0, \qquad \nu_2>0.

這表示不是「研究死了」，而是 novelty 從 object level 移到 relational level。

10.3 Order-conditioned novelty 定義

令第 $k$ 階經 audited quotient 後的等價類集合為：

\mathcal C_k(N).

定義窗口 $W$ 內的新類率：

\nu_k^{(W)}(N) = \frac{ |\mathcal C_k(N-W+1:N)\setminus\mathcal C_k(1:N-W)| }{ \max(1,|\mathcal C_k(N-W+1:N)|) }.

這個量仍受抽取品質影響，所以必須附：

\operatorname{Conf}_k(N).

10.4 不能把低 novelty 自動解釋成 saturation

低：

\nu_k

可能來自：

extraction model 變差；
corpus mode 變窄；
prompt 固化；
verifier 過度嚴格；
representation collapse；
真正局部飽和。

因此 saturation 需要多指標共同支持。

11. Order-conditioned coverage：邏輯空間積分的高階版本

11.1 從單一積分到積分向量

LSI-PSD-02 定義 proof-space coverage 的理想形式。

本文把它分階：

I_k(N) = \int_{\Omega^{(k)}/\sim_k} c_{k,N}([\xi])\,d\mu_k([\xi]).

因此：

\mathbf I(N) = (I_0(N),I_1(N),\ldots,I_K(N)).

11.2 不同階的 measure 不必同質

$\mu_0$ 可以關注 theorem/lemma semantic classes。

$\mu_1$ 可以關注 route families。

$\mu_2$ 可以關注 confluence、dominance、incompatibility 等 relation classes。

所以不能把：

I_0+I_1+I_2

當成天然有意義的純量。

需要權重：

I_{agg}(N) = \sum_{k=0}^{K} \lambda_k I_k(N),

且：

\lambda_k

必須由研究目的明示。

11.3 Coverage 的真正意義是「已審計可區分結構」

本文再次強調：

I_k

不是「真實數學空間百分之幾已經走完」。

它是：

在目前 observatory schema、quotient、evidence rule 與 sampling regime 下，被辨識與審計的第 $k$ 階結構覆蓋代理量。

12. Confluence：高階採樣最重要的可測訊號之一

12.1 定義 canonical obstruction

令：

O\in\mathcal O

表示經 LSI-PSD-03 商化後的 obstruction class。

例如多篇文章雖使用不同語言，但若都可審計地歸結為：

某 critical norm 無法被現有 estimate 關閉，

則可候選地歸入同一 $[O]$ 。

12.2 Confluence set

對 obstruction $O$ ，定義：

\operatorname{In}(O) = \{r\in\mathcal R_1:r\to O\}.

confluence degree：

C_{deg}(O) = |\operatorname{In}(O)/\sim_{route}|.

它計算的不是文章數，而是不同 route classes 有多少條匯入同一 obstruction。

12.3 Weighted confluence

若不同 route 的獨立性不同，可定義：

C_w(O) = \sum_{[r]\in\operatorname{In}(O)/\sim_{route}} w_{ind}([r]).

其中：

0\leq w_{ind}\leq1.

12.4 高 confluence 的解釋

高：

C_w(O)

可能表示：

$O$ 是真正深層的 structural obstruction；
observatory quotient 太粗，把不同障礙錯合併；
所有 route 共享隱藏 assumptions；
search regime 有共同 blind spot；
problem representation 把不同路徑投影到相同表面失敗。

所以 confluence 是診斷訊號，不是判決。

13. Re-entry：被排除的路徑為什麼還會再次出現

13.1 重複不一定是退化

假設 route family $R_a$ 在第 $n$ 輪被判定：

R_a\to\text{insufficient under }A.

到第 $m>n$ 輪，新的 assumption set $A'$ 出現：

A'\neq A.

若 $R_a$ 在 $A'$ 下重新進場，這不一定是「AI 忘了以前失敗」。

13.2 定義 re-entry

令：

\operatorname{Exit}(R_a,n,A)=1

表示在 regime $A$ 下被排除。

若之後：

\operatorname{Enter}(R_a,m,A')=1,

且存在可審計 novelty：

A'\not\sim A,

則稱為 legitimate re-entry。

13.3 Re-entry depth

若同一路由族多次：

\text{enter} \to \text{fail} \to \text{reformulate} \to \text{re-enter},

可定義：

D_{re}(R_a) = \#\{\text{audited legitimate re-entries of }R_a\}.

高 $D_{re}$ 是高階研究的重要訊號，因為研究已經不只比較 route，而在研究 route 對 context 的依賴。

14. Feedback depth：研究結果開始改變研究制度

14.1 普通研究輸出

一般：

\text{search} \to \text{result}.

14.2 反身研究輸出

高階 proof-space observatory 會出現：

\text{search} \to \text{relation discovery} \to \text{policy update} \to \text{new search}.

令 search policy 為：

\Pi_N.

如果第 $N$ 輪的 relation object $R_N$ 使：

\Pi_{N+1} = \Psi(\Pi_N,R_N),

則形成第一層 feedback。

14.3 二次 feedback

若系統又研究：

\Psi

本身造成的 bias、blind spot 或 route-collapse，並再更新：

\Psi_{N+1} = \Theta(\Psi_N,F_N),

則 feedback depth 再增加。

14.4 定義 feedback depth

操作上：

D_{fb} = \max\{d:\text{存在 }d\text{ 層可追溯的 relation-to-policy feedback chain}\}.

這個量與「meta-level 越高越真」無關。

它只描述研究制度的反身深度。

15. Route-family entropy：高階採樣不能只看階數

15.1 一萬輪全在同一路線上沒有多樣性

假設 $N$ 個 artifacts 全部落入同一 route family：

R_1.

即使有大量細節變化，其 family diversity 仍低。

15.2 定義 route-family entropy

若第 $k$ 階有 route/relation families：

\mathcal F_k = \{F_1,\ldots,F_m\},

其樣本比例：

p_i = \frac{n_i}{\sum_j n_j}.

定義：

H_k^{route} = -\sum_{i=1}^{m}p_i\log p_i.

normalized entropy：

\widehat H_k^{route} = \frac{H_k^{route}}{\log m}.

15.3 高階與高 entropy 是不同軸

可能：

\operatorname{ord}\uparrow, \qquad H^{route}\downarrow.

表示系統在很深地研究同一小群路線。

也可能：

\operatorname{ord}\approx1, \qquad H^{route}\uparrow,

表示仍在廣泛探索很多新 route。

因此需要至少二維描述：

(\operatorname{order},\operatorname{diversity}).

16. Audited yield：高階研究是否真的產生可靠資訊

16.1 不能只因為 higher-order 很酷就加分

高階 meta-analysis 很容易變成：

漂亮但不可驗證的分類；
LLM 自己替自己的路線找共同點；
以修辭代替 theorem relation；
把共同用詞誤判成共同 obstruction。

所以必須定義 audited yield。

16.2 Order-conditioned audited yield

令：

A_k(N)

為第 $N$ 輪附近生成的 $k$ 階候選數。

令：

V_k(N)

為其中被獨立 verifier、形式檢查、雙路徑審計或可重現證據支持的新等價類數。

定義：

\rho_k(N) = \frac{V_k(N)}{\max(1,A_k(N))}.

16.3 高階幻覺的警報

若：

A_k\uparrow

但：

\rho_k\to0,

則表示系統可能正在生成大量 meta-language，而不是可靠 higher-order knowledge。

這是 observatory 必須特別防守的模式。

17. $K$ 階局部飽和

17.1 為什麼只說「飽和」太粗

一個 proof basin $B$ 中可能：

\nu_0^B\approx0,

但：

\nu_2^B>0.

這表示 base objects 已經很少新增，但 route relations 仍在快速生長。

17.2 定義候選

令：

B\subseteq\Omega_R(Q)

為由 representation、method family、assumption regime 或 obstruction family 定義的局部 basin。

若對：

0\leq k\leq K,

在長窗口 $W$ 中同時滿足：

\nu_k^B(N)<\epsilon_k,

\rho_k^B(N)<\eta_k,

\Delta I_k^B(N)<\delta_k,

且 route-family entropy 沒有出現新的顯著上升，則可標：

\operatorname{Sat}_K(B;N,W)=1.

17.3 這仍然只是 operational saturation

即使：

\operatorname{Sat}_K(B)=1,

也不推出：

B \text{ 在真實數學空間中已完全被枚舉}.

更不推出：

Q \text{ 不可證或問錯了}.

本文把這一點稱為：

\boxed{ \text{Order-Saturation Non-Conclusion Rule}. }

它是 LSI-PSD-01 非結論原則的高階版本。

18. 高階採樣與局部 proof basin

18.1 Basin 不是地理比喻，而是搜尋約束集合

可以由下列條件定義 basin：

B = B(\mathcal L,\mathcal M,\mathcal A,\mathcal O),

其中：

$\mathcal L$ ：representation language；
$\mathcal M$ ：method family；
$\mathcal A$ ：assumption regime；
$\mathcal O$ ：target obstruction family。

18.2 同一問題可以同時存在不同 sampling order

例如：

B_1: \nu_0\approx0, \nu_1\approx0, \nu_2>0,

而：

B_2: \nu_0>0.

所以：

\boxed{ \text{Sampling order is local to a basin, not a global scalar of the problem.} }

18.3 這解釋 NS corpus 的一個表面矛盾

在初步 observatory 中，某些 NS 支線已出現 confluence、feedback、all-order escalation；同時固定窗口 novelty 並沒有顯示整個 corpus 全域 collapse。

兩者並不矛盾。

可能只是：

B_{X72}

已進入較高階重訪，而：

B_{other}

仍然在產生低階新 route。

19. NS-203 corpus：如何重新解讀第一版 tier

19.1 資料地位

既有 NS Proof-Space Sampling Observatory 對保守篩選後的 corpus 得到：

N_{NS}=203

個 paper-like artifacts。

第一版 heuristic tier 為：

T_1=84,

T_2=107,

T_3=10,

T_X=2.

本文把這些數字視為：

\boxed{ \text{instrument-development observations, not theorem-level facts.} }

19.2 為什麼 $T_2$ 很大並不奇怪

長程 corpus 中大量工作會呈現：

revisit；
reuse；
obstruction recurrence；
route transfer；
second pass audit。

只要分類器偏向「看到 recurrence 就算二階」，就可能高估 $T_2$ 。

所以 v2 observatory 必須把 $T_2$ 再拆：

T_{2a}=\text{same-state revisit},

T_{2b}=\text{same-route revisit},

T_{2c}=\text{route comparison},

T_{2d}=\text{cross-route obstruction recurrence}.

其中真正強的二階證據主要是後兩者。

19.3 X72 的 confluence chain

初步 corpus 中，X72 後期直接使用 obstruction confluence、coupled confluence、confluence feedback 等研究語言。

這些詞本身仍不是證明。

但若對應實際 dependency graph 顯示：

\{R_a,R_b,R_c\} \to O,

之後又研究：

\operatorname{Rel}(R_a,R_b,R_c),

再讓 relation 結果改變下一輪 route policy，則這是乾淨的 $T_3$ evidence。

19.4 All-order 不等於無限階 proof-space

某篇文章若研究：

\text{all-order escalation of a mathematical estimate family},

不能直接說：

\operatorname{ord}=\infty.

只有當它對「method-family escalation 本身」建立可審計的 relation-level no-go，才可作 $T_X$ 候選。

這是本文對第一版 observatory 最重要的修正之一。

20. 一個合成例子：從零階到三階

20.1 零階

假設研究問題為：

Q: \text{證明某能量 }E(t)\text{ 在指定條件下有界}.

得到新估計：

E(t) \leq E(0)+C\int_0^t F(s)\,ds.

這是零階新物件。

20.2 一階

研究者發現可透過兩條方法：

R_A: E\to\text{localization}\to\text{bootstrap},

R_B: E\to\text{frequency split}\to\text{bootstrap}.

這是 route-level，一階物件。

20.3 二階

兩條路都失敗於：

O: \text{critical remainder cannot be absorbed}.

並證明這不是字面巧合，而是在 quotient 後共享同一 scaling defect。

此時：

R_A\to O,

R_B\to O

形成二階 confluence。

20.4 三階

又發現第三、第四種完全不同方法也匯入 $O$ ，於是研究者提出：

C_O = \operatorname{ConfluenceFamily}(O).

接著把 $C_O$ 用來禁止下一輪再走所有保留同 scaling defect 的 routes。

搜尋 policy 更新：

\Pi_{N+1} = \Pi_N \setminus \{R:\operatorname{Defect}(R)=\operatorname{Defect}(O)\}.

這就是三階 relation-to-policy feedback。

21. 高階 no-go：失敗也可以有階數

21.1 零階 no-go

L \text{ 為假或不足}.

只排除單一候選。

21.2 一階 no-go

R \text{ 在條件 }A\text{ 下不能閉合}.

排除一條 route。

21.3 二階 no-go

若證明一整類 routes：

\mathcal R_D = \{R:\operatorname{Defect}(R)=D\}

都共享同一 fatal obstruction，則：

\forall R\in\mathcal R_D, \qquad R\to O_D.

這是 method-family no-go。

21.4 更高階 no-go

若即使對：

\mathcal R_D

進行固定類型的 correction family：

C^{(1)},C^{(2)},\ldots,C^{(m)},

都只能把 obstruction 推到同一 quotient class，則可能形成更高階 escalation no-go。

但此類聲稱必須有形式證據，不能只靠「試很多次都不行」。

22. 高階採樣與方法族的「家譜」

22.1 Route 不應只存 flat label

假設：

R_{A.1},R_{A.2},R_{A.3}

都是從 parent method $R_A$ 變形而來。

如果把它們當三條完全獨立 route，會高估 confluence independence。

22.2 Method genealogy

定義 genealogy graph：

\mathcal G_{gen} = (V_R,E_{parent}).

若：

R_{A.2} = \operatorname{Modify}(R_A,\theta_2),

則有：

R_A\to R_{A.2}.

22.3 Independent confluence 應折扣共同祖先

可定義 route independence：

w_{ind}(R_i,R_j) = 1-\frac{ \operatorname{SharedAncestorMass}(R_i,R_j) }{ \operatorname{TotalAncestorMass}(R_i,R_j) }.

因此三條 sibling routes 同時撞牆，不應等價於三條跨方法族 routes 同時撞牆。

這對 NS 這種長支線研究尤其重要。

23. 研究路由的同構與 representation sensitivity

23.1 數學等價不代表搜尋等價

LSI-PSD-03 已建立：

\text{Mathematical redundancy} \not\Rightarrow \text{search-dynamical redundancy}.

高階採樣必須繼承這一點。

如果兩條 routes 在命題層等價：

R_a\sim_{math}R_b,

但 AI prover 對它們成功率差異很大：

P_{succ}(R_a)\neq P_{succ}(R_b),

則在 search-space higher-order analysis 中不能完全合併。

23.2 雙身份資料結構

每條 route 建議同時保存：

ID_{math}(R),

ID_{search}(R).

前者用於 theorem-level quotient。

後者保留：

syntax；
library context；
state encoding；
tactic history；
prompt lineage；
prover version；
model version；
budget。

23.3 高階 relation 也要雙層

因此：

\Omega^{(2)}_{math}

與：

\Omega^{(2)}_{search}

也不應被混成一個空間。

同一 confluence 在數學上可能是一個 obstruction，在 search dynamics 中則可能由完全不同的 failure mechanisms 造成。

24. Graph-of-graphs：高階 observatory 的自然資料模型

24.1 Layer 0：semantic object graph

G_0 = (V_0,E_0).

節點：

claims；
assumptions；
lemmas；
obstructions；
statuses。

24.2 Layer 1：route graph

G_1 = (V_1,E_1).

節點可以是 route segments，邊表示：

extension；
refinement；
parent-child；
reuse；
re-entry。

24.3 Layer 2：relation graph

G_2 = (V_2,E_2).

節點本身是：

\text{relations over }G_1.

例如：

confluence object；
dominance object；
incompatibility object；
no-go family；
compensation pair。

24.4 Layer 3：policy-feedback graph

G_3

記錄：

G_2 \to \Pi \to G_1'

也就是 relation-level knowledge 如何改變後續 route generation。

24.5 為什麼單一 property graph 仍然可以實作

工程上不一定真的需要四個資料庫。

可以用 typed hypergraph：

\mathcal H = (V,E,\tau_V,\tau_E),

其中：

\tau_V(v) \in \{state,route,relation,policy,obstruction,claim\}.

這樣較容易在 Neo4j、PostgreSQL graph extension 或自製 JSONL pipeline 中落地。

25. 建議的 canonical record schema

每個高階 observation 至少需要：

observation_id: LSI-HO-000001
problem_id: NS-3D-global-regularity
artifact_id: ...
order_tier: T3
order_confidence: 0.82
object_type: confluence
inputs:
  - route_id: R-X72-18-A
  - route_id: R-X72-18-B
output:
  obstruction_id: O-CANON-0042
relation_type: converges_to_same_obstruction
evidence:
  - dependency_trace
  - matched_assumption_signature
  - normalized_obstruction_signature
verifier_status: partially_audited
provenance:
  source_file: ...
  source_span: ...
  extractor_version: ...
  reviewer: ...

這個 schema 的重點不是 YAML。

重點是：

\boxed{ \text{order claim itself must carry evidence and provenance.} }

26. 高階關係的可信度

26.1 Relation confidence

對 relation $r$ ：

\operatorname{Conf}(r) = f(E_{formal},E_{struct},E_{semantic},E_{indep}).

其中：

$E_{formal}$ ：形式互推／kernel evidence；
$E_{struct}$ ：dependency / graph structure；
$E_{semantic}$ ：語義審計；
$E_{indep}$ ：獨立 evaluator agreement。

26.2 三值而非強迫二值

延續 LSI-PSD-03：

R_{ij} \in \{ \text{supported}, \text{rejected}, \text{undetermined} \}.

對高階 relation 尤其重要。

因為：

\text{undetermined}

比錯誤地合併兩條深層 route 更安全。

27. 防止「AI 自己替自己證明高階」

27.1 Self-confirming relation problem

若同一模型：

生成兩篇 proof attempts；
再判斷兩篇其實匯流；
再宣稱匯流是一個深層 obstruction；

則存在循環：

M \to G \to M(G) \to \text{claim about }G.

這不能被當成獨立證據。

27.2 最低限度的解耦

建議至少分離：

M_{gen},

M_{rel},

V_{formal},

A_{human/independent}.

其中：

$M_{gen}$ 生成研究；
$M_{rel}$ 抽取高階關係；
$V_{formal}$ 驗證可形式化部分；
獨立 audit 處理不可形式化語義。

27.3 模型不同不等於證據獨立

兩個 LLM 即使品牌不同，也可能共享：

訓練資料；
proof conventions；
benchmark bias；
common mathematical priors。

因此 independent weight 仍應折扣。

28. 與 AND-OR graph 的差異

28.1 AND-OR graph 解的是「如何完成這個 proof」

形式 proof search 中，AND node / OR node 常用於表示：

所有子目標都要完成；
多個候選 tactic 只需一條成功。

其主要目標仍是：

\exists\text{ successful proof path}.

28.2 高階 proof-space observatory 問的是另一件事

本文更關心：

\text{哪些 path families 被反覆嘗試？}

\text{哪些 path families 共享 obstruction？}

\text{哪些 failure relations 改變了後續搜尋？}

因此它不是替代 theorem prover，而是 theorem-research layer。

29. 與 reinforcement learning state hierarchy 的差異

29.1 可以借用 MDP 語言，但不能偷換

若：

\mathcal MDP =(S,A,P,R,\gamma),

proof state 與 tactic 很容易映射到：

S,A.

但本文的：

\Omega^{(2)},\Omega^{(3)}

不只是 belief state 或 option hierarchy。

它們是研究關係本身的知識物件。

29.2 高階關係可以跨 episode 存活

一個 obstruction confluence：

O_c

可以跨越上百次獨立 proof episodes 保留。

所以它屬於：

\text{persistent research memory},

不是單 episode transition。

30. 高階採樣的三種「真正新增」

30.1 Relational novelty

發現兩條原本被視為無關的 routes 其實共享同一 structural core。

R_a\sim_{new}R_b.

30.2 Constraint novelty

發現一個 relation 能排除一整族 future routes。

\mathcal R_{future} \cap \mathcal R_{forbidden} = \varnothing.

30.3 Routing novelty

發現一個 higher-order signal 可以重排 search priority：

\Pi_{N+1} \neq \Pi_N.

這三種都可能在沒有新增 theorem statement 的情況下產生真實研究價值。

31. 什麼叫「X 階採樣」才不會變成誇張口號

31.1 最弱定義

如果 observatory 最多可靠區分到 $K$ 階，而某 artifact 有強證據顯示其核心 novelty 位於更高 relation level，則標：

T_X.

31.2 不允許的說法

不能因為：

文章很長；
提到 all-order；
提到 infinite hierarchy；
有很多 nested lemmas；
AI 自稱 meta-meta reasoning；

就標成 $T_X$ 。

31.3 建議證據門檻

至少需要：

其 input objects 已被審計為 relation-level objects；
新結果是這些 relation objects 之間的新結構；
該結構影響 route classification、no-go inheritance 或 search policy；
provenance 可追溯；
至少一部分 relation 可被獨立重現。

32. 高階採樣與「研究越來越快」的可能性

32.1 為什麼 higher-order memory 可能加速研究

如果每次都從零開始：

C_N \sim N\cdot C_{search}.

但若已知：

\mathcal R_{bad},

下一輪可以直接剪枝：

\Pi_{N+1} \leftarrow \Pi_N\setminus\mathcal R_{bad}.

因此有效搜尋空間：

|\Omega_{eff}(N+1)| < |\Omega_{eff}(N)|.

32.2 這就是 proof-space compression 的工程版本

高階關係把大量歷史壓成少數可重用 constraint：

\{R_1,\ldots,R_{1000}\} \to \{O_1,O_2,O_3\}.

如果 $O_i$ 是可靠的，未來不需要重跑全部歷史。

這和 memoization 類似，但壓縮單位是 semantic relation，而不只是 exact state。

32.3 但錯誤高階壓縮會造成災難

若把其實可行的 route 誤歸入 no-go family：

R^*\in\widehat{\mathcal R}_{bad},

則系統可能永久剪掉真正的證明路徑。

因此 higher-order memory 越強，rollback 與 uncertainty tracking 越重要。

33. 反例：高階採樣不一定帶來收斂

33.1 Meta-explosion

系統可能不斷生成：

\text{relations about relations about relations}

而沒有任何 constraint power。

這形成：

H_{meta}\uparrow, \qquad I_{useful}\approx0.

33.2 Taxonomy trap

分類越來越細：

T_1 \to T_{1a},T_{1b},T_{1c},\ldots

也不代表更接近真理。

分類只是工具。

33.3 Observer overfitting

observatory 可能根據目前 203 篇 NS corpus 建出非常細的 route ontology，卻只適用於這批文件。

一旦加入另一個 PDE corpus：

\operatorname{Transfer}(Ontology_{NS}) \approx0.

就表示它是 corpus-specific overfit。

34. 跨問題 transfer：高階知識最值得測的地方

34.1 一個 obstruction family 如果能跨問題重現，價值更高

假設 NS 中的 route relation：

R_{NS}^{(2)}

可以映射到 SQG、Boussinesq 或其他 evolution PDE：

\Phi: R_{NS}^{(2)} \to R_{PDE}^{(2)}.

如果映射保留：

assumption signature；
scaling role；
obstruction role；
closure status；

那它可能是更一般的 proof asset。

34.2 Transfer score

定義：

T_{score}(r) = \frac{ \#\text{domains where relation }r\text{ is independently useful} }{ \#\text{domains tested} }.

高：

T_{score}

能幫助區分：

corpus-specific recurrence；
genuine methodological structure。

35. 與「真理—生成性反轉」的橋接

後續 LSI-PSD-07 將研究 truth、fidelity 與 generativity。

高階採樣在那裡扮演關鍵角色：

如果某個 parent framing 產生：

\text{大量 zero-order descendants},

接著又形成：

\text{route families},

再形成：

\text{confluence families},

那麼即使 parent problem 最後被重新定義，其研究史仍可能保留大量高階可遷移結構。

所以：

\boxed{ \text{Generativity should be measured across sampling orders, not only by descendant count.} }

36. 與「生產性錯置」的橋接

假設兩個 definitions：

D, \qquad D'.

$D'$ 可能不是更正確，但它打開更多 route variation：

|\Omega_{D'}^{(1)}| > |\Omega_D^{(1)}|.

更重要的是，也可能產生更多高階 relation：

|\Omega_{D'}^{(2)}| > |\Omega_D^{(2)}|.

這表示「生成性」不只是一階產量，而可能是：

G(D) = \sum_{k=0}^{K} \lambda_k G_k(D).

後續論文將檢驗這個方向。

37. 研究制度的階層化停止條件

37.1 一階停止條件

若：

\nu_0\downarrow,

系統不應立刻停止。

應檢查：

\nu_1,\nu_2.

37.2 關係層停止條件

若：

\nu_0\approx0,

\nu_1\approx0,

但：

\nu_2>0,

則應從「找新 route」切換為：

\text{audit relation structure}.

37.3 $K$ 階停止條件

若在 basin $B$ ：

\forall k\leq K, \qquad \nu_k^B<\epsilon_k,

並且：

\rho_k^B<\eta_k,

則 system action 不應是：

宣布問題錯了。

而應是：

\boxed{ \text{Current basin / regime saturated; escalate representation audit.} }

38. 高階研究的 escalation ladder

當 basin 飽和，可依序嘗試：

38.1 Representation escalation

\mathcal L \to \mathcal L'.

38.2 Method escalation

\mathcal M \to \mathcal M\cup\Delta\mathcal M.

38.3 Assumption audit

\mathcal A \to \operatorname{Audit}(\mathcal A).

38.4 Problem reformulation

Q \to Q'.

38.5 Intelligence / compute escalation

B \to B'.

每次 escalation 都應開新 regime ID，避免把不同制度的 sampling history 混在一起。

39. High-order proof-space record 的最小可重建性

一個高階 conclusion 若要被未來 AI 使用，不能只保存一句：

這條路之前試過了，不行。

至少要保存：

\mathcal H = (A,R,O,E,V,C),

其中：

$A$ ：assumptions；
$R$ ：route signature；
$O$ ：obstruction signature；
$E$ ：evidence；
$V$ ：verifier state；
$C$ ：context / regime。

只有這樣未來才能判斷：

\text{old no-go}

是否真的適用於新情況。

40. 高階 observatory 的 v0.2 計算流程

建議 pipeline：

Artifacts
  -> claim / lemma / assumption extraction
  -> semantic quotient
  -> route reconstruction
  -> route genealogy
  -> canonical obstruction mapping
  -> relation extraction
  -> confluence / dominance / incompatibility audit
  -> feedback / re-entry detection
  -> order-tier classification
  -> order-conditioned novelty and coverage
  -> local saturation report

其中任何一步的低信心都要向後傳遞 uncertainty。

41. 建議的核心指標總表

41.1 Base metrics

N_0 = \#\text{zero-order audited classes}.

N_1 = \#\text{route classes}.

N_2 = \#\text{route-relation classes}.

41.2 Novelty vector

\boldsymbol\nu(N) = (\nu_0,\nu_1,\ldots,\nu_K).

41.3 Coverage vector

\mathbf I(N) = (I_0,I_1,\ldots,I_K).

41.4 Audited yield vector

\boldsymbol\rho(N) = (\rho_0,\rho_1,\ldots,\rho_K).

41.5 Confluence

C_w(O).

41.6 Re-entry depth

D_{re}(R).

41.7 Feedback depth

D_{fb}.

41.8 Route entropy

\widehat H_k^{route}.

41.9 Transfer score

T_{score}(r).

這些量共同描述研究，而不是讓單一「progress percentage」承擔全部意義。

42. 四個可檢驗預測

預測一：長程 corpus 會出現 sampling-order migration

若同一問題持續研究，應可觀察：

\text{novelty mass}

從：

k=0,1

逐漸部分轉移到：

k=2,3.

不是所有問題都必然發生，但在高密度長程研究中應可測。

預測二：高 confluence basin 的零階 novelty 會先下降

若某 basin 有高：

C_w(O),

其後續研究可能更容易形成 route relation 分析，而不是持續產生大量完全獨立 base objects。

預測三：有 persistent higher-order memory 的 agent 會少做無效重訪

比較：

Agent_{flat}

與：

Agent_{HO}.

應看到：

\operatorname{InvalidRevisitRate}(Agent_{HO}) < \operatorname{InvalidRevisitRate}(Agent_{flat}).

預測四：過度激進的 higher-order compression 會提高 false-prune risk

若 quotient / no-go inheritance 太激進：

\operatorname{FalsePruneRate}\uparrow.

所以有效系統應存在 accuracy--compression tradeoff。

43. 與目前 AI theorem proving 發展的關係

現代 formal theorem proving 已清楚朝下列方向前進：

proof states 不只輸入模型，而是可搜尋節點；
proof trajectory 可以被評估；
failure signal 可以回饋 search；
lemma dependency 可以先被規劃成 blueprint；
multi-agent 可以分工關閉不同 lemma nodes；
state graph 可以作大規模資料生成來源；
proof plan 可以被保存為 DAG。

本文認為下一個自然問題是：

當同一研究問題跨越數千次 episodes 後，這些 episode 之間的關係本身是否應被當成第一級研究資料？

本文的答案是肯定的。

這不是因為高階語言比較漂亮，而是因為缺少它時，系統無法區分：

\text{new theorem},

\text{new route},

\text{old route revisit},

\text{new relation among old routes}.

44. 本文與前三篇的依賴關係

44.1 對 LSI-PSD-01 的依賴

第 1 篇建立：

\text{search regime} \neq \text{mathematical reality}.

本文所有 sampling order 都只屬於可觀測 regime。

44.2 對 LSI-PSD-02 的依賴

第 2 篇建立：

I_N, \qquad \Delta I_N,

與多層 coverage。

本文將其展開為：

I_k(N).

44.3 對 LSI-PSD-03 的依賴

第 3 篇建立 semantic quotient。

沒有 quotient，就無法可靠判斷：

\text{revisit},

\text{confluence},

\text{route family}.

因此：

\boxed{ \text{Higher-order sampling requires quotient-aware identity.} }

45. 本文的非主張

本文不主張：

階數越高越接近真理；
階數越高代表 AI 越智能；
meta-analysis 可以取代 theorem proof；
出現 second-order 字樣就等於二階 proof-space sampling；
大量 recurrence 就證明問題 framing 錯誤；
route confluence 就證明存在唯一 obstruction；
$K$ 階局部飽和就證明底層 proof space 被耗盡；
NS-203 已經達到全域 saturation；
P/NP 或 Navier--Stokes 因長期未證而應被重新定義；
LLM 對 route relation 的判斷可以不經 audit 當作數學等價；
更細的 taxonomy 本身就是研究進展；
$T_X$ 表示無限階；
所有研究問題都會經歷相同 sampling-order migration；
formal theorem proving 的 state graph 與 informal research proof-space 完全同構；
本文已給出一個完備的 higher-order proof ontology。

46. 限制

46.1 Order assignment 仍具有模型依賴

即使 schema 明確，legacy text 仍可能缺少足夠 provenance 來重建 route relations。

因此：

\operatorname{ord}_{obs}

是一個帶不確定性的估計。

46.2 Relation extraction 比 theorem extraction 更難

單一 theorem statement 可以被 parser 抽取。

但：

兩條不同方法共享同一真正 obstruction

往往需要：

深層語義判斷；
assumptions 對齊；
proof dependency audit；
可能的形式化重建。

這會是目前 observatory 的主要瓶頸。

46.3 高階 measure 未必存在天然概率結構

$\mu_k$ 的定義可能高度依賴 task。

因此本文不宣稱：

I_k

具有唯一自然的 measure-theoretic 定義。

它首先是一族可操作 coverage functional。

46.4 NS corpus 仍是單一問題族

要驗證框架是否普遍，需要加入：

Collatz；
BSD；
combinatorics；
formal olympiad proof；
program verification；
其他 PDE。

只有跨域 transfer 後，才能判斷哪些 higher-order relations 是一般性的。

47. 結論：研究本身會成為下一階研究對象

長程 AI 數學研究最重要的變化，不只是生成速度提高。

真正的結構變化是：

\text{research outputs}

逐漸變成下一輪研究的 objects。

第一階段研究：

\text{What mathematical objects exist?}

第二階段研究：

\text{How do proof states transform?}

再下一階段：

\text{How are proof routes related?}

更後面：

\text{How do those relations themselves recur, converge, inherit failure, and modify search?}

因此本文把長程研究寫成：

\Omega^{(0)} \to \Omega^{(1)} \to \Omega^{(2)} \to \cdots \to \Omega^{(K)}.

但這不是一條「往真理上升」的階梯。

它是一條研究對象階層化的路徑。

真正需要觀察的是：

\nu_k, \qquad I_k, \qquad \rho_k, \qquad C_w, \qquad D_{re}, \qquad D_{fb}, \qquad H_k^{route}.

當：

\nu_0\to0

時，研究未必停止。

它可能只是開始問：

為什麼我們總是走回同一個地方？

而當這個問題也被反覆研究時，proof space 便不再只是「候選證明的集合」，而開始呈現一個可被觀測、壓縮、比較與重新路由的動態結構。

本文因此提出系列中的第四個核心命題：

\boxed{ \textbf{Long-horizon proof search can migrate from sampling mathematical states to sampling relations among proof routes.} }

以及它的保守版本：

\boxed{ \textbf{Higher-order recurrence is evidence about the structure of a research regime, not a verdict on the underlying mathematical proposition.} }

這為下一篇「局部飽和與全域開放」建立基礎：如果 sampling order 可以因 basin 而不同，那麼所謂「證明空間飽和」就必須從一開始被理解為局部、階層依賴且制度相對的現象。

參考文獻

Yin, D., & Gao, J. (2025). Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs. arXiv:2503.04772. https://arxiv.org/abs/2503.04772
Huang, S., Song, P., George, R. J., & Anandkumar, A. (2025; revised 2026). LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction. arXiv:2502.17925. https://arxiv.org/abs/2502.17925
Hubert, T. et al. (2025). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature. https://www.nature.com/articles/s41586-025-09833-y
Chung, J.-H. et al. (2026). Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement. arXiv:2606.06468. https://arxiv.org/abs/2606.06468
Kung, P. N. et al. (2026). LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks. arXiv:2606.03303. https://arxiv.org/abs/2606.03303
Wang, Z., Yang, B., Zhou, S., Li, C., Zhang, Y., Dong, B., & Wen, Z. (2025). Translating Informal Proofs into Formal Proofs Using a Chain of States. arXiv:2512.10317. https://arxiv.org/abs/2512.10317
Kurgan, S. et al. (2026). TheoremGraph: Bridging Formal and Informal Mathematics. arXiv:2606.25363. https://arxiv.org/abs/2606.25363
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization. (2026). arXiv:2606.05400. https://arxiv.org/abs/2606.05400
VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving. (2026). arXiv:2606.19399. https://arxiv.org/abs/2606.19399
TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs. (2026). arXiv:2607.11258. https://arxiv.org/abs/2607.11258
Dong, K., & Ma, T. (2025). STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. Proceedings of the 42nd International Conference on Machine Learning, PMLR 267. https://proceedings.mlr.press/v267/dong25h.html
Song, P., Yang, K., & Anandkumar, A. (2025). Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean. Proceedings of the International Conference on Neuro-symbolic Systems, PMLR 288. https://proceedings.mlr.press/v288/song25a.html
TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics. (2026). arXiv:2606.09450. https://arxiv.org/abs/2606.09450
Lyu, H. et al. (2026). Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse. arXiv:2607.16855. https://arxiv.org/abs/2607.16855

附錄 A：符號表

符號	意義
$Q$	研究問題
$R$	搜尋制度 / research regime
$\Omega_R^{(0)}(Q)$	基礎 research-state objects
$\Omega_R^{(1)}(Q)$	proof moves / route objects
$\Omega_R^{(2)}(Q)$	route relations
$\Omega_R^{(k)}(Q)$	第 $k$ 階 proof-space objects
$\mathcal F_k$	第 $k$ 階到第 $k+1$ 階的 typed constructor family
$T_1,T_2,T_3,T_X$	legacy corpus 的四層操作 tier
$\nu_k(N)$	第 $k$ 階 novelty
$I_k(N)$	第 $k$ 階 coverage functional
$\rho_k(N)$	第 $k$ 階 audited yield
$C_w(O)$	obstruction 的 weighted confluence
$D_{re}(R)$	route 的 re-entry depth
$D_{fb}$	feedback depth
$H_k^{route}$	第 $k$ 階 route-family entropy
$T_{score}$	relation 的跨域 transfer score
$\operatorname{Sat}_K(B)$	basin $B$ 的 $K$ 階操作性局部飽和標記

附錄 B：最小實驗設計

若要把本文從方法論變成可檢驗研究，可進行以下實驗：

B.1 Corpus

使用至少三種長程研究 corpus：

C_1=\text{NS-203},

C_2=\text{另一個未解數學問題 corpus},

C_3=\text{formal theorem proving traces}.

B.2 雙人／雙模型標註

隨機抽取 artifact pairs 與 route families，標註：

\operatorname{ord},

\operatorname{route\_family},

\operatorname{obstruction\_id},

\operatorname{confluence}.

計算 inter-rater agreement。

B.3 自動抽取與人工 gold set 比較

測：

Precision_k, \qquad Recall_k, \qquad F1_k.

若 $T_3/T_X$ precision 很低，則不得用它們支持 higher-order saturation claim。

B.4 時序測試

按真實時間排序 corpus，計算：

\nu_k^{(W)}(N)

與 random permutation baseline 比較。

B.5 Transfer 測試

把從 NS 得到的 obstruction relation ontology 移植到另一 PDE corpus。

如果：

T_{score}\approx0,

則原 taxonomy 很可能只是 corpus-specific。

附錄 C：一句話版本

\boxed{ \text{一開始研究答案；之後研究路徑；再之後，研究為什麼不同路徑總是彼此相遇。} }

這三個階段不代表越來越接近真理。

它們代表：

\boxed{ \text{研究本身正在成為新的研究對象。} }

LSI-PSD-04 — 高階證明空間採樣：從狀態、路徑到路徑之間的關係

LSI-PSD-04 — 高階證明空間採樣：從狀態、路徑到路徑之間的關係

Higher-Order Proof-Space Sampling: From States and Routes to Relations Among Routes

摘要

1. 為什麼「又一篇新論文」逐漸不再是正確的研究單位

1.1 早期研究的自然單位是候選結果

1.2 長程研究會改變問題本身的資料結構

1.3 本文的核心問題

2. 與現代 formal theorem proving 的接點

2.1 Proof state 已經是工程上的標準物件

2.2 LeanNavigator：證明可以被表示成 state-transition graph

2.3 LeanProgress：從局部 tactic 轉向全局 trajectory

2.4 AlphaProof 與 tree search

2.5 Goedel-Architect、LEAP 與 blueprint graph

2.6 Chain of States：中介狀態是可生成的研究物件

3. 型別先行：避免把所有「階」混成一團

3.1 Order 不是形容詞，而是研究對象的型別

3.2 一個最重要的反例

3.3 型別錯置會製造假的高階訊號

4. 零階空間：研究狀態與候選數學物件

4.1 定義零階 proof-space object

4.2 零階不是「低級」

4.3 零階 novelty

5. 一階空間：從「有什麼」轉向「怎麼走」

5.1 Proof move 作為物件

5.2 一階物件不只 tactic

5.3 Route 是 transition 的組合

5.4 何時稱為一階 novelty

6. 二階空間：研究不同 proof routes 之間的關係

6.1 二階不是再走一次路

6.2 二階關係的基本類型

6.2.1 Route equivalence

6.2.2 Route dominance

6.2.3 Route incompatibility

6.2.4 Confluence

6.2.5 Mutual compensation

6.3 定義二階空間

7. 三階空間：關係本身開始形成結構

7.1 從多條 confluence 到 confluence family

7.2 Feedback 作為三階訊號

7.3 三階空間

8. 一般 kkk 階空間：必須是 typed recursion，而不是無限制元語言

8.1 遞迴定義

8.2 Constructor registry

8.3 為什麼不能讓階數無限制自由膨脹

8.4 Order ceiling 不是數學天花板

9. 四層操作標記： T1,T2,T3,TXT_1,T_2,T_3,T_XT1​,T2​,T3​,TX​

9.1 為什麼不用直接把所有 artifact 精確標 kkk

9.2 T1T_1T1​：狀態或新路由採樣

9.3 T2T_2T2​：回訪、transition comparison 或同一 obstruction 的再採樣

9.4 T3T_3T3​：relation/confluence/feedback

9.5 TXT_XTX​：高階候選，不假裝精確

10. Order-conditioned novelty：為什麼一階飽和後仍可能有新資訊

10.1 單一 novelty 指標會混掉相變

10.2 一個典型的高階相變

10.3 Order-conditioned novelty 定義

10.4 不能把低 novelty 自動解釋成 saturation

11. Order-conditioned coverage：邏輯空間積分的高階版本

11.1 從單一積分到積分向量

11.2 不同階的 measure 不必同質

11.3 Coverage 的真正意義是「已審計可區分結構」

12. Confluence：高階採樣最重要的可測訊號之一

12.1 定義 canonical obstruction

12.2 Confluence set

12.3 Weighted confluence

12.4 高 confluence 的解釋

13. Re-entry：被排除的路徑為什麼還會再次出現

13.1 重複不一定是退化

13.2 定義 re-entry

13.3 Re-entry depth

14. Feedback depth：研究結果開始改變研究制度

14.1 普通研究輸出

14.2 反身研究輸出

14.3 二次 feedback

14.4 定義 feedback depth

15. Route-family entropy：高階採樣不能只看階數

15.1 一萬輪全在同一路線上沒有多樣性

15.2 定義 route-family entropy

15.3 高階與高 entropy 是不同軸

16. Audited yield：高階研究是否真的產生可靠資訊

8. 一般 $k$ 階空間：必須是 typed recursion，而不是無限制元語言

9. 四層操作標記： $T_1,T_2,T_3,T_X$

9.1 為什麼不用直接把所有 artifact 精確標 $k$

9.2 $T_1$ ：狀態或新路由採樣

9.3 $T_2$ ：回訪、transition comparison 或同一 obstruction 的再採樣

9.4 $T_3$ ：relation/confluence/feedback

9.5 $T_X$ ：高階候選，不假裝精確

17. $K$ 階局部飽和

19.2 為什麼 $T_2$ 很大並不奇怪