Variable Ontology Audit for Mathematical Proof Search

Residual-Freedom Reduction as a Proof-Search Architecture

Series: Constraint-Generated Numerical and Symbolic Computation
Paper 05
Status: Proof-search methodology and case-study synthesis
Language: zh-TW
Depends on:

Paper 01 — Variablehood by Residual Constraint Domain
Paper 02 — Constraint-Generated Sequence Representation
Paper 03 — Decimal-Free and Generator-First Real Numbers
Paper 04 — Constraint-Aware Information Encoding and Residual Bits

Scope: theorem variables, residual domains, proof DAGs, witness search, next-separating-constraint policy, AI theorem proving, BSD normalization case study, proof-state compression

作者： Neo.K
機構： EveMissLab／一言諾科技有限公司
日期： 2026-10-08（整理日期；原稿未標註日期）
版本： 原稿未標註（本次整理版）

摘要

傳統 theorem proving 通常以：

lemma 數量；
proof depth；
search tree size；
tactic steps；
symbolic transformations；

描述證明進度。

但這些量不一定直接反映核心困難是否真的下降。

一個 proof system可以產生大量正確 lemmas，而主要未知變量的 admissible domain幾乎完全沒變。

本文提出一個不同的 proof-search ontology：

\boxed{ \text{proof progress} = \text{reduction of residual admissible freedom}. }

對每一個主要 theorem variable $x$ ，定義：

\mathcal V_x = \mathcal A_x(\mathcal K)/{\sim},

其中：

$\mathcal A_x(\mathcal K)$ 是目前 constraints 下的 admissible domain；
$\sim$ quotient 掉 gauge、coordinate、basis、representation等假自由度；
$\mathcal V_x$ 是真正尚未 closure 的 residual variable domain。

proof search的核心任務不再只是：

下一個 lemma 是什麼？

而是：

\boxed{ \text{下一個 constraint 應該消除哪個 residual variable direction？} }

本文提出 Variable Ontology Audit、Residual Variable Graph、Constraint Gain、Proof Search Priority、Variablehood Witness Search、Closure Certificate、Theorem Obligation Compression、Proof-State Sequence 與 Reopening Rules。

同時，本文以 BSD rank- $2$ calibration / normalization 架構作為案例，展示一個看似單一的 unknown scalar 如何被拆成：

common normalization character；
quotient transport；
period / de Rham pairing；
determinant comparison；
finite lattice defect；
residual flat torsor；

並在多輪約束後被壓縮成少數明確 theorem obligations。

本文不宣稱 BSD 已被證明。

案例的目的只是展示：

\boxed{ \text{opaque symbolic unknown} \to \text{explicit residual-domain graph} \to \text{finite proof obligations}. }

最後，本文提出一個 AI proof-search runtime的最小抽象：

\boxed{ \text{Variable Registry} + \text{Constraint Graph} + \text{Witness Engine} + \text{Residual Rank Estimator} + \text{Next-Constraint Scheduler} + \text{Verifier}. }

其目標不是產生更多文字，而是更系統地回答：

為什麼這個變量仍然是變量？

以及：

哪個新約束最值得被證明？

1. 問題：Proof Search 常把活動量誤認為進展

假設一個 theorem search系統在一小時內產生：

100

個 lemmas。

這不代表主要 theorem variable的 residual domain已經顯著下降。

可能出現：

\mathcal V_x^{(0)} = \mathcal V_x^{(100)}.

也就是所有 lemmas都正確，但對核心未知沒有 closure gain。

因此：

\boxed{ \text{proof activity} \neq \text{proof progress}. } \tag{1.1}

我們需要直接追蹤：

\boxed{ \text{what remains free}. }

2. Theorem Variable

定義 2.1

Theorem Variable不只指 algebraic variable。

任何尚未被 closure、且會影響 theorem truth或 exact comparison的結構都可視為 theorem variable。

例如：

unknown scalar；
determinant line；
period normalization；
quotient map；
local system；
finite index；
branch；
rank；
sign；
cohomology class；
regulator；
morphism；
comparison theorem；
admissible category membership。

因此 theorem variable是：

\boxed{ \text{a handle to unresolved proof-relevant residual structure}. } \tag{2.1}

3. Variable Registry

一個 proof runtime應維護：

\boxed{ \mathcal R_V = \{ \mathfrak X_1,\ldots,\mathfrak X_n \}. } \tag{3.1}

其中：

\mathfrak X_i = ( x_i, \mathcal K_i, \sim_i, \mathcal V_i, \rho_i, W_i, S_i ).

這些欄位分別是：

symbol / object handle；
current constraints；
declared equivalence；
residual domain；
residual freedom measure；
witness；
scope。

4. Variable Ontology Audit

對每個重要 theorem variable，系統至少回答：

它的 admissible domain是什麼？
現在有哪些 constraints？
哪些差異只是 gauge？
quotient後還剩什麼？
residual freedom有幾個 independent directions？
是否存在 Variablehood Witness？
是否存在 Closure Witness？
哪些 constraints還只是猜測？
哪些 constraints是 theorem？
哪些 constraints只對某個 partner / branch有效？
下一個最便宜的 separating constraint是什麼？
如果 scope改變，哪些 closure會 reopening？

這整組檢查稱為：

\boxed{ \text{Variable Ontology Audit}. } \tag{4.1}

5. Residual Variable Graph

不同 theorem variables之間通常有依賴。

定義 graph：

\boxed{ G_V = (V,E). } \tag{5.1}

若：

x_i \to x_j

表示 $x_j$ 的 closure依賴 $x_i$ 。

node可標記：

closure level；
residual rank；
witness state；
theorem status；
verification cost。

edge可標記：

dependency type；
monotonicity；
exactness level；
partner scope。

6. Variable Graph 與 Proof DAG 的差異

傳統 proof DAG追蹤：

\text{lemma} \to \text{lemma}.

Residual Variable Graph追蹤：

\boxed{ \text{unresolved structure} \to \text{unresolved structure}. }

一個 lemma可能影響多個 variables。

一個 variable也可能需要多個 lemmas。

因此兩種 graph應分開。

7. Constraint Graph

令：

\mathcal K = \{ K_1,\ldots,K_m \}.

每個 $K_i$ 可以對多個 variables施加限制。

建立 bipartite graph：

\boxed{ G_{VK} = ( V\cup K, E_{VK} ). } \tag{7.1}

