下一步到底為什麼是下一步：Arrow Legitimacy 與 Same-Parent Path

系列：形式封閉與過程完備：AI 數學證明的下一步問題
Paper 02
作者：Neo.K / EveMissLab Research Series
版本：v0.1 — 2026-09-11

機構： EveMissLab／一言諾科技有限公司
日期： 2026-09-11

摘要

在大量形式證明、存在性證明與 AI 自動定理搜尋中，一個常見而不容易被直接看見的問題是：證明可以反覆產生「下一個合法對象」，卻沒有證明這個對象真的是上一個對象的合法下一步。形式上，研究者往往證明：

\forall n,\quad \exists S_{n+1}\;P_n(S_n,S_{n+1}),

或甚至：

\forall n,\forall S_n\in X_n,\quad \exists S_{n+1}\in X_{n+1}\;P_n(S_n,S_{n+1}),

然後在語言上把這些局部存在結果描述成一條連續演化路徑。然而，真正的動態過程通常要求更多：下一狀態必須保留父狀態的歷史、約束、守恆量、分支身份與生成關係；不能在每一階段重新選取一個滿足局部條件但不屬於同一條 parent-consistent branch 的 witness。

本文將「下一步為什麼是下一步」形式化為 Arrow Legitimacy 問題，提出 Same-Parent Path、Branch Identity、History Preservation、No-Hidden-Reset、Successor Compatibility 與 Arrow Composition 等條件。本文指出：

\boxed{ \text{Local successor existence} \neq \text{same-parent continuation} }

以及：

\boxed{ \text{same-parent continuation} \neq \text{globally coherent trajectory} }

本文進一步分析 classical choice、induction、compactness、diagonal selection 與 AI proof search 如何在形式上產生一串彼此可接受的 witnesses，卻可能在過程語義上發生 branch switching。最後，本文提出 Arrow Audit Schema，作為後續處理 bounded/unbounded、completion operator 與 Navier–Stokes 個案審計的基礎。

關鍵詞

下一步、箭頭合法性、Same-Parent Path、branch identity、trajectory、witness substitution、history dependence、hidden reset、AI 數學、形式化證明、induction、choice、proof graph

1. 問題不是「有沒有下一個狀態」，而是「它是不是這一個狀態的下一步」

設狀態空間為：

\mathcal S.

一個最弱的逐步存在命題可以寫成：

\forall S\in\mathcal S,\quad \exists S'\in\mathcal S,\quad P(S,S').

如果 $P$ 只表示「 $S'$ 滿足下一階段需要的某些條件」，那麼這個命題只能保證：

\text{Next-stage witness exists}.

它不自動保證：