edge表示：

K_j

影響：

x_i.

這能回答：

哪些 constraints在控制哪個 residual domain？

8. Constraint Gain

對 candidate constraint：

K,

若加入前 residual measure：

\rho_{\mathrm{before}},

加入後：

\rho_{\mathrm{after}},

定義：

\boxed{ G(K) = \rho_{\mathrm{before}} - \rho_{\mathrm{after}}. } \tag{8.1}

這是 proof-search中的 closure gain。

9. Constraint Cost

令：

C(K)

表示：

theorem proving成本；
numerical verification成本；
symbolic manipulation成本；
external computation成本；
formalization成本；
memory / context成本。

則：

\boxed{ \operatorname{Priority}(K) = \frac{ G(K) }{ C(K) }. } \tag{9.1}

這只是最簡單的 scheduler。

實務上還可加入：

uncertainty；
theorem centrality；
branch impact；
verification confidence。

10. Centrality-Weighted Gain

若某 variable $x_i$ 位於 proof DAG中心，可給權重：

w_i.

candidate constraint的 weighted gain：

\boxed{ G_w(K) = \sum_i w_i \Delta\rho_i(K). } \tag{10.1}

如此可優先攻擊會同時關閉多個 downstream obligations的 constraint。

11. Constraint Dominance

若兩個 constraints：

K_A, \qquad K_B

滿足：

\mathcal V(K_A) \subseteq \mathcal V(K_B),

且：

C(K_A)\le C(K_B),

則 $K_A$ dominates $K_B$ 。

scheduler可降低 $K_B$ priority。

這能避免重複探索較弱 constraints。

12. Redundant Lemma Detection

若一個新 lemma：

L

加入後：

\mathcal V_i

對所有主要 variables都不變，則：

\boxed{ G(L)=0. }

它可以是正確 lemma。

但不是 closure-progress lemma。

這可幫助 AI避免在局部正確敘述上無限展開。

13. Witness Search

對未 closure variable $x$ ，系統應嘗試找到：

W_x = (s_1,s_2).

如果找到：

s_1,s_2\models\mathcal K,

但：

s_1\not\sim s_2,

則：

\boxed{ x \text{ definitely remains open}. } \tag{13.1}

這比單純說「還不知道」更強。

14. Counterexample Engine

對一個宣稱 closure的 theorem state：

|\mathcal V_x|=1,

counterexample engine的任務就是：

\boxed{ \text{find a Variablehood Witness}. }

所以 counterexample search與 variable ontology天然統一。

15. Closure Witness Search

如果找不到 variablehood witness，不能自動宣稱 closure。

還需要 Closure Witness：

\boxed{ \forall s_1,s_2\in\mathcal A_x(\mathcal K), \quad s_1\sim s_2. } \tag{15.1}

對 finite domain可 exhaustive。

對 infinite domain需要 structural theorem。

16. Closure Levels in Proof Search

可使用 Paper 01 的 V0--V6：

V0

Unconstrained.

V1

Bounded domain.

V2

Gauge quotient完成。

V3

Finite candidate set.

V4

One-dimensional torsor.

V5

Finite root / sign ambiguity.

V6

Exact closure.

proof dashboard不應只顯示：

\text{open}

或：

\text{closed}.

而應顯示 closure level。

17. Proof-State Sequence

由 Paper 02，proof search可保存：

\boxed{ S_P = (s_0,s_1,s_2,\ldots). } \tag{17.1}

每個 node：

s_n = ( K_n, W_n, \Delta\mathcal V_n, P_n ).

其中：

$K_n$ ：新增 constraint；
$W_n$ ：witness / proof；
$\Delta\mathcal V_n$ ：消除的 residual freedom；
$P_n$ ：provenance。

所以 proof history變成 residual-domain reduction trace。

18. Proof Compression

如果 100 個 lemmas最後只產生：

3

個真正 independent constraints，

proof runtime可壓成 constraint basis：

\boxed{ K_1,K_2,K_3. }

這是 proof-history compression。

不是刪除 theorem內容。

而是找到真正 closure-critical subset。

19. Constraint Basis

若：

\mathcal V( K_1,\ldots,K_r ) = \mathcal V( \mathcal K_{\mathrm{full}} ),

則：

K_1,\ldots,K_r

是 constraint basis。

final proof certificate可以引用 basis，再保留其 derivation provenance。

20. Theorem Obligation Compression

大型 proof project常有數百條 open items。

其中很多其實只是同一 residual freedom的不同表述。

Variable Ontology Audit可把它們壓縮成：

\boxed{ \text{independent theorem obligations}. }

這比 task count更接近真正 proof distance。

21. Opaque Scalar Problem

一個典型問題是：

\eta

被標記為 unknown scalar。

但沒有說明：

它來自哪；
哪些 factors；
哪些 gauge；
哪些 partner-dependent；
哪些 finite；
哪些 exact。

此時：

\eta

是一個 opaque theorem variable。

proof search最應做的不是立刻算 $\eta$ 。

而是：

\boxed{ \text{decompose its variable ontology}. }

22. Variable Expansion

若：

\eta = \eta_1 \eta_2 \eta_3,

且三者受 independent constraints，則應：

\boxed{ \eta \rightsquigarrow ( \eta_1,\eta_2,\eta_3 ). } \tag{22.1}

但只有在它們真的是 independent residual directions時才展開。

23. Variable Compression

若 theorem只觀測：

\eta_1\eta_2^{-1},

則：

(\eta_1,\eta_2)

有一個 diagonal gauge。

真正 observable variable是：

\boxed{ u = \eta_1\eta_2^{-1}. } \tag{23.1}

proof search應 quotient掉 gauge。

24. Character-Lattice Audit

對 multiplicative unknowns：

n_1,\ldots,n_s,

可建立 character lattice：

M = \mathbf Z^s.

每個 observable有 weight：

\mathbf w_i.

形成 matrix：

W.

使用：

rank；
Smith normal form；
saturation；
target lattice；

分析真正 residual normalization directions。

這是 proof-search中特別便宜而有力的 audit。

25. Smith Normal Form as Proof Diagnostic

若：

W

的 rank小於 unknown count，存在 continuous invisible directions。

若 invariant factor：

d_i>1,

存在 finite root ambiguity。

因此 SNF能直接回答：

\boxed{ \text{還缺的是新方向，還是只缺 root / sign？} }

這比盲目增加 calibrator更有效。

26. Scope of Unknown

同一符號在不同 theorem target下，variablehood可能不同。

例如某 sign：

\epsilon\in\{\pm1\}

對線性 equality重要。

但對 quadratic regulator：

\epsilon^2=1,

它可能完全不可觀測。

因此：

\boxed{ \text{variablehood is target-dependent}. } \tag{26.1}

proof runtime必須記錄 target scope。

27. Observable-Relative Variablehood

令 theorem observable：

F.

若：

F(s_1)=F(s_2)

對所有 residual states成立，

即使：

s_1\neq s_2,

這個 freedom對 target theorem不可觀測。

因此可 quotient：

\ker F.

得到：

\boxed{ \text{observable-relative residual domain}. }

這可進一步壓縮 proof obligations。

28. P/L/E Data Levels

proof audit可將未知分成：

P-level

Projective / nonvanishing / direction.

L-level

Lattice / valuation / index.

E-level

Exact element / unit / scalar.

如果 theorem只需要 P-level，去計算 E-level可能是浪費。

如果 theorem需要 E-level，只證 L-level則 under-specified。

因此每個 obligation應標記 required data level。

29. Category Mismatch Detection

一個常見 proof waste是：

\boxed{ \text{trying to solve stronger data than the theorem can observe}. }

例如：

saturation index只需 valuation，卻追 local unit；
nonannihilation只需 nonzero map，卻追 exact scalar；
projective jet只需 direction，卻固定 basis。

Variable Ontology Audit可把這些標記為 category mismatch。

30. Under-Specification Detection

另一方向是：

exact coefficient equality卻只證 nonzero；
regulator equality卻未固定 height normalization；
scalar BSD formula卻只證 line equality。

這叫 under-specification。

runtime應警告：

\boxed{ \text{required data level > proved data level}. }

31. Theorem Boundary

當所有 internal variables都被壓到 boundary comparison maps後，proof search應停止在內部尋找新 scalar。

剩餘 obligations應被視為：

\boxed{ \text{boundary theorem}. }

例如：

arithmetic-to-analytic comparison；
p-adic-to-complex comparison；
period trivialization。

32. Proof Phase Transition

一個大型 proof常經歷：

\text{structural decomposition}

\to \text{normalization compression}

\to \text{few substantive bridges}.

如果 runtime能偵測 residual variable count從：

30

降到：

5,

但剩下每個 centrality極高，應切換 search策略。

不應繼續產生低-impact lemmas。

33. High-Weight Blocker

定義 blocker weight：

\boxed{ W_i = w_i \rho_i C_i. } \tag{33.1}

其中：

$w_i$ ：centrality；
$\rho_i$ ：residual freedom；
$C_i$ ：closure cost estimate。

這可粗略表示 blocker的重要性。

低數量 blockers也可能仍然很難。

34. Number of Papers Is Not Proof Distance

大量研究輸出：

N_{\mathrm{paper}}

不能直接映射：

\text{proof completion}.

因為早期 paper可能在消除低成本 structural ambiguity。

後期一個 theorem bridge可能權重遠高於前面數十個 lemmas。

所以：

\boxed{ \text{proof distance} \neq \text{document count}. } \tag{34.1}

35. Search Strategy after Compression

當 residual variables很少時，應從 broad exploration切換成：

\boxed{ \text{targeted bridge attack}. }

也就是對每個 blocker：

定義 exact input；
定義 exact output；
定義 missing map；
列所有 known constraints；
搜尋 variablehood witness；
搜尋最小 separating theorem。

36. Missing-Map Variable

一個 theorem bridge本身也可以是 variable。

例如：

\Phi: L_A \to L_B.

若只知道 projective class：

[\Phi],

則 residual variable可能是一個 scalar torsor。

若甚至不知道存在性，residual domain更大。

所以 morphism也需要 variable ontology。

37. Map Variable State

可表示：

\boxed{ \mathfrak M = ( \operatorname{Dom}, \operatorname{Cod}, \operatorname{AdmissibleMaps}, \operatorname{Equivalence}, \operatorname{Constraints} ). } \tag{37.1}

這使 proof search能問：

還有哪些 maps符合目前 theorem？

38. Nonzero-Map Witness

若只需證：

\Phi\neq0,

最便宜 witness可能是一個：

v

使：

\Phi(v)\neq0.

所以 search不應追 exact matrix。

這是 P-level map closure。

39. Exact-Map Closure

若需要 exact $\Phi$ ，則需證：

\operatorname{AdmissibleMaps}/\sim

只有一個 equivalence class。

這可能需要 naturality、functoriality或anchor。

40. Naturality as Constraint

naturality equation：

B(f)\Phi_X = \Phi_YA(f)

本身就是非常強的 constraint。

在 connected category中，它可能把 objectwise unknown scalars壓成一個 global scalar。

所以 proof search應高度重視 naturality constraints。

41. Functoriality as Constraint Compression

若每條 edge scalar都獨立未知，variable count很高。

證明 functoriality後，許多 edge variables變成 path products。

再證 flatness後，只剩一個 anchor。

這是大型 variable compression的典型例子。

42. Holonomy Witness

若懷疑 transport不 flat，可搜尋 loop：

\gamma

使：

h(\gamma)\neq1.

這就是 residual variablehood witness。

所以 graph holonomy test是 witness search的一種。

43. Finite Cycle Basis

對 finite graph：

\beta_1 = |E|-|V|+1.

只需測 cycle basis。

因此 variablehood witness search也可以被 graph theory finite化。

44. Residual Torsor

當所有 relative transport closure，只剩：

K^\times\text{-torsor},

proof search應停止搜尋更多 edge relations。

下一步只需：

\boxed{ \text{one absolute anchor}. }

這是 closure-level-aware search。

45. Finite Root State

若只剩：

\mu_n,

下一步不是再找 arbitrary scalar theorem。

而是：

sign theorem；
branch theorem；
second calibrator；
orientation convention。

這類低維 ambiguity應有專門 tactic。

46. Proof Tactic by Closure Level

可以建立 tactic policy：

V0

Domain discovery.

V1

Bound finding.

V2

Gauge quotient.

V3

Candidate elimination.

V4

Anchor search.

V5

Root / sign disambiguation.

V6

Freeze variable.

這比 universal tactic更有針對性。

47. Frozen Variable

一旦 variable達 V6，可標記：

\boxed{ \text{FROZEN}. }