\text{$S'$ 是由 $S$ 合法生成}.

更不保證：

\text{$S'$ 與 $S$ 屬於同一條歷史分支}.

因此本文把「下一步」分解成兩個不同概念：

\operatorname{CandidateNext}(S,S')

與：

\operatorname{LegitimateNext}(S,S').

第一個只要求 $S'$ 滿足下一階段的局部條件。

第二個要求 $S'$ 同時保留 $S$ 所承載的歷史、身份與生成義務。

因此：

\boxed{ \operatorname{CandidateNext}(S,S') \not\Rightarrow \operatorname{LegitimateNext}(S,S') }

這就是 Arrow Legitimacy 問題的起點。

2. 把箭頭本身升格成數學物件

普通證明通常把：

S\to S'

當成一個語言上的縮寫。

本文則把箭頭寫成：

\alpha:S\rightsquigarrow S'.

其中 $\alpha$ 不是單純的真值，而是一個包含 transition information 的物件。

定義一個箭頭：

\alpha= ( S, S', \mathcal R, \mathcal I, \mathcal H, \mathcal C ),

其中：

$\mathcal R$ ：生成規則；
$\mathcal I$ ：必須保持的 invariants；
$\mathcal H$ ：歷史相容條件；
$\mathcal C$ ：局部約束與 admissibility conditions。

箭頭合法性定義為：

\operatorname{ArrowValid}(\alpha)=1

當且僅當：

\mathcal R(S)=S'

或至少：

\mathcal R(S,S')

成立，且：

\operatorname{Preserve}_{\mathcal I}(S,S'),

\operatorname{HistoryCompatible}_{\mathcal H}(S,S'),

\operatorname{ConstraintValid}_{\mathcal C}(S,S').

因此真正的下一步不只是：

P(S').

而是：

P(S') \land \operatorname{ArrowValid}(S\rightsquigarrow S').

3. Same-Parent Path

設：

S_0

為起始狀態。

一條有限路徑：

\pi_n=(S_0,S_1,\ldots,S_n)

若滿足：

\forall k<n,\quad \operatorname{ArrowValid}(S_k\rightsquigarrow S_{k+1}),

則稱為 Same-Parent Finite Path。

若存在無限 trace：

\tau:\mathbb N\to\mathcal S,

滿足：

\tau(0)=S_0

以及：

\forall n,\quad \operatorname{ArrowValid}(\tau(n)\rightsquigarrow\tau(n+1)),

則稱 $\tau$ 為 Same-Parent Path。

記作：

\operatorname{SPP}(\tau)=1.

這個條件直接排除一類常見錯覺：

\forall n,\quad \exists S_n\in X_n

並不等價於：

\exists\tau,\quad \forall n,\; \tau(n)\in X_n \land \operatorname{ArrowValid}(\tau(n)\rightsquigarrow\tau(n+1)).

換句話說：

\boxed{ \text{Layerwise existence} \neq \text{pathwise existence} }

4. Branch Identity：為什麼每一層都有解仍可能不是同一條解？

考慮一棵分支樹。

第 $n$ 層合法節點集合為：

L_n.

每個節點 $x\in L_n$ 可能有自己的 child set：

\operatorname{Child}(x)\subseteq L_{n+1}.

即使：

L_n\neq\varnothing

對所有 $n$ 都成立，也可能存在：

x_n\in L_n

使每一個 $x_n$ 分別合法，但：

x_{n+1}\notin\operatorname{Child}(x_n).

也就是：

x_0,\;x_1,\;x_2,\ldots

是一串合法節點，卻不是一條 path。

因此我們引入 branch identity：

\beta(S)\in\mathcal B,

其中 $\mathcal B$ 是 branch identifier space。

對合法 successor：

S\rightsquigarrow S',

要求：

\beta(S')\succeq\beta(S),

也就是 $S'$ 必須是 $S$ 的 branch extension，而不是另一條分支的合法節點。

最簡單的情況可寫成：

\operatorname{Parent}(S')=S.

更一般地，若狀態是壓縮表示，則要求：

\operatorname{History}(S) \preceq \operatorname{History}(S').

5. Hidden Reset：最常被忽略的 branch switching

很多證明沒有顯式寫：

S_n\to S_{n+1}.

而是每一階段執行：

S_{n+1} := \operatorname{Choose} \{x\mid Q_{n+1}(x)\}.

如果 $Q_{n+1}$ 只描述第 $n+1$ 階需要的性質，而沒有強制：

x\in\operatorname{Child}(S_n),

那麼這一步實際上不是 successor。

它是 reset：

S_n \xrightarrow{\operatorname{Reset}} \widetilde S_{n+1}.

其中：

\widetilde S_{n+1}

只是在新的可行域裡重新挑出的 witness。

本文把這種操作稱為 Hidden Reset Operator：

\mathcal R_n: \mathcal S \to \mathcal S,

但其輸出不真正依賴輸入狀態的 branch identity。

形式上，如果：

\mathcal R_n(S)=\mathcal R_n(S')

對大量不同 $S,S'$ 都成立，或 $\mathcal R_n$ 只依賴 stage index 而不是 parent state，則應進一步檢查它是否只是：

\operatorname{StageWitnessSelector}(n).

Hidden Reset 不一定使 theorem 錯誤。

但若 theorem 的語義宣稱「同一系統逐步演化」，則 Hidden Reset 必須被禁止或明確揭露。

6. Witness Substitution

設原來有：

P(S_n).

下一步需要證：

Q(S_n).

但直接從 $S_n$ 推不出來。

證明可能改做：

\exists \widehat S_n, \quad P(\widehat S_n)\land Q(\widehat S_n),

然後把後續全部改用 $\widehat S_n$ 。

若 proof statement 只需要：

\exists S_n,

這可能完全合法。

但若整個 proof narrative 說的是：

S_0\to S_1\to\cdots\to S_n\to S_{n+1},

那麼：

S_n\rightsquigarrow \widehat S_n

本身就是一個需要審計的新箭頭。

如果這個箭頭沒有保存歷史，則實際發生：

\text{branch substitution}.

因此定義：

\operatorname{WitnessSubstitute}(S,\widehat S)

並要求：

\operatorname{EquivalentHistory}(S,\widehat S)

或：

\operatorname{AdmissibleReplacement}(S,\widehat S).

否則不能把 substitution 當成「同一個對象的改寫」。

7. 局部 successor theorem 不等於全域路徑 theorem

一個常見且較強的條件是：

\forall n,\forall S_n\in A_n, \quad \exists S_{n+1}\in A_{n+1}, \quad R_n(S_n,S_{n+1}).

這比：

\forall n,\exists S_n

強很多。

在有適當選擇原理的形式系統中，從給定 $S_0$ 可以構造一條無限 relation-compatible sequence。

但仍然存在至少三個不同層級：

\text{Relational successor existence},

\text{Selected infinite trace},

\text{Effective generated trace}.

第一層：

\forall S_n\exists S_{n+1}.

第二層：

\exists\tau,\quad R_n(\tau(n),\tau(n+1)).

第三層：

\exists F,\quad \tau(n+1)=F(n,\tau(n)).

其中 $F$ 可構造或可計算。

所以：

\boxed{ \text{successor existence} \neq \text{successor mechanism} }

這個區分對 AI theorem proving 特別重要，因為 AI 很容易把第一層語言描述成第三層。

8. 下一步合法性的最低條件

本文提出以下最低條件。

對：

S\rightsquigarrow S',

要求至少有：

8.1 Parent Dependence

S'

必須依賴 $S$ ，而不是只依賴 stage index。

形式上：

S'\in\Phi(S).

8.2 Constraint Preservation

若：

\mathcal I(S)

是 invariants，則要求：

\mathcal I(S').

更強地，應有：

\mathcal I(S)\Rightarrow\mathcal I(S').

8.3 History Preservation

令：

H(S)

為歷史摘要。

則：

H(S)\preceq H(S').

8.4 No Hidden Reset

不存在未聲明的：

S\to\widehat S

使後續在新 branch 上重新開始。

8.5 Local Causality

若過程宣稱是 forward process，則 $S'$ 不應依賴未來狀態：

S_{n+k}, \quad k>0,

除非 theorem 明確使用 boundary-value 或 global construction ontology。

8.6 Arrow Composability

若：

S_0\rightsquigarrow S_1

及：

S_1\rightsquigarrow S_2,

則 composite arrow：

S_0\rightsquigarrow S_2

必須在同一 semantic category 中可解釋。

若第二步偷偷更換 ontology，則 composition 失敗。

9. Local Causality 與 Global Construction 必須分開

不是所有數學證明都需要 forward causality。

例如 boundary value problem 可以一次指定：

u(0)=a, \qquad u(1)=b,

再求中間解。

這完全合法。

問題出現在研究者先採用：

\text{global object construction}

但在科學語言上把結果描述成：

\text{forward generation}.

因此本文要求先標記 proof ontology。

至少分成：

\mathsf{Forward},

\mathsf{Boundary},

\mathsf{GlobalExistential},

\mathsf{InverseConstructive},

\mathsf{CompletionBased}.

若 proof 屬於：

\mathsf{GlobalExistential},

則它可以合法地一次選完整 object。

但不能無條件推論：

\mathsf{Forward}.

因此：

\boxed{ \text{global consistency} \neq \text{forward causality} }

10. History State：若下一步依賴過去，就不能只保存當前表面狀態

有些系統不是 Markovian。

即：

S_{n+1}

不只依賴：

S_n,

還依賴：

S_0,\ldots,S_n.

那麼真正的 state 應該升格成：

\widehat S_n = (S_0,\ldots,S_n)

或某個足夠的歷史壓縮：

M_n = \operatorname{Compress}(S_0,\ldots,S_n).

此時 successor 應寫成：

M_{n+1} = F(M_n,S_{n+1}).

如果形式化只保留表面狀態 $S_n$ ，卻在後面偷偷使用完整歷史中的資訊，那麼 proof state representation 本身就不完整。

因此：

\boxed{ \text{state sufficiency} }

也是 Arrow Legitimacy 的前提。

定義：

\operatorname{SufficientState}(S_n)

表示所有未來合法 transition 所需資訊都已被 $S_n$ 表示。

11. Branch Switching 的四種典型模式

11.1 Stagewise Witness Switching

每一階：

\exists x_n

各自成立，但沒有：

R(x_n,x_{n+1}).

11.2 Constraint Refresh

第 $n$ 階使用約束：

C_n,

第 $n+1$ 階重新選一個：

C_{n+1}

但：

C_{n+1}

不保證包含或延續 $C_n$ 。

11.3 Future-Compatible Reselection

為了讓後面的 theorem 成立，重新選前面的 witness。

即：

S_n

本來已固定，但看到 $S_{n+k}$ 的需求後又改成：

\widehat S_n.

如果 theorem 宣稱 forward construction，這是顯著的 semantic violation。

11.4 Completion-Induced Identity Change

有限階段 object 是：

S_n,

但 completion 後的 object：

S_*

不再是：

\lim S_n

或同一種 object，而是另一個 realization。

此時：

S_n\to S_*

需要新的 identity bridge。

這一點將在 Paper 04 詳細展開。

12. Induction 為什麼容易讓人產生「路徑已經存在」的錯覺？

數學歸納法證：

P(0)

和：

P(n)\Rightarrow P(n+1).

便得到：

\forall n,\;P(n).

如果 $P(n)$ 只是：

\exists S_n\;Q_n(S_n),

那麼歸納得到的是：

\forall n,\exists S_n\;Q_n(S_n).

它沒有自動得到：

\exists(S_n), \quad \forall n,\; Q_n(S_n) \land R_n(S_n,S_{n+1}).

若 inductive hypothesis 本身包含完整 prefix：

\exists(S_0,\ldots,S_n), \quad \forall k<n,\;R_k(S_k,S_{k+1}),

那麼情況不同。

此時 induction 確實是在延長同一條 finite path。

因此一個重要審計問題是：

Inductive hypothesis 保存的是單一 stage witness，還是整條 path prefix？

這可以寫成：

\operatorname{IH}_{\text{node}}

與：

\operatorname{IH}_{\text{path}}.

其中：

\boxed{ \operatorname{IH}_{\text{path}} > \operatorname{IH}_{\text{node}} }

在 process proof 中通常更安全。

13. Classical Choice 與 Same-Parent Path

若我們有：

\forall x\in X,\quad \exists y\in X,\quad R(x,y),

classical dependent choice 可以給一條：

x_0,x_1,x_2,\ldots

滿足：

R(x_n,x_{n+1}).

這種情況比單純：

\forall n\exists x_n

好得多，因為 relation compatibility 被保留。

然而，仍需區分：

\text{relation-compatible selected path}

與：

\text{effective forward-generated path}.

Choice 可以保證存在某條 path。

它未必提供：

F(x_n)=x_{n+1}

的可計算 procedure。

所以如果 theorem 只要求 existence，choice 可以足夠。

如果 theorem 宣稱 algorithmic generation，choice 不足。

因此：

\boxed{ \text{Dependent Choice can close path existence, but not necessarily path computation.} }

這個區分同時避免兩種錯誤：

第一種是把 choice 一律視為「假」。

第二種是把 choice 得到的 path 一律視為「已經可執行」。

兩者都不準確。

14. 一個 Arrow Audit Schema

對 proof graph 中每一個關鍵箭頭：

A\xrightarrow{\alpha}B,

本文建議至少檢查以下欄位：

\operatorname{Source}(\alpha)=A,

\operatorname{Target}(\alpha)=B,

\operatorname{Rule}(\alpha),

\operatorname{ParentDependency}(\alpha),

\operatorname{InvariantPreservation}(\alpha),

\operatorname{HistoryPreservation}(\alpha),

\operatorname{BranchIdentity}(\alpha),

\operatorname{NoFutureDependency}(\alpha),

\operatorname{NoHiddenReset}(\alpha),

\operatorname{Composability}(\alpha).

若 theorem 宣稱計算性，再追加：

\operatorname{Computability}(\alpha),

\operatorname{Termination}(\alpha),

\operatorname{ResourceBound}(\alpha).

因此可以把一個 proof 從單純 DAG：

V,E

升格成：

G_{\mathrm{proof}} = (V,E,\Lambda),

其中 $\Lambda$ 為每個 edge 的 semantic metadata。

15. Arrow Closure

Paper 01 提出了 Theorem Closure。

本文進一步定義 Arrow Closure。

若 proof 中所有對結論必要的 transition：

\alpha_1,\ldots,\alpha_k

皆滿足：

\operatorname{ArrowValid}(\alpha_i)=1,

且不存在未聲明的 identity-changing transition，則稱：

\operatorname{AC}(\Pi)=1.

因此：

\operatorname{TC}(\Pi)=1

與：

\operatorname{AC}(\Pi)=1

是不同性質。

一個 theorem 可以有：

\operatorname{TC}=1,

但因為 statement 本身沒有要求 process semantics，而具有：

\operatorname{AC}=0

或：

\operatorname{AC}

根本未定義。

這不是 kernel error。

這是 proof ontology 未被完整指定。

16. Same-Parent Closure

進一步，若存在 trace：

\tau,

使：

\operatorname{SPP}(\tau)=1,

並且所有 theorem conclusion 都是針對同一條 $\tau$ 建立，而不是在不同 branch witnesses 間切換，則稱 proof 達成：

\operatorname{SPC}(\Pi)=1.

其中 SPC 表示 Same-Parent Closure。

因此有：

\boxed{ \operatorname{TC} \neq \operatorname{AC} \neq \operatorname{SPC} }

在很多傳統 theorem 中，只需要 TC。

在動態過程 theorem 中，至少應檢查 AC。

若 theorem 宣稱一條完整演化，則應進一步檢查 SPC。

17. 對 AI theorem proving 的直接意義

AI proof search 很容易採用如下策略：

\text{current obligation} \to \text{find any witness satisfying it} \to \text{continue}.

這在局部非常有效。

但如果每次都重新解當前 obligation，而沒有保留：

\text{branch identity},

\text{history state},

\text{parent constraints},

那麼系統可能得到：

\text{a sequence of locally valid proofs}

卻不是：

\text{a globally coherent construction}.

因此 future AI mathematician 不只需要 proof memory，還需要：

\boxed{ \text{trajectory memory}. }

也就是記住：

\text{我現在證明的 object 是哪一條 branch 的第幾步？}

而不是只記住：

\text{目前有哪些 theorem 可用？}

18. 「下一步到底是下一步」的強版本

最弱版本只問：

\exists S_{n+1}.

較強版本問：

S_{n+1}\in\Phi(S_n).

更強版本問：

S_{n+1}=F(S_n).

再更強版本問：

F

是否 preserving、computable、stable。

因此可以形成一個層級：

\mathsf{N}_0: \quad \exists S_{n+1},

\mathsf{N}_1: \quad \exists S_{n+1}\in\Phi(S_n),

\mathsf{N}_2: \quad S_{n+1}=F(S_n),

\mathsf{N}_3: \quad F\text{ preserves required invariants},

\mathsf{N}_4: \quad F\text{ is effectively realizable}.

不同研究問題可以要求不同層。

但必須明確標示自己到底證到了哪一層。

19. 一個實用判準：如果拿掉 stage label，下一步還能被認出來嗎？

很多 proof 的 successor 實際只靠：

n

而不是：

S_n.

因此可使用一個簡單測試。

假設把 stage label $n$ 隱藏，只給 current state $S_n$ 。

問：

能否從 $S_n$ 與合法規則辨認或生成下一步？

若不能，而必須額外知道：

\text{「現在是第 73 階，所以請選第 74 階要求的 witness」},

則這個 construction 可能更接近：

\text{externally scheduled family}

而不是：

\text{self-contained dynamics}.

因此可以定義：

\operatorname{StageFreeStep}(S_n)

作為更強的 generative criterion。

這不是所有數學 construction 都需要。

但如果宣稱 process autonomy，這是一個很有價值的測試。

20. Arrow Legitimacy 與反事實構造

某些 existence proof 會先假設：

H

然後在 $H$ 下建立一連串狀態：

S_0^H\to S_1^H\to\cdots.

最後推出：

\bot.

這是正常反證法。

但若在不同 stage 使用不同 strengthened hypothesis：

H_0,H_1,H_2,\ldots

並且：

H_{n+1}

不是由：

H_n

合法推得，而是為了下一階方便而重新加入，則 proof graph 可能出現：

\text{hypothesis drift}.

因此 Arrow Audit 也必須包含：

\operatorname{AssumptionMonotonicity}.

即：

\Gamma_n \to \Gamma_{n+1}

時，需要知道新增的前提到底是：

已證 theorem；
definition unfolding；
admissible strengthening；
conditional branch；
還是未被證明的新假設。

這一點對長鏈 AI-generated proof 尤其重要。

21. 與 Paper 01 的關係

Paper 01 提出：

\text{Theorem Closure} \neq \text{Process Completeness}.

本文進一步指出 Process Completeness 的第一個必要條件就是：

\boxed{ \text{Arrow Closure}. }

若：

S_n

與：

S_{n+1}

之間的箭頭沒有被完整定義，那麼即使兩個節點各自都具有完美 theorem certificates，也不能自動把它們連成同一條過程。

所以：

\text{Certified nodes} + \text{uncertified arrows}

不等於：

\text{certified trajectory}.

這可濃縮為：

\boxed{ \text{A proof graph is only as process-complete as its edges.} }

22. 核心命題

本文提出以下六個核心命題。

第一：

\boxed{ \text{A valid next-stage object is not necessarily a valid successor.} }

第二：

\boxed{ \text{Layerwise existence is weaker than pathwise existence.} }

第三：

\boxed{ \text{Pathwise existence is weaker than generative continuation.} }

第四：

\boxed{ \text{Witness substitution must itself be treated as an arrow.} }

第五：

\boxed{ \text{Hidden reset can preserve theoremhood while destroying process identity.} }

第六：

\boxed{ \text{A process proof must certify edges, not only nodes.} }

23. 結論

「下一步」在數學文字中常常只是一個語言習慣。

然而，只要 theorem 宣稱的是演化、生成、逐步修正、迭代逼近、尺度遞進或同一系統的長時間行為，「下一步」就不應只是修辭。

它必須有數學身份。

因此，對：

S_n\to S_{n+1},

真正需要問的是：

\boxed{ \text{Why is this state the successor of this parent?} }

而不只是：

\boxed{ \text{Can we find some state satisfying the next theorem?} }

這兩句話的差異，就是 Arrow Legitimacy。

當形式數學進入 AI 大規模 proof search 時，這個問題將更加重要。因為 AI 可以極高速地找到下一個可用 witness，也可以極高速地完成局部 theorem closure；若系統缺乏 trajectory identity，它反而更容易在大規模搜尋中產生一條「每一步都對，但不是同一條路」的 proof narrative。

因此，下一代 proof audit 不只要驗：

\text{node correctness}.

還必須驗：

\text{edge correctness},

\text{branch consistency},

\text{history preservation},

以及：

\text{same-parent closure}.

這就是「下一步到底為什麼是下一步」的形式版本。

24. 系列後續

下一篇將進入：

Paper 03 — 有限、無界與無限：Boundedness、Unbounded Quantification 與 Completion

核心問題將從箭頭轉向量詞與極限：

\boxed{ \forall M<\infty,\;\exists x_M }

到底證明了什麼？

以及：

\boxed{ \text{arbitrarily large finite} \neq \text{completed infinite object} }

我們將進一步分析 boundedness、unboundedness、completed infinity、diagonal quantification 與 finite-to-limit transition 的合法性。