只有 scope change、new theorem target或 contradiction witness才 reopening。

這避免 AI反覆重算已 closure問題。

48. Reopening Rule

若新 constraint scope：

S'

不被原 closure certificate涵蓋，則：

\boxed{ \text{reopen}. }

例如：

target從 P-level升到 E-level；
新 partner加入；
period convention變更；
observable增加新 character。

49. Closure Certificate

每個 frozen variable保存：

\boxed{ \operatorname{Cert}(x) = ( \mathcal K_{\min}, \sim, W_{\mathrm{close}}, S ). } \tag{49.1}

這就是最小 proof-state memory。

50. Proof Memory Compression

大型 AI proof conversation可能有幾十萬 token。

但 variable ontology可壓成：

variable registry；
constraint basis；
closure certificates；
open blocker list；
proof DAG。

這比保存所有 prose reasoning更有效。

51. Crystalized Proof State

可定義：

\boxed{ \mathfrak P = ( G_V, G_{VK}, \mathcal C_{\mathrm{closed}}, \mathcal O_{\mathrm{open}}, \mathcal D_{\mathrm{proof}} ). } \tag{51.1}

這是一個 crystallized proof state。

AI可以從這裡繼續，而不必重新讀所有歷史。

52. Search Budget Allocation

假設有 blockers：

x_1,\ldots,x_n.

可按：

\operatorname{Priority}(x_i) = \frac{ \text{expected downstream closure} }{ \text{estimated cost} }

分配 compute / agent budget。

這比平均分配更合理。

53. Multi-Agent Proof Search

不同 agents可負責：

variable decomposition；
theorem search；
counterexample；
formal verification；
numerical certificate。

共享：

\boxed{ \text{same residual variable graph}. }

所以 agents不會只交換 prose。

而是交換 closure state。

54. Generator Agent

負責提出：

K_{\mathrm{new}}.

Verifier Agent

驗證：

K_{\mathrm{new}}.

Auditor Agent

更新：

\mathcal V_x.

Counterexample Agent

搜尋：

W_x.

Scheduler Agent

決定下一個 blocker。

這是一個自然的 multi-agent architecture。

55. Proof Search as Constraint-Generated Sequence

整個 proof process可寫成：

\boxed{ \mathfrak P_0 \to \mathfrak P_1 \to \mathfrak P_2 \to \cdots } \tag{55.1}

每一步：

\mathfrak P_n \to \mathfrak P_{n+1}

加入 certified constraints並降低 residual freedom。

因此 proof本身就是 Paper 02 的 constraint-generated sequence。

56. Information Block in Proof Search

proof node不一定是 lemma全文。

可以是：

\boxed{ ( \text{variable id}, \text{constraint}, \text{witness}, \text{gain}, \text{scope} ). }

這是 theorem reasoning的 semantic block。

57. Constraint-Aware Proof Storage

Paper 04 的 residual encoding概念也可用在 proof memory。

如果某 conclusion可由 closure certificate推導，就不必重複存所有中間 derivation。

只保存：

minimal constraint basis；
witness；
theorem references。

這是 proof-state compression。

58. BSD Case Study Scope

以下 BSD case study只展示 variable ontology方法。

它不宣稱：

\boxed{ \text{BSD is proved}. }

案例重點是：

\boxed{ \text{如何把一個 opaque normalization problem 壓成少數 explicit theorem obligations}. }

59. BSD Initial Opaque State

假設一開始有 schematic relation：

\widehat B_i = C_\pi A_i j z_i.

表面上只有一個：

C_\pi.

但這個 symbol可能隱含：

auxiliary leading scale；
quotient transport；
period choice；
projected comparison；
partner independence；
exact unit；
coordinate normalization。

所以：

C_\pi

是一個 over-compressed theorem variable。

60. First Expansion

進一步解析：

\boxed{ C_\pi = c_{\mathrm{lead}} q_{\mathbf f}^{-1}. } \tag{60.1}

此時 variable ontology從一個 opaque scalar展開成兩個 potential directions：

(c_{\mathrm{lead}},q_{\mathbf f}).

但不能立刻說 rank是 $2$ 。

還要看 observables。

61. Observable Compression

late projected target與 calibrator都只看：

c_{\mathrm{lead}} q_{\mathbf f}^{-1}.

weight：

(1,-1).

因此 late theorem只觀測 rank-one character。

所以：

\boxed{ \text{late normalization residual} = \mathbf Z(1,-1). }

第二個 diagonal direction對 late theorem是 gauge / invisible。

62. Pre-Leading Reopening

當 theorem target升級為 pre-leading object時，需要：

c_{\mathrm{lead}}

weight：

(1,0).

此時原本不可觀測的方向重新變得 relevant。

所以 normalization scope變更。

這是一個典型：

\boxed{ \text{variable reopening}. }

63. Character-Lattice Witness

late character：

(1,-1),

pre-leading character：

(1,0).

形成 matrix：

\begin{pmatrix} 1&-1\\ 1&0 \end{pmatrix}.

determinant：

1.

因此它們構成完整 primitive rank- $2$ lattice。

這是一個 exact structural witness：

\boxed{ \text{one late calibrator cannot determine pre-leading normalization}. }

64. Missing Direction as Kernel

late quotient：

\chi_\pi(c,q) = cq^{-1}.

kernel：

\boxed{ K = \{ (u,u) \}. }

因此 pre-leading missing variable不是「又一個神秘 scalar」。

而是：

\boxed{ \text{the one-dimensional kernel coordinate of }\chi_\pi. }

這是 variable ontology的成功例子。

65. Second Anchor Criterion

candidate second weight：

(a,b)

在 kernel上作用：

u^{a+b}.

所以：

a+b=0

表示 redundant。

|a+b|=1

表示 primitive kernel probe。

因此「第二 calibrator有沒有用」變成一個 integer test。

66. Construction Independence

即使 candidate weight是：

(1,0),

若它的 construction先使用 unknown：

q_{\mathbf f},

則它是 circular。

所以 variable ontology還要追：

\boxed{ \text{provenance}. }

這說明 weight analysis不是全部。

67. Source-Line Search

為了得到真正 $(1,0)$ source，引入：

\mathscr C_{\mathrm{aux}},

並尋找：

\Theta_{\mathrm{aux}} \in \operatorname{Sym}^m(T^\ast) \otimes \mathscr C_{\mathrm{aux}}.

這把「找第二 scalar」改寫成：

\boxed{ \text{找一條 q-blind native source line}. }

68. Comparison Defect

auxiliary line與 arithmetic line未必相同。

定義：

\boxed{ \mathscr D = \mathscr C_{\mathrm{arith}} \otimes \mathscr C_{\mathrm{aux}}^{-1}. }

此時剩餘 variable不再是 $q_{\mathbf f}$ 本身。

而是：

\boxed{ \text{comparison defect line}. }

這是又一次 variable transformation。

69. Defect Decomposition

將 defect分類成：

E, \quad L, \quad G, \quad P.

分別代表：

exact；
lattice；
gauge；
partner-dependent。

這把一個 opaque scalar拆成不同 data levels。

70. Period--de Rham Compression

period與 de Rham frame若來自同一 pairing：

\mathscr P \otimes \mathscr D_{\mathrm{dR}} \to K,

兩個 apparent exact variables壓成一個 intrinsic product：

\eta_{\mathrm{pdR}}.

若 pairing canonical：

\eta_{\mathrm{pdR}}=1.

又消掉一個 residual direction。

71. Determinant Compression

determinant defect再拆成：

lattice index；
$K_1$ automorphism scalar；
orientation。

只有：

\kappa_{\det}

是真正 internal E-level variable。

若兩 comparison routes在 cohomology上相同：

\kappa_{\det}=1.

再 closure一層。

72. Residual Neutral Torsor

所有 character、lattice、partner、pairing、determinant defects被處理後，最後只剩：

\mathscr R.

若 monodromy trivial：

\mathscr R

的 flat sections形成：

K^\times\text{-torsor}.

此時 residual freedom rank已降到：

\boxed{ 1\text{ anchor}. }

73. Normalization Closure Certificate

最後定義 C1--C10 certificate。

通過後：

\boxed{ \text{NORMALIZATION-CLOSED}. }

這不是 BSD closure。

只是 normalization variable從高維 opaque domain被壓到 closure。

這是 variable ontology方法的一個完整案例。

74. BSD Case Study 的真正重點

這個案例展示：

\boxed{ \text{one symbol} \to \text{two characters} \to \text{kernel} \to \text{source line} \to \text{defect line} \to \text{flat torsor} \to \text{anchor}. }

也就是：

\boxed{ \text{variable form changes as constraints accumulate}. }

這正是本文方法想捕捉的東西。

75. Post-Normalization Blockers

Normalization closure後，remaining blockers是：

actual BF / Kato classes；
arithmetic fundamental-line identification；
regulator bridge；
explicit reciprocity；
p-adic leading-line theorem；
complex leading-line theorem；
finite arithmetic certificates。

這些 variables不能再被稱為 normalization unknowns。

proof ontology已經變了。

76. Phase Transition Detection

當 variable class從：

\text{normalization scalar}

轉成：

\text{arithmetic morphism}

時，scheduler應切換 tactic。

例如不應再找 period scalar。

應開始搜尋：

\boxed{ \text{BF determinant} \to \text{Mordell--Weil determinant} }

的 map。

這是 proof-search phase transition。

77. Regulator Bridge as Variable Audit

對 regulator bridge，可建立：

\mathfrak R_{\mathrm{reg}}.

admissible domain包含所有符合目前 constraints的 maps：

\Phi: D_{\mathrm{BF}} \to D_{\mathrm{MW}}.

quotient掉 gauge。

再問：

map是否存在？
是否非零？
是否 rational？
lattice index是多少？
height pairing是否 compatible？

這就是下一階段的 variable ontology。

78. Reciprocity Bridge as Variable Audit

對 reciprocity map：

\lambda: Q\to A.

若：

\dim Q = \dim A = 1,

則 projectively只有：

zero；
nonzero。

一旦證：

\lambda\neq0,

P-level closure完成。

若 exact scalar還需要，再升到 E-level。

這說明 data-level-aware audit能顯著縮小 theorem burden。

79. Complex Comparison as Variable Audit

對：

\Xi_{\mathbf C}

應分：

existence；
projective line comparison；
period frame；
exact scalar；
coordinate tensor。

這能避免把所有問題壓成「complex comparison unknown」。

80. AI Proof Search Runtime

本文建議最小 runtime包含六個核心模組。

Module 1: Variable Registry

維護所有 theorem variables與 closure level。

Module 2: Constraint Graph

維護 constraints與dependencies。

Module 3: Witness Engine

找 variablehood / closure witness。

Module 4: Residual Analyzer

估計：

\rho.

Module 5: Scheduler

選 next separating constraint。

Module 6: Verifier

驗證 theorem / certificate。

81. Variable Registry Schema

每個 variable可保存：

\boxed{ ( id, \text{type}, \text{scope}, \text{domain}, \text{equivalence}, \text{constraints}, closure\_level, residual\_rank, \text{witness}, \text{status} ). }

這比單純 TODO list豐富。

82. Constraint Record Schema

每個 constraint：

\boxed{ ( id, \text{statement}, \text{targets}, \text{source}, \text{proof}, \text{scope}, \text{cost}, \text{gain}, \text{dependencies} ). }

這可以直接支援 scheduler。

83. Witness Record

Variablehood witness：

\boxed{ ( state_1, state_2, \text{verification}, inequivalence\_proof ). }

Closure witness：

\boxed{ ( constraint\_basis, uniqueness\_proof ). }

84. Search Loop

AI proof loop可寫成：

\boxed{ \text{Audit} \to \text{Select Variable} \to \text{Propose Constraint} \to \text{Verify} \to \text{Update Domain} \to \text{Recompute Priority}. }

而不是：

\boxed{ \text{Generate more lemmas indefinitely}. }

85. Select Variable

可優先選：

x^\ast = \arg\max_x \operatorname{Priority}(x).

priority考慮：

residual freedom；
downstream centrality；
expected cost；
probability of closure。

86. Propose Constraint

對 $x^\ast$ ，generator提出：

K^\ast.

candidate來源可包括：

theorem database；
symbolic derivation；
numerical experiment；
analogy；
categorical naturality；
duality；
local-global principle；
formal solver。

87. Verify Constraint

constraint不能直接進 authoritative state。

必須：

\boxed{ \operatorname{Verify}(K^\ast)=\text{true}. }

否則只能保留為 conjectural edge。

88. Update Residual Domain

加入後：

\mathcal K' = \mathcal K \cup \{K^\ast\}.

更新：

\mathcal V_x' = \mathcal A_x(\mathcal K')/{\sim}.

再估：

\Delta\rho.

89. Promote or Freeze

若 closure level提高，更新 variable state。

若：

|\mathcal V_x|=1,

freeze。

若只剩 finite ambiguity，切換 tactic。

若 constraint無 gain，降低同類 search priority。

90. Search for Independent Constraint Directions

scheduler不應一直找同方向 stronger lemmas。

例如已有：

(1,-1)

character，下一步應找不共線 direction。

可以用 linear algebra / rank test判斷。

這是一個非常便宜的 meta-search criterion。

91. Branch Search

若 proof有多個 competing models：

M_1,\ldots,M_k,

proof search可把它們當 finite residual domain。

下一 constraint目標是最大化 branch elimination。

這類 problem特別適合 information gain scheduling。

92. Minimal Separating Set

如果要在 candidate states間唯一辨識正確 state，可尋找最小 constraint集合：

\boxed{ \mathcal K_{\mathrm{sep}}. }

這類似 feature selection / decision tree。

proof search可利用這個觀點。

93. Theorem Search as Experimental Design

如果某 constraint可透過 computation測試，其作用類似 experiment。

應選擇最能分離 residual hypotheses的 experiment。

因此 theorem search與 scientific experimental design在 residual-domain觀點下統一。

94. Numerical Experiment 的地位

numerical evidence可以縮小：

\mathcal V_x

但除非有 rigorous certificate，不能直接進 exact theorem constraints。

所以 runtime要標：

\boxed{ \text{heuristic constraint} }

與：

\boxed{ \text{proved constraint}. }

95. Soft Constraints

可允許概率型 soft constraint：

P(K\mid \text{data}).

但它只能影響 search priority。

不能直接 closure exact variable。

這對 AI exploratory mathematics有用。

96. Hard Constraints

只有 verified theorem / certificate可進 exact admissible domain。

所以 hard / soft separation非常重要。

97. Search Memory

AI不必記住所有 prose。

只要記：

open variables；
closure level；
hard constraints；
soft hypotheses；
witnesses；
next priorities。

這就是高密度 proof memory。

98. Why Symbols Become Dangerous

符號本身很方便。

但當：

x

裡壓進：

period；
quotient；
index；
torsor；
partner factor；

AI很容易對 $x$ 做錯 category的操作。

Variable Ontology Audit要求先拆清楚。

這能降低 hallucinated algebraic cancellation。

99. Wrong Cancellation Detection

若兩個 terms：

x_i, x_j

看起來名字相似，

但 scope / partner / data level不同，

不能直接 cancel。

runtime可透過 variable metadata阻止這種錯誤。

100. Wrong Universality Detection

某 factor在一個 partner是 constant，不代表 across partners universal。

Variable Registry可標：

\operatorname{Scope}=i.

只有 theorem證明 transport後才升級：

\operatorname{Scope}=\text{family}.

101. Circularity Detection

若 constraint：

K

的 proof dependency graph回到它要 closure的 variable，

系統標記 potential circularity。

這對 second-anchor / normalization問題尤其重要。

102. Proof Obligation Type

每個 open blocker可以分類：

existence；
uniqueness；
nonvanishing；
exact normalization；
finite index；
naturality；
functoriality；
comparison；
support；
rationality；
computation certificate。

不同類型使用不同 search tactic。

103. Existence versus Normalization

例如：

\Phi

可能尚未證存在。

這時去找它的 exact scalar沒有意義。

先 closure：

\boxed{ \text{existence}. }

Variable Ontology Audit可防止 theorem order錯置。

104. Nonvanishing before Exact Value

若 theorem只需要：

\lambda\neq0,

先找 witness。

不要先追：

\lambda=?

這是 proof-cost optimization。

105. Exactness Escalation

當 downstream theorem真的需要 scalar coefficient，再把 variable從 P-level升級到 E-level。

這種 escalation應顯式。

106. Proof Search Stop Rule

一個 branch若：

residual gain長期接近零；
cost持續升高；
centrality低；

可以暫停。

這避免 agent無限鑽局部 lemma。

107. Proof Search Escalation Rule

若同一 blocker高 centrality但 local search無 gain，應換 representation：

variable expansion；
quotient；
dual formulation；
category change；
computational experiment；
new source theorem。

這是 structural escalation。

108. Representation Switch

有時 blocker難，是因為 symbol representation錯。

例如：

q

看似一個 scalar。

展開成：

(c,q)

的 character lattice後問題變清楚。

所以 representation change本身是 proof tactic。

109. Constraint Sequence for a Blocker

對一個 blocker可保存：

\boxed{ S_x = ( K_1, K_2, K_3,\ldots ). }

每個 constraint有 gain。

這使研究者看到：

這個問題到底被壓縮到哪裡了？

比「寫了 80 篇」更有意義。

110. Research Progress Metric

可以定義 project residual score：

\boxed{ R_{\mathrm{project}} = \sum_i w_i \rho_i. } \tag{110.1}

當：

R_{\mathrm{project}} \to0,

proof接近 closure。

這只是 heuristic，但比 document count更結構化。

111. Blocker Count

也可記：

\boxed{ N_{\mathrm{indep}} = \text{number of independent high-weight blockers}. }

對大型猜想，這個量比 lemma count更值得觀察。

112. Blocker Compression Event

當多個 open issues被證明其實是同一 residual direction，可記為：

\boxed{ \text{compression event}. }

例如：

5 \text{ unknown scalars} \to 1 \text{ observable character}.

這是重大進展。

113. Variable Split Event

反之若一個 opaque symbol被發現包含：

3

個 independent directions，這不是退步。

是：

\boxed{ \text{latent structure discovery}. }

proof state變得更真實。

114. Proof Transparency

好的 proof-search system應能顯示：

哪些 variables已 closure；
為何 closure；
哪些還 open；
為何 open；
下一步最值得做什麼。

這比生成長篇 reasoning更有可操作性。

115. Human-AI Collaboration

人類可以擅長：

新 representation；
high-level abstraction；
unusual constraints；
theorem intuition。

AI可以擅長：

exhaustive variable audit；
dependency maintenance；
witness search；
formal derivation；
constraint scheduling。

Variable Ontology提供共享語言。

116. Local Agent Role

Local agents可實際跑：

symbolic rank；
SNF；
interval certificates；
counterexamples；
graph holonomy；
cohomology maps；
finite factors。

Web / reasoning agent則維護：

ontology；
theorem architecture；
category boundaries；
proof DAG。

這是一個自然分工。

117. Proof Runtime Interface

最小 API可包含：

\boxed{ \operatorname{register\_variable} }

\boxed{ \operatorname{add\_constraint} }

\boxed{ \operatorname{quotient\_gauge} }

\boxed{ \operatorname{estimate\_residual} }

\boxed{ \operatorname{find\_witness} }

\boxed{ \operatorname{freeze} }

\boxed{ \operatorname{reopen} }

\boxed{ \operatorname{next\_constraint} }

118. Variable Query

研究者可以直接問：

為什麼 $x$ 還是 variable？

runtime回傳：

current domain；
witness；
missing constraints；
closure level。

這正是本系列起點的問題。

119. Next-Constraint Query

研究者問：

下一步做什麼？

runtime不只列 TODO。

而是按：

\frac{ \text{expected residual gain} }{ \text{cost} }

排序 constraints。

120. Proof Explanation

對已 closure variable，runtime可回答：

它曾有哪幾個 freedom？哪些 constraint逐一消掉？最後 witness是什麼？

這是 proof explainability。

121. Reproducibility

另一個 agent只要拿到：

variable registry；
constraint basis；
witnesses；
scope；

即可重建 closure state。

不必拿到原始完整 conversation。

這對長期 AI research很重要。

122. Formal Proof Integration

proof assistant可以驗：

K_i.

Variable Ontology層負責：

為何需要 $K_i$ ；
它 closure 哪個 direction；
是否足夠；
還缺什麼。

所以 ontology層與 formal proof層互補。

123. SMT Integration

SMT可協助：

witness search；
finite model elimination；
residual domain checking。

但 ontology層仍需判斷：

gauge；
scope；
theorem target；
data level。

124. Numerical Integration

數值程式可提供：

candidate witness；
counterexample；
interval bound；
finite certificate。

只要結果被 verifier升級成 hard constraint。

125. Database Integration

proof knowledge base不只存 papers。

也可存：

\boxed{ \text{constraint objects}. }

每個 constraint標：

applies to variable types；
prerequisites；
closure gain history；
formal proof reference。

這有利於 theorem reuse。

126. Constraint Reuse

若某 constraint pattern已在多個 problems中成功 closure相似 variable，可被 scheduler提高 prior。

這形成 meta-learning。

127. Variable Pattern Library

可建立 pattern：

hidden gauge scalar；
rank-one torsor；
finite root ambiguity；
determinant lattice mismatch；
period duality；
transport holonomy；
partner-dependent factor。

AI遇到類似 pattern可直接套 audit template。

128. Anti-Pattern Library

同時保存常見錯誤：

exact scalar chasing when P-level enough；
using same symbol across partners；
absorbing partner factor into common line；
treating finite index as exact unit；
circular anchor construction；
scalarizing before pairing；
assuming equal character means equal line。

這能顯著降低重複錯誤。

129. Theorem Search Strategy Library

不同 residual shape可有不同 tactic。

例如：

Torsor

找 anchor / naturality。

Finite roots

找 sign / branch。

Character lattice

找 independent weight。

Holonomy

找 cycle basis。

Lattice index

找 local length。

Comparison line

找 natural transformation。

這形成 structural tactic library。

130. Variable Ontology as Meta-Mathematics

本方法不直接給出每個 theorem答案。

它提供的是：

\boxed{ \text{how to represent what remains unknown}. }

這是一種 meta-mathematical architecture。

它的價值在於讓：

proof search；
numerical computation；
AI memory；
theorem planning；

共享同一 residual-freedom語言。

131. Proof Search Convergence

如果每一步 hard constraint都 strict 降低某個 well-founded residual measure：

\rho_0 > \rho_1 > \rho_2 > \cdots,

且 $\rho$ 不可無限下降，則 search可保證 finite closure。

但一般 theorem domain未必有這種離散 measure。

因此 convergence theorem需依 domain而定。

132. Non-Monotone Research

實際研究有時會 reopening variables。

例如發現 hidden assumption。

所以 research sequence可能：

\rho_{n+1} > \rho_n.

這不一定是失敗。

它可能是更正 ontology。

因此應區分：

proof monotonicity；
research-state correction。

133. Research Honesty

好的 system應允許：

\boxed{ \text{we discovered more residual freedom}. }

而不是強迫 progress score永遠下降。

這比假裝 closure更重要。

134. Confidence 與 Proof Status

每個 constraint可有 status：

conjectural；
numerically supported；
independently verified；
formally proved。

只有最後兩類可進 exact closure，視 policy而定。

135. Independent Verification

若兩個 agents獨立得到同一 constraint，可提高信心。

但 mathematically仍需 proof / certificate。

所以 agreement不等於 theorem。

136. High-Dimensional Unknown 的問題

AI很容易在高維 opaque variable上產生 plausible但無法閉合的 narrative。

Variable decomposition可以降低這種風險。

因為每個 residual direction都要有：

domain；
constraint；
witness。

137. Semantic Overload Detection

若一個 symbol被發現同時參與多個 independent transformation laws，可能代表 semantic overload。

system應提示：

\boxed{ \text{consider variable expansion}. }

138. Over-Parameterization Detection

若多個 variables總是以固定 combination出現，可能 over-parameterized。

system提示：

\boxed{ \text{consider quotient / compression}. }

139. Variable Ontology Fixed Point

理想 proof state中，每個主要 symbol都滿足：

residual domain明確；
gauge明確；
data level明確；
next closure condition明確。

這可視為 ontology fixed point。

之後才適合集中火力證 final theorem。

140. Minimal AI Architecture

一個最小可行實作不需要自動證明深 theorem。

只要能：

讀取 symbolic project；
註冊 variables；
接收 constraints；
計算簡單 residual rank；
維護 dependency graph；
顯示 closure level；
提醒 redundant / circular constraints；
產生 audit report。

就已經有價值。

141. Advanced AI Architecture

進階版再加入：

automatic variable decomposition；
automatic character lattice；
witness synthesis；
theorem retrieval；
constraint gain estimation；
multi-agent scheduling；
formal proof integration；
proof-state crystallization。

142. Variable Ontology Report

對一個 project可生成：

\boxed{ \text{Variable Ontology Report}. }

包含：

open variables；
residual rank；
closure level；
witness；
centrality；
next constraints；
estimated costs；
proof phase。

這比普通 research summary更適合長期攻堅。

143. BSD Example Report

例如 normalization phase可報：

\boxed{ \text{late normalization character} : \text{V6 under assumptions} }

\boxed{ \text{pre-leading quotient kernel} : \text{V4 before second anchor} }

\boxed{ \text{period--de Rham defect} : \text{E-level comparison obligation} }

\boxed{ \text{determinant defect} : K_1\text{-type residual} }

\boxed{ \text{residual neutral line} : K^\times\text{-torsor}. }

這比「還有一些 normalization問題」資訊密度高很多。

144. Proof Phase Report

Normalization closure後：

\boxed{ \text{phase} = \text{Regulator Bridge}. }

system應停止推薦 normalization tactics。

改推薦：

determinant comparison；
lattice saturation；
height pairing；
Mordell--Weil map。

這就是 phase-aware proof search。

145. Why This Matters for AI

大型語言模型善於生成局部合理推理。

但深數學常失敗在：

hidden variable scope；
repeated normalization；
circularity；
symbol overloading；
category mismatch；
stale assumptions。

Variable Ontology是一個外部結構化約束層，可補強這些弱點。

146. Why This Matters for Human Mathematicians

人類研究者也常把：

\text{unknown}

當成單一類型。

但其實：

unknown sign；
unknown torsor；
unknown map；
unknown index；
unknown line；
unknown partner factor；

需要完全不同方法。

將它們分型可以改善研究策略。

147. Generality beyond BSD

本方法可應用於：

algebraic geometry；
number theory；
PDE；
optimization；
formal verification；
program synthesis；
symbolic physics；
exact numerics；
constraint programming；
AI planning。

只要問題可以描述成：

\boxed{ \text{admissible states + constraints + equivalences}. }

就可以做 variable ontology。

148. Proof Search and Numerical Search Unification

Paper 03--04處理 exact real與 residual bits。

Paper 05處理 theorem variables。

兩者其實共享：

\boxed{ \text{residual admissible domain}. }

numerical refinement消除：

\text{value states}.

proof refinement消除：

\text{model / theorem states}.

所以 computation與 proof search可被視為同一種 constraint refinement。

149. Unified Constraint Runtime

最終可以想像一個 runtime同時處理：

numbers；
symbols；
lines；
maps；
proofs；
packets；

每個 object都提供：

\boxed{ \operatorname{residual}() }

\boxed{ \operatorname{refine}() }

\boxed{ \operatorname{verify}() }

\boxed{ \operatorname{witness}() }

\boxed{ \operatorname{encode}() }

這是本系列五篇共同指向的更大方向。

150. Main Theorem Package

本文提出以下核心結論。

Theorem A

Proof progress應以主要 theorem variables的 residual freedom reduction衡量，而不是 lemma count。

Theorem B

Variablehood Witness提供「仍未 closure」的可證明證據。

Theorem C

Closure Level決定不同 proof tactics。

Theorem D

Character lattice、Smith normal form、holonomy與torsor可作為 residual-domain分析工具。

Theorem E

Constraint-generated proof sequence可以壓縮長期 theorem state。

Theorem F

當 normalization certificate closure後，search strategy應 phase-transition到 substantive arithmetic bridges。

Theorem G

Opaque symbolic unknown可透過 Variable Ontology Audit轉成有限且類型明確的 theorem obligations。

151. 最重要的八個原則

Principle 1

\boxed{ \text{proof progress} \neq \text{lemma count}. }

Principle 2

\boxed{ \text{proof progress} = \text{residual freedom reduction}. }

Principle 3

\boxed{ \text{every important unknown should expose why it remains unknown}. }

Principle 4

\boxed{ \text{gauge should be quotiented before counting variables}. }

Principle 5

\boxed{ \text{search the next separating constraint, not merely the next plausible lemma}. }

Principle 6

\boxed{ \text{data level must match theorem demand}. }

Principle 7

\boxed{ \text{closure should be frozen and only reopened by explicit triggers}. }

Principle 8

\boxed{ \text{proof state should preserve witnesses and provenance}. }

152. 系列總結

五篇形成一條完整鏈：

Paper 01

\boxed{ \text{Why is a symbol still a variable?} }

Paper 02

\boxed{ \text{How does residual closure become a generated sequence?} }

Paper 03

\boxed{ \text{How can exact reals exist without decimal ontology?} }

Paper 04

\boxed{ \text{How much physical information is actually still free?} }

Paper 05

\boxed{ \text{How can theorem search systematically reduce residual freedom?} }

整個系列的主線是：

\boxed{ \text{Symbol} \to \text{Constraint Domain} \to \text{Residual Freedom} \to \text{Generated Sequence} \to \text{Residual Encoding} \to \text{Proof / Computation Closure}. }

153. 結論

一個數學問題中的變量，不應只被記成：

x=?

而應被描述成：

\boxed{ \mathfrak X = ( x, \mathcal K, \sim, \mathcal V, W, \rho, S ). }

真正的 proof progress不是產生更多文字。

而是讓：

\mathcal V

逐步縮小。

當：

|\mathcal V|=1,

variable closure。

當只剩：

K^\times\text{-torsor},

下一步是 anchor。

當只剩：

\mu_n,

下一步是 root / sign resolution。

當只剩一個 map existence theorem，下一步就應停止追 scalar。

因此 proof search可以被重新描述為：

\boxed{ \text{a controlled process of residual-variable elimination}. }

這也是本系列最核心的統一觀點。

數值計算、symbolic representation、bit encoding與 theorem proving，不再是完全分離的領域。

它們都可以被放入同一個架構：

\boxed{ \text{admissible states} + \text{constraints} + \text{equivalence} + \text{refinement} + \text{witness} + \text{closure}. }

這為未來 constraint-generated numerical runtime、AI proof search與跨域 exact computation提供了一個共同理論基礎。

Series Status

Paper 01: Variablehood by Residual Constraint Domain — completed
Paper 02: Constraint-Generated Sequence Representation — completed
Paper 03: Decimal-Free and Generator-First Real Numbers — completed
Paper 04: Constraint-Aware Information Encoding and Residual Bits — completed
Paper 05: Variable Ontology Audit for Mathematical Proof Search — completed

The first five-paper foundational series is complete.