title: 從自然語言到可驗證形式化：SREG–SRBC 語義分支與閉合方法論
english_title: From Natural Language to Verifiable Formalization: The SREG–SRBC Methodology for Semantic Branching and Closure
series: SRBC：符號表徵邊界與語義完備性理論
series_english: SRBC: Symbolic Representation Bounds and Semantic Completion
series_number: SRBC-07/07
author: Neo.K with Aletheia (GPT-5.6 Sol)
institution: EveMissLab / 一言諾科技有限公司
version: v0.1
date: 2026-09-23
language: zh-TW
document_type: 理論論文 / 系列收束篇 / 方法論與 Runtime 規格
status: 初版完成

從自然語言到可驗證形式化

SREG–SRBC 語義分支與閉合方法論

English Title: From Natural Language to Verifiable Formalization: The SREG–SRBC Methodology for Semantic Branching and Closure
系列：《SRBC：符號表徵邊界與語義完備性理論》SRBC-07/07
作者： Neo.K with Aletheia (GPT-5.6 Sol)
機構： EveMissLab / 一言諾科技有限公司
版本： v0.1
日期： 2026-09-23

Canonical Source Note

本文件以 UTF-8 Markdown 保存正式原稿。數學 source 僅使用 $...$ 與 $$...$$ 作為 canonical delimiter。本文把自然語言、形式化候選、completion branch、query、lift、metric、certificate 與 closure artifact 視為不同型別的研究物件，不允許在 source artifact 中以渲染畫面、隱含假設或未標來源的轉譯取代 canonical state。若未來進入 proof assistant、typed IR、NCM、EveGlyph、SREG runtime、概率程式、模型檢查器或自動科學系統，應保存 source version、frame、query version、admissibility rule、branch graph、provenance、verification state、GAP profile、budget、reopen condition 與所有 closure certificate。

摘要

SRBC 系列前六篇建立了一條從符號表徵到可驗證語義手術的完整理論鏈。SRBC-01 建立符號的動態表徵邊界；SRBC-02 將單一自然語言表述提升為合法語義完成族；SRBC-03 引入查詢 $Q$ ，把「多個解讀」與「多個答案」分離；SRBC-04 建立語義非法升格與隱含結構注入審計；SRBC-05 把 GAP 從布林判定提升為歧義寬度、完備距離、閉合代價與穩健性等多維測度；SRBC-06 則以 Monty Hall 為第一個完整案例，示範同一表述如何在不同 protocol 與 query 下產生不同的完備性狀態。

本文作為系列收束篇，將上述理論接回 SREG 的長程形式生成與脈衝閉包框架，正式提出第一代 SREG–SRBC Formal Semantic Surgery Methodology。其基本流程為：

\boxed{ \text{Source Freeze} \rightarrow \text{Representation Audit} \rightarrow \text{Completion Branching} \rightarrow \text{Query Canonicalization} \rightarrow \text{Query Quotient} \rightarrow \text{Lift Audit} \rightarrow \text{Countermodel Search} \rightarrow \text{GAP Measurement} \rightarrow \text{Minimal Closure} \rightarrow \text{Verification} \rightarrow \text{Certificate} \rightarrow \text{Reopen}. }

本文特別拒絕把「閉合」定義成強迫所有語義 branch 收斂到單一答案。對一個 query 而言，成熟的研究閉合至少有三種合法終點：

\operatorname{QRC}

表示已證明查詢相對完備；

\operatorname{QRU}

表示已證明存在合法且 query-distinguishable 的 completion；

\operatorname{QDU}

表示已證明某些合法 completion 中該 query 尚未被充分定義。

因此，真正的閉合對象不是「唯一答案」，而是 查詢的可證狀態。本文將其稱為：

\boxed{ \operatorname{QRSRC} = \text{Query-Relative Semantic Resolution Closure}. }

一個 QRSRC artifact 可以證明唯一答案，也可以證明欠決定，或證明目前問題本身尚不具足可計算結構。只要 frame、query、admissibility、provenance、verification、known frontier 與 reopen condition 被完整保存，研究即可在有限邊界內形成誠實閉合。

本文進一步建立 SREG–SRBC 統一狀態 tuple、branch graph、semantic ledger、query-sensitive debt、lift ledger、GAP profile、closure gate、reopen protocol、adversarial reopening test、版本規則與第一代 YAML artifact schema。SREG 的：

\text{Explore} \rightarrow \text{Branch} \rightarrow \text{Formalize} \rightarrow \text{Verify} \rightarrow \text{Merge} \rightarrow \text{Compress} \rightarrow \text{Reopen}

由此獲得 SRBC 所提供的語義合法性、query-relative equivalence、GAP measurement 與 provenance discipline；SRBC 則獲得 SREG 的長程生成、脈衝閉合、frontier、debt、budget 與 reopen 機制。

本文最後提出下一階段正式研究綱領：不再繼續以論文先行擴張理論，而應建立可執行 benchmark 與 runtime，對 Monty Hall、Bertrand 類問題、Sleeping Beauty、因果歧義、法律規則、軟體需求與 AI prompt formalization 進行多模型、跨模型與形式驗證實驗。SRBC 系列至此由「理論建立期」轉入「正式研究期」。

關鍵詞： SRBC、SREG、Formal Semantic Surgery、語義分支、查詢相對完備、語義閉合、completion space、provenance、GAP、countermodel、closure certificate、reopen、AI reasoning

0. 系列收束：SRBC 到底完成了什麼？

SRBC 並沒有證明：

\boxed{ \text{自然語言普遍不完備}. }

也沒有證明：

\boxed{ \text{所有數學形式化都會扭曲自然語言}. }

這兩個命題都太強。

SRBC 真正完成的是一個較弱但可研究的框架：

\boxed{ \text{給定表述、上下文與查詢，我們能否明確描述其合法完成空間、答案分岔、隱含注入與閉合條件？} }

因此整個系列的研究對象始終是：

(u,C,Q).

而不是抽象地談：

\text{Language}

本身。

1. 七篇論文的功能分解

SRBC-01：Symbolic Representation Bounds

建立：

\mathbb B_{A,C,Q}^{\Lambda}(s) = \left[ \underline{\mathcal B}, \overline{\mathcal B} \right].

核心問題：

一個符號在指定表示系統、主體、上下文與任務中，能穩定承載到哪裡？

SRBC-02：Semantic Completion Space

建立：

u \mapsto \mathfrak I(u,C).

核心問題：

一段表述究竟允許哪些合法形式完成？

SRBC-03：Query-Relative Completeness

建立：

M_i\sim_Q M_j \iff Q(M_i)=Q(M_j),

以及：

\mathfrak G_Q = \mathfrak I/{\sim_Q}.

核心問題：

多個 completion 是否真的造成當前問題的答案分岔？

SRBC-04：Semantic Illegal Lifts

建立：

\mathcal J = \Gamma_{\mathrm{analysis}} \setminus \operatorname{Cn} \left( \Gamma_{\mathrm{source}} \right),

以及 hidden structure injection、bridge certificate 與 query-harmful lift。

核心問題：

形式化過程究竟偷偷加入了哪些原表述沒有支付的語義負擔？

SRBC-05：Semantic GAP Measurement

建立：

\mathbf G_Q = \left( N_Q, \Delta_Q, R_Q^*, H_Q, D_{\mathrm{comp}}, \kappa_Q, D_{\mathrm{inj},Q}, m_Q, \kappa_{\mathrm{sem}} \right).

核心問題：

GAP 有多大、離閉合多遠、修補要多少成本、答案有多脆弱？

SRBC-06：Monty Hall Semantic Surgery

建立第一個完整案例：

P(C=d_2\mid E) = \frac{ p_2\ell_2 }{ p_1\ell_1+p_2\ell_2 }.

並證明：

\text{粗 query 可完備}

同時：

\text{細 query 可欠決定}.

核心問題：

如何把一個經典爭議從語感辯論轉成 source、model、query 與 certificate 的可審計系統？

SRBC-07：Methodology and Runtime

本文的任務是：

\boxed{ \text{把前六篇變成可以真正跑的研究方法。} }

2. SREG 提供了什麼？

SREG-F03 已建立：

\boxed{ \text{Explore} \rightarrow \text{Branch} \rightarrow \text{Formalize} \rightarrow \text{Verify} \rightarrow \text{Merge} \rightarrow \text{Compress} \rightarrow \text{Reopen}. }

它同時提出：

latent semantic field；
candidate formalization family；
delayed commitment；
ambiguity debt；
branch merge；
semantic observability；
replayability。

這些正是 SRBC 所需要的運行載體。

3. SRBC 補給 SREG 的內容

SREG-F03 已知道：

不應太早把 ambiguity 消掉。

但它還需要回答：

哪個 branch 是合法 completion？
branch 之間哪個差異會改變 query？
哪個 commitment 是 text-given？
哪個是 analyst injection？
branch 可以在什麼條件下 merge？
何時可以宣告 semantic closure？
closure 是唯一答案，還是已證明欠決定？
GAP 可以如何量化？

SRBC 就是這組補件。

4. 統一架構

整體關係可寫成：

\boxed{ \mathrm{SREG} + \mathrm{SRBC} = \text{Generative Formalization} + \text{Semantic Accountability}. }

SREG 負責：

\text{generate / explore / reopen}.

SRBC 負責：

\text{bound / audit / quotient / measure / certify}.

5. 第一代統一狀態 tuple

定義時刻 $t$ 的語義研究狀態：

\mathfrak S_t = ( u_t, C_t, \Lambda_t, \Gamma_t, \Theta_t, \mathfrak I_t, Q_t, \mathfrak G_{Q,t}, \mathcal J_t, \mathbf G_{Q,t}, \mathcal V_t, B_t, \mathcal F_t, \mathcal R_t ).

其中：

u_t

為 source expression；

C_t

為 context；

\Lambda_t

為 representation system；

\Gamma_t

為已確認 commitment set；

\Theta_t

為 open semantic slots；

\mathfrak I_t

為 admissible completion space；

Q_t

為 canonical query；

\mathfrak G_{Q,t}

為 query quotient；

\mathcal J_t

為 semantic injection / lift ledger；

\mathbf G_{Q,t}

為 GAP profile；

\mathcal V_t

為 verification state；

B_t

為 resource budget；

\mathcal F_t

為 known frontier；

\mathcal R_t

為 reopen conditions。

6. 為什麼 source 必須是一等物件？

如果 source：

u

被分析者在過程中重寫，

但系統沒有版本紀錄，

那麼最後可能不知道：

\boxed{ \text{究竟是在證原句，還是在證自己的改寫。} }

因此：

u_t

不能只是一段 transient prompt。

它必須具有：

\operatorname{SourceID}.

7. Source Freeze

Formal Semantic Surgery 的第一步是：

\boxed{ \operatorname{Freeze}(u,C). }

保存：

原始 UTF-8 source；
語言；
標點；
source version；
source origin；
context boundary；
已知外部規則。

Freeze 不表示內容永遠不能修改。

而是：

\boxed{ \text{任何修改都產生新版本，而不覆蓋原版本。} }

8. Source Version Graph

如果：

u_0 \rightarrow u_1 \rightarrow u_2,

應保存：

G_{\mathrm{source}} = (V,E).

例如：

u_0

原始 Parade-style Monty Hall；

u_1

標準 protocol 版；

u_2

對稱 tie-breaking 版。

它們不是同一 source。

9. 第一階段：Representation Audit

輸入：

(u,C,\Lambda).

執行 SRBC-01。

目標不是立即解析所有語義。

而是找：

identity-preserving interpretation range；
overloaded symbols；
hidden role index；
hidden time index；
hidden quantifier；
overloaded modal；
overloaded probability term；
需要重符號化的位置。

10. Representation Audit Output

輸出：

\mathcal B_{\mathrm{rep}} = ( \underline{\mathcal B}, \overline{\mathcal B}, D_{\mathrm{repr}}, \mathcal O_{\mathrm{resym}} ).

其中：

D_{\mathrm{repr}}

為 representation debt；

\mathcal O_{\mathrm{resym}}

為候選重符號化操作。

11. 第二階段：Semantic Frame Extraction

從：

u,C

抽取：

\Gamma_0.

要求 commitment 分型：

\Gamma_0 = \Gamma_{\mathrm{text}} \cup \Gamma_{\mathrm{context}} \cup \Gamma_{\mathrm{institution}} \cup \Gamma_{\mathrm{theorem}} \cup \Gamma_{\mathrm{declared}}.

12. 不允許 provenance-free commitment

每個：

\lambda\in\Gamma

至少有：

\operatorname{Origin}(\lambda).

若來源不明：

\operatorname{Origin}(\lambda) = \text{unresolved}.

而不是默認：

\text{text}.

13. 第三階段：Open Slot Detection

找出：

\Theta = \{ \theta_1,\ldots,\theta_n \}.

open slot 可能包含：

quantifier；
time；
role；
policy；
prior；
causal direction；
intervention semantics；
tie-breaking；
norm modality；
threshold；
utility；
observer information；
protocol stationarity。

14. Open Slot 不等於問題

存在：

\theta_i

不代表一定要解析。

只有當：

\theta_i\in\Theta_Q^{+}

才是 query-sensitive。

因此 open-slot detection 只是候選階段。

15. 第四階段：Completion Branching

根據：

\Gamma, \Theta

建立：

\mathfrak I(u,C).

這可以是：

顯式有限模型；
參數化模型族；
constraint system；
symbolic model class；
probabilistic program family；
theorem-prover model class。

16. Completion Branch 必須自帶 provenance

每個 branch：

B_i

至少保存：

B_i = ( \Gamma, \Delta_i, P_i, V_i ),

其中：

\Delta_i

為 branch-specific commitments；

P_i

為 provenance；

V_i

為 verification state。

17. Branch Legality Gate

只有：

\operatorname{Adm}(B_i\mid u,C)=1

才進：

\mathfrak I.

如果：

\operatorname{Adm}

未決，

則 branch 狀態是：

\operatorname{Pending}.

不能直接當 countermodel。

18. 第五階段：Query Canonicalization

自然語言問題：

q_{\mathrm{NL}}

必須轉成：

Q.

Query object 至少包含：

Q = ( \mathcal D_Q, \mathcal A_Q, I_Q, T_Q, V_Q, \Pi_Q, \varepsilon_Q ).

19. Query Schema

其中：

\mathcal D_Q

為 input model domain；

\mathcal A_Q

為 answer domain；

I_Q

為 conditioning information；

T_Q

為 time index；

V_Q

為 observer / perspective；

\Pi_Q

為 intervention / policy specification；

\varepsilon_Q

為 tolerance。

20. Query Versioning

Query 也必須版本化：

Q_0 \rightarrow Q_1.

例如：

Q_0 = \text{Is switching advantageous?}

可拆成：

Q_1 = P(\text{always-switch win})

與：

Q_2 = P(C=d_2\mid E).

這些不是同一 query。

21. 第六階段：Query Quotient

建立：

M_i\sim_QM_j \iff Q(M_i)=Q(M_j).

然後：

\mathfrak G_Q = \mathfrak I/{\sim_Q}.

22. Query Quotient 的工程價值

如果一百個 branch 對：

Q

都同值，

它們可以暫時合併成：

[B]_Q.

因此 runtime 不必攜帶一百份完整 branch 進入後續決策。

23. Query-Directed Compression

定義：

\pi_Q: \mathfrak I \rightarrow \mathfrak G_Q.

這是 SRBC 版本的 query-directed semantic compression。

24. 不可過度 merge

若未來 query：

Q'

可能區分原本被 $Q$ merge 的模型，

就必須保存：

\operatorname{MemberRefs}([B]_Q).

也就是：

\boxed{ \text{merge for current query} \neq \text{delete semantic history}. }

25. 第七階段：Query-Sensitive Slot Analysis

把：

\Theta

分解：

\Theta = \Theta_Q^{+} \cup \Theta_Q^{0}.

其中：

\Theta_Q^{+}

可能改變答案；

\Theta_Q^{0}

目前對 query 中性。

26. Delayed Commitment Rule

若：

\theta\in\Theta_Q^{0},

則優先：

\boxed{ \operatorname{DelayCommitment}(\theta). }

除非它對 verification、future query 或 safety 有其他必要性。

27. Clarification Rule

若：

\theta\in\Theta_Q^{+},

系統可選：

branch；
clarification；
conditional answer；
interval answer；
underdetermination certificate。

不是所有情況都必須詢問使用者。

28. 第八階段：Lift Audit

比較：

\Gamma_{\mathrm{source}}

與：

\Gamma_{\mathrm{analysis}}.

候選 injection：

\mathcal J = \{ \lambda\in\Gamma_{\mathrm{analysis}} : \Gamma_{\mathrm{source}}\not\models\lambda \}.

29. Lift Ledger

每個：

\lambda\in\mathcal J

記：

L(\lambda) = ( \operatorname{Type}, \operatorname{Scope}, \operatorname{Origin}, \operatorname{Bridge}, \operatorname{QueryEffect}, \operatorname{ReopenCondition} ).

30. Lift 不一定要刪除

若：

\lambda

是合理 completion，

只要標：

\operatorname{Assumption}(\lambda)

即可。

真正錯誤是：

\operatorname{Assumption}(\lambda) \rightarrow \operatorname{Given}(\lambda)

的 provenance falsification。

31. 第九階段：Evaluate Branches

對：

M_i\in\mathfrak I,

計算：

Q(M_i).

可能需要：

theorem proving；
symbolic algebra；
probability inference；
simulation；
causal inference；
program execution；
database query；
model checking。

32. 計算工具不能決定 source semantics

工具可以證：

Q(M_i)=a.

但工具本身不能證：

u\mapsto M_i

是唯一合法 mapping。

這是 SRBC 的 typed boundary。

33. 第十階段：Resolution Classification

定義：

\mathsf R_Q \in \{ \operatorname{QRC}, \operatorname{QRU}, \operatorname{QDU}, \operatorname{UNRESOLVED} \}.

34. QRC

如果：

\operatorname{Dom}(Q)=\mathfrak I

且：

|\mathfrak G_Q|=1,

並具有完備證書，則：

\mathsf R_Q = \operatorname{QRC}.

35. QRU

若找到：

M_i,M_j\in\mathfrak I

使：

Q(M_i)\neq Q(M_j),

且兩 branch admissibility 已驗證，則：

\mathsf R_Q = \operatorname{QRU}.

36. QDU

若存在：

M\in\mathfrak I

使：

M\notin\operatorname{Dom}(Q),

且這不是工具失敗，而是模型本身缺少 query 所需結構，則：

\mathsf R_Q = \operatorname{QDU}.

37. UNRESOLVED

如果：

尚未找到 countermodel；
但也沒有 completeness proof；
或 admissibility 尚未閉合；

則：

\mathsf R_Q = \operatorname{UNRESOLVED}.

38. 第十一階段：Countermodel Search

若目標是測：

\operatorname{QRC},

優先搜尋：

\max_{M_i,M_j\in\mathfrak I} d_Q \left( Q(M_i),Q(M_j) \right).

39. Adversarial Semantic Search

這不是惡意攻擊。

而是：

\boxed{ \text{主動尋找最能破壞過早唯一化的合法模型。} }

40. Countermodel Priority

優先選：

commitment 差異小；
query 差異大；
provenance 清楚；
易驗證；
易重放。

即高：

L_Q(M_i,M_j).

41. 第十二階段：GAP Measurement

若：

\mathsf R_Q = \operatorname{QRU},

或仍未解，

建立：

\mathbf G_Q.

至少可包含：

N_Q, \quad \Delta_Q, \quad \kappa_Q.

42. GAP Measurement 不要求全量

如果只能證：

\Delta_Q \ge L,

也應保存。

如果只能證：

\Delta_Q \le U,

也應保存。

最成熟形式是：

L \le \Delta_Q \le U.

43. 第十三階段：Minimal Closure Search

搜尋：

\Delta\Gamma^* = \arg\min_{\Delta\Gamma} c(\Delta\Gamma)

subject to：

\operatorname{QRC}_{\Gamma+\Delta\Gamma}.

44. Minimal Closure 不是強迫 source 改寫

它只回答：

如果我們想讓這個 query 變唯一，最少還要固定什麼？

原 source 可以保持原樣。

45. Closure Candidate Types

候選 closure 可能是：

補一條自然語言規則；
指定 prior；
指定 time scope；
指定 observer；
指定 policy；
指定 causal graph；
指定 intervention；
指定 metric；
指定 tolerance。

46. 第十四階段：Verification

所有主要 artifact 進入：

\mathcal V.

Verification 可分：

\mathcal V = ( V_{\mathrm{source}}, V_{\mathrm{logic}}, V_{\mathrm{model}}, V_{\mathrm{numeric}}, V_{\mathrm{simulation}}, V_{\mathrm{provenance}}, V_{\mathrm{replay}} ).

47. Source Verification

檢查：

source 是否正確；
版本是否固定；
quote 是否準確；
context 是否混版。

48. Logical Verification

檢查：

\Gamma\models\lambda?

以及：

M_i\models\Gamma?

49. Model Verification

檢查 completion：

M_i

是否真的滿足 admissibility。

50. Numerical Verification

檢查：

Q(M_i)

的算術、概率、最佳化與數值誤差。

51. Simulation Verification

Simulation 只驗：

\operatorname{Behavior}(M_i).

不能被升格成：

\operatorname{UniqueSemantics}(u).

52. Provenance Verification

檢查：

\operatorname{Origin}(\lambda)

是否被正確標記。

這是 SRBC 特有的重要 verification layer。

53. Replay Verification

另一個系統是否能用 artifact 重建：

\mathsf R_Q

與：

\mathbf G_Q

的主要結果？

54. 第十五階段：Closure

這裡需要一個重要修正。

傳統「閉合」容易讓人聯想到：

\boxed{ \text{找到唯一答案}. }

SRBC 不接受這個定義。

55. Resolution Closure

真正閉合的是：

\boxed{ \text{對 query 狀態的可證判定}. }

因此定義：

\operatorname{QRSRC} = \text{Query-Relative Semantic Resolution Closure}.

56. QRSRC 的三種成功狀態

56.1 Unique Closure

證明：

\operatorname{QRC}.

56.2 Underdetermination Closure

證明：

\operatorname{QRU}.

這也是成功。

因為研究問題：

原表述是否唯一決定答案？

已被回答為：

否。

56.3 Undefinability Closure

證明：

\operatorname{QDU}.

這也是成功。

因為已證：

目前 source / frame 尚不足以使 query 在所有合法 completion 中定義。

57. 不能把 QRU 視為「研究失敗」

這是整個方法論很重要的一點。

如果：

\operatorname{QRU}

被嚴格證明，

那研究反而完成了一個強結果：

\boxed{ \text{唯一化不可由目前 source 合法完成。} }

58. Conditional Closure

有時可以輸出：

Q(M) = \begin{cases} a_1,&\lambda_1,\\ a_2,&\lambda_2. \end{cases}

並證明 branch cover 完整。

這形成：

\operatorname{ConditionalClosure}.

59. Epsilon Closure

若任務容差：

\varepsilon_Q>0

且已證：

\Delta_Q\le\varepsilon_Q,

可形成：

\operatorname{QRSRC}_{\varepsilon}.

但必須標：

\varepsilon_Q.

60. QRSRC 不等於 Terminal Completeness

QRSRC 必須帶：

\Phi

frame，

B

budget，

Q

query。

所以：

\operatorname{QRSRC}_{\Phi,B}(u,C;Q)

只表示：

在目前已聲明 frame、representation、knowledge、verification 與 budget 中，query 狀態已取得可審計閉合。

61. 與 SREG PEC 對接

SREG 的 pulse：

\Pi_k = ( \mathfrak M_k, \Gamma_k, K_k, \mathcal L_k, \mathcal O_k, \mathcal V_k, B_k ).

SRBC 可嵌入 semantic substate：

\Sigma_k^{\mathrm{SRBC}} = ( u_k, C_k, Q_k, \mathfrak I_k, \mathfrak G_{Q,k}, \mathcal J_k, \mathbf G_{Q,k} ).

62. Semantic Pulse

定義：

\Pi_k^{\mathrm{sem}} = ( u_k, C_k, \Lambda_k, \Gamma_k, Q_k, \mathcal V_k, B_k ).

執行：

\mathfrak C_k^{\mathrm{sem}} = \operatorname{QRSRC} \left( \Pi_k^{\mathrm{sem}} \right).

63. Closure Artifact

每次閉合產生：

\mathfrak C_k^{\mathrm{sem}} = ( \mathsf R_Q, \operatorname{Cert}_Q, \mathbf G_Q, D_Q, \mathcal F_Q, \mathcal R_Q ).

其中：

D_Q

為 unresolved debt；

\mathcal F_Q

為 frontier；

\mathcal R_Q

為 reopen condition。

64. Closure Gate

第一代 QRSRC closure gate 至少要求：

source 已 freeze；
context boundary 已聲明；
query 已 canonicalize；
admissibility rule 已聲明；
query-sensitive branches 已處理；
hidden query-harmful injection 已清零或明確保留；
resolution status 有證書；
known frontier 已保存；
resource budget 已保存；
reopen condition 已保存。

65. Debt Gate

定義：

D_Q = ( D_{\mathrm{amb},Q}^{+}, D_{\mathrm{inj},Q}, D_{\mathrm{verify},Q}, D_{\mathrm{frontier},Q} ).

Exact QRSRC 可以要求：

D_{\mathrm{amb},Q}^{+}=0,

D_{\mathrm{inj},Q}=0,

並使 verification debt 低於聲明門檻。

66. QRU 的 ambiguity debt 如何可能是零？

如果我們已經證明：

\operatorname{QRU},

並且完整描述：

\mathfrak G_Q,

那「多個答案」本身不是 debt。

Debt 是：

還不知道有哪些合法 branch。

因此：

\boxed{ \text{ambiguity} \neq \text{ambiguity debt}. }

67. 這是一個關鍵哲學修正

成熟系統不是：

\boxed{ \text{消滅所有歧義}. }

而是：

\boxed{ \text{知道歧義在哪、是否合法、是否影響 query、是否已被完整表達。} }

68. Reopen Condition

closure artifact 必須包含：

\mathcal R_Q = \{ r_1,\ldots,r_n \}.

例如：

source version 改變；
新 context evidence；
新 admissible branch；
query 改變；
新 metric；
verification 失敗；
countermodel 出現；
budget 大幅增加；
representation system 擴張。

69. 自動重開

若：

r_i

被觸發，

則：

\mathfrak C_k^{\mathrm{sem}} \rightarrow \operatorname{REOPENED}.

並啟動：

\Pi_{k+1}^{\mathrm{sem}}.

70. Reopen 不是推翻舊結果

若舊 certificate 在舊 frame 仍有效，

它仍保留：

\operatorname{Valid}_{\Phi_k}.

新研究只是：

\Phi_k \rightarrow \Phi_{k+1}.

71. Frame-Relative Validity

因此所有結論最好寫：

\operatorname{Valid} ( \phi \mid \Phi, Q, V ).

而不是漂浮：

\phi=\text{absolute}.

72. Adversarial Reopening Test

借用 SREG PEC 的 ART 思想。

closure 後主動測：

改 query；
改 observer；
改 time scope；
移除 critical assumption；
加入 alternative completion；
改 prior；
改 policy；
改 representation。

看：

\mathsf R_Q

是否仍穩定。

73. Semantic ART

定義：

\operatorname{SART} ( \mathfrak C^{\mathrm{sem}} )

為 Semantic Adversarial Reopening Test。

它不是用來證 terminal completeness。

而是估 closure robustness。

74. SART Output

可輸出：

m_Q

robustness margin，

J_Q

reopen jump，

以及：

\mathcal C_Q^*

minimal semantic cut set。

75. Closure Confidence 與 Closure Truth 分開

可以有：

\operatorname{Confidence}=0.99

但沒有 formal certificate。

也可以有 formal proof，卻只在狹窄 frame 成立。

所以需要分：

\operatorname{CertStatus}

與：

\operatorname{Confidence}.

76. 第一代狀態機

可以建立：

SOURCE_FROZEN
    ↓
FRAME_EXTRACTED
    ↓
BRANCHED
    ↓
QUERY_CANONICALIZED
    ↓
AUDITED
    ↓
EVALUATED
    ↓
{QRC | QRU | QDU | UNRESOLVED}
    ↓
MEASURED
    ↓
CERTIFIED
    ↓
QRSRC
    ↓
REOPENED

77. UNRESOLVED 不能進 exact QRSRC

如果：

\mathsf R_Q = \operatorname{UNRESOLVED},

則最多形成：

\operatorname{CheckpointArtifact}.

不能叫 exact closure。

78. Research Checkpoint

checkpoint 可保存：

已驗證 branch；
已知 GAP 下界；
尚未解的 slot；
搜索 budget；
下一輪 reopening route。

這能避免長程研究斷裂。

79. SRBC Runtime 的最小模組

第一代可以拆：

Source Registry；
Semantic Parser；
Commitment Extractor；
Completion Generator；
Admissibility Checker；
Query Compiler；
Branch Quotient Engine；
Lift Guard；
Evaluator；
Countermodel Searcher；
GAP Analyzer；
Closure Optimizer；
Certificate Builder；
Reopen Manager。

80. Source Registry

保存：

(u,C,\operatorname{SourceID},\operatorname{Version}).

81. Semantic Parser

不是直接輸出唯一 formula。

而是：

u \rightarrow ( \Gamma, \Theta, \operatorname{CandidateBranches} ).

82. Commitment Extractor

每一 commitment：

commitment:
  id: ...
  proposition: ...
  type: ...
  origin: ...
  scope: ...
  confidence: ...

83. Completion Generator

輸出：

B_1,\ldots,B_n

或參數化族：

B(\theta).

84. Admissibility Checker

判定：

\operatorname{Adm}(B_i\mid u,C) \in \{ \text{yes}, \text{no}, \text{pending} \}.

85. Query Compiler

把：

q_{\mathrm{NL}}

編譯成：

Q.

若存在多個 query formalization：

Q_1,\ldots,Q_m,

則自身也需 branch。

86. Branch Quotient Engine

計算或近似：

\mathfrak I/{\sim_Q}.

87. Lift Guard

檢查：

\Gamma_{\mathrm{source}} \rightarrow \Gamma_{\mathrm{analysis}}.

輸出：

\mathcal J.

88. Evaluator

依 query type 路由：

logic；
probability；
simulation；
causal；
optimization；
code；
symbolic math。

89. Countermodel Searcher

目標：

\max d_Q.

或者至少尋找：

d_Q>0.

90. GAP Analyzer

生成：

\mathbf G_Q.

91. Closure Optimizer

求：

\Delta\Gamma^*.

92. Certificate Builder

產生：

QRC certificate；
QRU certificate；
QDU certificate；
conditional closure certificate；
epsilon closure certificate。

93. Reopen Manager

監控：

\mathcal R_Q.

94. 第一代總 artifact schema

srbc_artifact:
  artifact_id: ...
  source:
    id: ...
    version: ...
    text_hash: ...
    context_id: ...

  representation:
    system: ...
    audit_status: ...
    overloaded_symbols: ...

  commitments:
    given: []
    contextual: []
    declared_assumptions: []
    defaults: []
    unresolved: []

  open_slots: []

  completion_space:
    representation: ...
    admissibility_rule: ...
    branches: []

  query:
    id: ...
    version: ...
    answer_domain: ...
    tolerance: ...

  quotient:
    equivalence_rule: ...
    classes: ...

  lift_audit:
    injections: []
    query_harmful: []

  evaluation:
    branch_answers: []

  resolution:
    status: QRC
    certificate_ref: ...

  gap_profile:
    branch_count: ...
    diameter: ...
    closure_cost: ...
    injection_debt: ...
    robustness_margin: ...

  closure:
    frame_id: ...
    budget: ...
    verification: ...
    frontier: []
    reopen_conditions: []

  provenance:
    created_by: ...
    source_refs: []

95. Canonical artifact 與 rendering 分離

正式研究 artifact 應保存：

\boxed{ \text{canonical source} }

而不是只保存 UI rendering。

這和本文的數學 source 原則一致。

96. Hashing

可保存：

h(u),

h(Q),

h(\Gamma),

h(\operatorname{Cert}).

避免 source 被改後仍沿用舊 certificate。

97. Certificate Invalidating Change

如果：

h(u)\neq h(u'),

certificate 不應自動沿用。

需要：

\operatorname{MigrationProof}.

98. Branch DAG

branch 不一定是樹。

因為不同路徑可能 merge。

所以：

G_B = (V_B,E_B)

最好是 DAG 或更一般的 provenance graph。

99. Merge Edge

若：

B_i\sim_Q B_j,

可以建立：

B_i,B_j \rightarrow [B]_{Q}.

但保留原 references。

100. Split Edge

若 query 變：

Q\rightarrow Q',

原 quotient class 可能重新分裂：

[B]_Q \rightarrow B_i,B_j.

所以 compression 必須 reversible。

101. Reversible Semantic Compression

理想條件：

\operatorname{Expand} ( \operatorname{Compress}_Q(B) )

能恢復 member refs 與 branch commitments。

不是一定恢復所有計算 cache，但要恢復 provenance。

102. Semantic Ledger

研究過程至少有五本帳。

102.1 Commitment Ledger

記：

\Gamma.

102.2 Ambiguity Ledger

記：

\Theta.

102.3 Branch Ledger

記：

\mathfrak I.

102.4 Lift Ledger

記：

\mathcal J.

102.5 Closure Ledger

記：

\mathfrak C^{\mathrm{sem}}.

103. Debt Ledger

再加：

D_Q.

這讓「還沒完成什麼」變成一等資料。

104. Frontier Ledger

記錄：

\mathcal F_Q.

例如：

尚未檢查的 linguistic theory；
尚未枚舉的 policy class；
尚未 formalize 的 query；
尚未 proof-check 的 theorem；
尚未探索的 countermodel family。

105. 為什麼 frontier 不能省略？

沒有 frontier 的 closure 容易被誤讀成：

\boxed{ \text{已經沒有東西可研究}. }

而真正的 QRSRC 只表示：

\boxed{ \text{目前聲明邊界內的 query 狀態已閉合}. }

106. Budget Ledger

保存：

B = ( b_{\mathrm{time}}, b_{\mathrm{compute}}, b_{\mathrm{memory}}, b_{\mathrm{token}}, b_{\mathrm{tool}}, b_{\mathrm{verification}} ).

這沿用 SREG PEC。

107. Budget-Relative Closure

低 budget 下沒有找到 countermodel，

不能推出：

\operatorname{QRC}.

只能說：

\operatorname{NoCountermodelFound}_{B}.

108. Countermodel Found 則不同

一旦找到合法：

M_i,M_j

使：

Q(M_i)\neq Q(M_j),

就足以證：

\operatorname{QRU}.

所以：

\boxed{ \text{underdetermination often has finite witness;} }

而：

\boxed{ \text{completeness often needs global proof.} }

109. 不對稱性

這是 runtime 策略的重要來源。

在 early phase：

\boxed{ \text{先找反例，後做全域完備證明。} }

通常比較有效。

110. Counterexample-First Strategy

流程：

\text{Generate diverse admissible branches} \rightarrow \text{maximize query separation}.

若成功：

\operatorname{QRU}.

若長期失敗：

才投入更昂貴的 QRC proof。

111. 但不能把 search failure 當 QRC

這一點全系列反覆強調：

\boxed{ \text{no counterexample found} \neq \text{proved complete}. }

112. Clarification as Experiment

當系統可以詢問人類時：

\lambda

的 clarification 可視為 experiment。

選：

\lambda^* = \arg\max \frac{ \operatorname{ExpectedGapReduction}(\lambda) }{ c_{\mathrm{ask}}(\lambda) }.

113. 不是所有歧義都問

如果：

S_Q(\lambda)=0,

不必問。

這能大幅減少 AI 的「過度澄清症」。

114. Conditional Answer as Closure

如果使用者不想補資訊，

系統可以輸出：

\{ (\lambda_1,a_1), (\lambda_2,a_2) \}.

只要 branch cover 經證明完整，

這仍是成熟 closure。

115. Interval Closure

如果：

Q(M)\in[a,b]

對所有 admissible $M$ ，

可以輸出：

[a,b].

若：

b-a\le\varepsilon,

可形成 task-relative epsilon closure。

116. Set-Valued Answer

SRBC 允許答案本身是：

\mathcal A_Q.

這比強迫選一個 scalar 更誠實。

117. Proof Object

理想 certificate 應包含 machine-checkable proof object 或至少：

\operatorname{ProofTrace}.

尤其 QRC。

118. Simulation Object

若用 simulation，保存：

code hash；
seed；
model config；
run count；
estimator；
confidence interval。

但 simulation artifact 型別應標：

\operatorname{ModelEvidence},

不是：

\operatorname{TextEntailmentProof}.

119. Model Checker Interface

對有限 completion：

\mathfrak I = \{M_1,\ldots,M_n\},

可直接 model-check：

Q(M_1)=\cdots=Q(M_n)?

120. SMT / SAT Interface

若 completion constraints 可編碼，

可以搜尋：

\exists M_i,M_j: \Gamma(M_i) \land \Gamma(M_j) \land Q(M_i)\neq Q(M_j).

若 solver 找到 witness：

得到 QRU certificate。

121. QRC 的 solver 形式

若能證 unsat：

\Gamma(M_i) \land \Gamma(M_j) \land Q(M_i)\neq Q(M_j),

且 query 對所有模型已定義，

則得到 QRC。

122. 這是一個非常重要的可執行化方向

SRBC 的核心可以被轉成：

\boxed{ \text{model-separation satisfiability problem}. }

這是正式研究階段最值得先做的 runtime MVP 之一。

123. Continuous Model Family

若：

M(\theta),

則可以改成 optimization：

\max_{\theta_i,\theta_j} d_Q \left( Q(M(\theta_i)), Q(M(\theta_j)) \right)

subject to：

\theta_i,\theta_j \in \Theta_{\mathrm{adm}}.

124. Probabilistic Program Interface

host policy、causal model、Bayesian narrative 都可以表示成 probabilistic program。

SRBC runtime 可以對 program family 做：

inference；
symbolic likelihood；
simulation；
sensitivity。

125. Natural Language Interface

自然語言仍然保留。

因為：

\boxed{ \text{自然語言擅長生成與跨域壓縮；形式層擅長約束與驗證。} }

不應把其中一個消滅。

126. Dual Representation

維持：

L_N \leftrightarrow L_F.

其中：

L_N

為 natural language；

L_F

為 formal objects。

127. 轉譯本身也是 artifact

每一次：

L_N\rightarrow L_F

保存：

\operatorname{TranslationID}.

這是防止 formalization drift 的關鍵。

128. Translation Non-Uniqueness

如果：

F_1(u)\neq F_2(u),

不要直接判一個錯。

先測：

F_1,F_2\in\mathfrak I?

再測：

F_1\sim_QF_2?

129. 如果 query 等價，可 merge

即使 formalization 不同：

F_1\neq F_2,

若：

Q(F_1)=Q(F_2),

當前 query 下可合併。

130. 如果 query 不等價，必須保留 branch

這正是：

\Theta_Q^{+}.

131. Formalization Compiler 的新定義

不再定義：

\operatorname{Compiler}:L_N\rightarrow L_F.

而更成熟地寫：

\boxed{ \operatorname{Compiler} : (L_N,C,Q) \rightarrow ( \Gamma, \Theta, \mathfrak I, \operatorname{Prov} ). }

它輸出的是受約束 completion family，不是單一 formula。

132. Query-Directed Compiler

更進一步：

\operatorname{QCompiler} : (u,C,Q) \rightarrow \mathfrak I_Q,

其中只保留 query-relevant distinctions。

133. Lift-Aware Compiler

compiler 每加入：

\lambda

就必須標：

\operatorname{Origin}(\lambda).

134. Gap-Aware Compiler

compiler 不只輸出 model。

還輸出：

\widehat{\mathbf G}_Q.

135. Closure-Aware Compiler

最後可以輸出：

\operatorname{QRSRC}

或：

\operatorname{Checkpoint}.

136. AI 的理想回答模式

對一個簡單問題：

如果：

\operatorname{QRC}

且 confidence / certificate 足夠，

直接答。

如果：

\operatorname{QRU},

輸出：

在條件 A 下答案 X；在條件 B 下答案 Y。原表述沒有唯一固定兩者。

如果：

\operatorname{QDU},

輸出：

目前問題缺少讓該量被定義的必要規則。

137. 不把方法論暴露給普通使用者

Runtime 可以內部跑：

\mathfrak I, \mathcal J, \mathbf G_Q.

但對普通使用者只輸出必要層。

這避免方法論成為 UX 負擔。

138. Research Mode

研究者則可以要求：

full branch graph；
countermodels；
GAP profile；
lift ledger；
closure certificate；
reopen conditions。

139. Education Mode

教學可展示：

\text{source} \rightarrow \text{assumption} \rightarrow \text{formula} \rightarrow \text{answer}.

讓學生看到每一支箭頭。

140. Specification Mode

對軟體需求：

u_{\mathrm{req}}

轉：

\mathfrak I_{\mathrm{impl}}.

如果 acceptance query 分岔，

規格需要補充。

141. Legal / Policy Mode

對規範文本：

u_{\mathrm{rule}}

保持：

modal operator；
exception；
time；
subject；
jurisdiction；

為 typed fields。

本文不提供法律判決，只提供語義審計框架。

142. Scientific Model Mode

對理論敘述：

u_{\mathrm{theory}}

區分：

\Gamma_{\mathrm{obs}}, \Gamma_{\mathrm{model}}, \Gamma_{\mathrm{bridge}}.

避免 assumption 被倒灌成 observation。

143. Causal Mode

明確區分：

P(Y\mid X),

P(Y\mid\operatorname{do}(X)),

Y_x.

把 observational / interventional / counterfactual 當不同 query type。

144. Probability Mode

明確保存：

(\Omega,\mathcal F,P),

condition event，

protocol，

prior，

observer。

145. Dynamic-System Mode

保存：

t,

transition kernel，

stationarity，

history state。

146. SREG Pulse 中的 SRBC

每一次 SREG pulse 都可以帶：

\operatorname{SRBCSnapshot}_k.

這樣長程形式生成中不會失去：

branch；
provenance；
query；
debt；
closure status。

147. Pulse-to-Pulse Semantic Drift

定義：

D_{\mathrm{drift}} \left( \mathfrak S_k, \mathfrak S_{k+1} \right).

如果 source 未變但 commitment 大量變，

就要檢查是否有 silent drift。

148. Semantic Drift Alarm

若：

h(u_k)=h(u_{k+1})

但：

d( \Gamma_k, \Gamma_{k+1} ) > \tau,

觸發：

\operatorname{DriftAudit}.

149. Query Drift Alarm

若：

Q_k\neq Q_{k+1}

但使用者以為仍在回答同一問題，

必須標記。

150. Metric Drift Alarm

若：

d_Q

改變，

不能直接比較：

\Delta_Q^{(k)}

與：

\Delta_Q^{(k+1)}.

151. Admissibility Drift Alarm

如果：

\operatorname{Adm}_k \neq \operatorname{Adm}_{k+1},

branch count 變化可能只是規則改變。

必須保存。

152. Research Reproducibility

一個 SRBC 實驗最少應能重建：

(u,C,Q,\Gamma,\mathfrak I,\operatorname{Adm},\mathsf R_Q).

153. Strong Reproducibility

更強版本還能重建：

\mathbf G_Q, \mathcal J, \Delta\Gamma^*, \operatorname{Cert}_Q.

154. Benchmark Unit

一個 benchmark case 定義：

\mathcal B = ( u,C,Q, \mathfrak I^*, \operatorname{GoldCert} ).

155. Benchmark 不只要 gold answer

傳統 benchmark 常只有：

(u,a).

SRBC benchmark 應有：

(u,C,Q,\text{branch family},\text{status},\text{certificate}).

156. 四類 benchmark

156.1 QRC Case

多 branch，但同 answer。

156.2 QRU Case

至少兩合法 branch 不同 answer。

156.3 QDU Case

某些 branch 中 query 未定義。

156.4 Lift Trap Case

標準答案依賴 hidden injection。

157. Monty Hall 可以同時產生四類子題

不同 query / frame 下：

QRC；
QRU；
QDU；
lift trap；

都可出現。

所以它非常適合作為第一個 benchmark family。

158. 下一階段不應只繼續寫論文

七篇完成後，理論已足夠。

接下來最有資訊價值的是：

\boxed{ \text{做 runtime、做 benchmark、做反例搜索、做形式驗證。} }

159. 第一批正式研究案例

建議第一批至少包括：

Monty Hall；
Bertrand paradox；
Sleeping Beauty；
Newcomb-like protocol problem；
Simpson-like narrative ambiguity；
causal observational/interventional swap；
legal modal ambiguity；
software requirement ambiguity；
AI prompt hidden-assumption benchmark；
scientific model-selection narrative。

160. 每個案例都跑同一 pipeline

這才有可比較性：

\operatorname{Pipeline}(u_i,C_i,Q_i).

161. Cross-Case Metrics

可比較：

\Delta_Q,

\kappa_Q,

D_{\mathrm{inj},Q},

m_Q,

\kappa_{\mathrm{sem}}.

162. Cross-Model Experiment

讓不同 AI：

A_1,\ldots,A_n

對同一 case 產生：

\mathfrak I^{(A_i)}.

比較：

branch recall；
false branch rate；
hidden injection rate；
QRC false positive；
QRU detection；
minimal closure quality。

163. Human–AI Comparison

也可以比較人類與 AI：

H_j

對：

u

的 completion family。

但這是實證研究，不應用單次聊天輸出當一般心理學結論。

164. Third-Type Experimental Interface

當有真實模型、真實 runtime 與足夠資料後，可把 SRBC case 放入更高階實驗方法：

生成；
擾動；
反事實；
cross-model；
heldout；
adversarial reopen；
formal verification。

本文只建立接口，不在此展開另一套方法論。

165. 形式驗證目標一：Countermodel Soundness

對 QRU：

\operatorname{Adm}(M_1),

\operatorname{Adm}(M_2),

Q(M_1)\neq Q(M_2).

三者都要 machine-check。

166. 形式驗證目標二：QRC Completeness

若有限模型：

證：

\forall M\in\mathfrak I: Q(M)=a.

若參數化：

證：

\forall\theta\in\Theta_{\mathrm{adm}}: Q(M(\theta))=a.

167. 形式驗證目標三：Lift Soundness

對候選：

\lambda,

檢查：

\Gamma\models\lambda?

168. 形式驗證目標四：Query Definability

證：

\forall M\in\mathfrak I: M\in\operatorname{Dom}(Q).

169. 形式驗證目標五：Minimal Closure

證：

\Delta\Gamma^*

使 QRC，

並且沒有更低成本 repair。

170. Formalization Boundaries

有些自然語用判定可能無法完全 proof-assistant 化。

例如：

\operatorname{Adm}(M\mid u,C)

可能仍需語言學判斷。

這時應把：

\operatorname{Adm}

的證據型別標明：

formal；
corpus-supported；
expert-annotated；
model-consensus；
unresolved。

171. 不要偽造形式嚴格性

如果 admissibility 本身不是 theorem，

不能因後面用了 Lean / Coq 就把整條鏈說成形式證明。

所以 certificate 必須有：

\operatorname{EvidenceType}.

172. Mixed-Evidence Certificate

一個結果可以是：

evidence:
  source_parse: expert_annotated
  branch_constraints: formal
  query_evaluation: proof_assistant
  gap_bound: symbolic
  admissibility: mixed

這比統稱「已證明」更誠實。

173. Closure Strength Levels

可定義：

L0

Informal hypothesis.

L1

Explicit branch analysis.

L2

Countermodel / conditionally verified.

L3

Machine-checkable branch constraints and query evaluation.

L4

Certified admissibility + complete model coverage.

L5

Frame-relative adversarially reopened and re-certified.

這不是學術評分，只是 artifact maturity level。

174. 不使用單一「論證強度分數」

因為：

\operatorname{Strength}

本身多維。

更好保存：

source certainty；
admissibility certainty；
formal coverage；
verification level；
GAP bound quality；
reopen robustness。

175. 系列核心原理一：語義責任外顯化

\boxed{ \text{Formalization} = \text{Externalization of Semantic Commitments}. }

不是：

\text{Natural Language} \rightarrow \text{One Formula}.

176. 核心原理二：合法多分支

\boxed{ |\mathfrak I|>1 }

不代表失敗。

未標記多分支才是風險。

177. 核心原理三：Query Indexing

\boxed{ \text{Completeness is query-relative}. }

178. 核心原理四：Branch Non-Backprojection

\boxed{ \lambda\in B_i \not\Rightarrow \lambda\in\Gamma_{\mathrm{source}}. }

179. 核心原理五：No Silent Lift

\boxed{ \text{No semantic strengthening without provenance or bridge.} }

180. 核心原理六：GAP is Multidimensional

\boxed{ \text{Gap} \neq \text{one scalar by default}. }

181. 核心原理七：Closure Can Certify Non-Uniqueness

\boxed{ \operatorname{QRU} }

也可以是成功閉合。

182. 核心原理八：Closure is Frame-Bound

\boxed{ \operatorname{QRSRC}_{\Phi,B} \not\Rightarrow \operatorname{TerminalComplete}. }

183. 核心原理九：Compression Must Be Reversible

對當前 query 的 merge 不應刪除 provenance。

184. 核心原理十：Reopen is Native

任何 closure 都要保存：

\operatorname{ReopenCondition}.

185. 系列最簡公式

整個 SRBC 可以壓成：

\boxed{ u \rightarrow \Gamma \rightarrow \mathfrak I \rightarrow Q \rightarrow \mathfrak G_Q \rightarrow \mathcal J \rightarrow \mathbf G_Q \rightarrow \mathsf R_Q \rightarrow \operatorname{Cert} \rightarrow \operatorname{Reopen}. }

186. 與 SREG 的合成公式

SREG 原循環：

\text{Explore} \rightarrow \text{Branch} \rightarrow \text{Formalize} \rightarrow \text{Verify} \rightarrow \text{Merge} \rightarrow \text{Compress} \rightarrow \text{Reopen}.

SRBC 加入：

\boxed{ \text{Bound} \rightarrow \text{Admit} \rightarrow \text{Query} \rightarrow \text{Audit} \rightarrow \text{Measure} \rightarrow \text{Certify}. }

187. 統一循環

因此：

\boxed{ \text{Explore} \rightarrow \text{Bound} \rightarrow \text{Branch} \rightarrow \text{Admit} \rightarrow \text{Query} \rightarrow \text{Formalize} \rightarrow \text{Audit} \rightarrow \text{Evaluate} \rightarrow \text{Counterexample Search} \rightarrow \text{Measure} \rightarrow \text{Verify} \rightarrow \text{Merge} \rightarrow \text{Certify} \rightarrow \text{Compress} \rightarrow \text{Reopen}. }

188. 這不是固定線性 pipeline

某些案例可能跳過：

metric；
simulation；
clarification；
complete enumeration。

所以 runtime 應是 graph。

189. Pipeline DAG

定義：

G_{\mathrm{proc}} = (V_{\mathrm{proc}},E_{\mathrm{proc}}).

每個節點是一個 typed operation。

190. 操作型別

例如：

\operatorname{Parse}, \operatorname{Branch}, \operatorname{Prove}, \operatorname{Simulate}, \operatorname{Merge}, \operatorname{Measure}, \operatorname{Close}, \operatorname{Reopen}.

191. Typed Edge

每條 edge 保存：

\operatorname{InputType} \rightarrow \operatorname{OutputType}.

這能阻止：

\text{simulation evidence} \rightarrow \text{text entailment}

這種非法 type cast。

192. SRBC 其實也是一套 Type Safety

很多推理錯誤可以重寫成：

\boxed{ \text{semantic type mismatch}. }

例如：

\operatorname{Knowledge} \neq \operatorname{Policy}.

\operatorname{Event} \neq \operatorname{Protocol}.

\operatorname{ModelEvidence} \neq \operatorname{SourceEntailment}.

193. Future Typed IR

未來可建立：

TextCommitment
ContextCommitment
AssumptionCommitment
Policy
Observation
ProbabilityKernel
CausalEdge
Query
Answer
Certificate

避免天然語言全部混成 string。

194. EveGlyph / NCM 接口

如果未來 formal object native：

\operatorname{Commitment}

可以是真正 typed object。

branch、query、lift 與 certificate 可以直接連圖。

195. Semantic Graph

可建立：

G_S = ( V_S, E_S ),

節點：

symbol；
commitment；
branch；
model；
query；
answer；
certificate。

邊：

entails；
assumes；
completes；
contradicts；
answers；
invalidates；
reopens。

196. Provenance Graph

另建：

G_P.

追：

\text{source} \rightarrow \text{commitment} \rightarrow \text{branch} \rightarrow \text{result}.

197. 一個結果可追到每個假設

理想情況：

a \rightarrow \{ \lambda_1,\ldots,\lambda_n \}

可反查。

這是 semantic accountability。

198. Semantic Diff

兩個答案：

a_1,a_2

對應 branch：

M_1,M_2.

系統應能輸出：

\operatorname{Diff}(M_1,M_2).

只顯示 query-relevant commitment difference。

199. Minimal Semantic Diff

求：

\operatorname{Diff}_Q^{\min}.

這就是最小解釋：

為什麼兩個答案不同？

200. Human-Readable Explanation

由 formal diff 投影成：

模型 A 假設主持人必定開羊門；模型 B 只假設主持人知道門後內容但隨機開未選門。因此觀察到三號羊門在兩模型中的 likelihood 不同，後驗分別為 $2/3$ 與 $1/2$ 。

這是 SRBC runtime 應輸出的解釋型態。

201. 語義手術的「手術報告」

每個案例最終可有：

source；
query；
critical slots；
admissible models；
semantic diff；
answer diff；
GAP；
repair；
certificate；
reopen conditions。

202. 這比一般解答多了什麼？

一般解答回答：

Q(M)=a.

Semantic Surgery 回答：

\boxed{ \text{為什麼是這個 }M， \text{還有哪些 }M， \text{它們是否改變 }Q， \text{要補什麼才能閉合。} }

203. 何時不需要 SRBC？

如果 source 本身已是嚴格 formal specification：

\Gamma

且 query：

Q

明確，

completion space 已由語義制度唯一決定，

那 SRBC runtime 可以快速退化成普通 theorem proving / model checking。

204. Fast Path

若：

|\mathfrak I|=1

且：

D_{\mathrm{inj},Q}=0,

直接：

M \rightarrow Q(M).

所以 SRBC 不必讓所有簡單問題變慢。

205. Slow Path

若：

|\mathfrak G_Q|>1

或：

\operatorname{QDU},

才啟動更完整 branch / clarification / GAP 分析。

206. Adaptive SRBC

因此可以做：

\boxed{ \text{fast if stable, deep if branch-sensitive}. }

207. Runtime 的失敗模式

207.1 Branch Explosion

completion 太多。

207.2 False Admissibility

生成不合法 branch。

207.3 Missing Branch

漏掉合法 countermodel。

207.4 Query Miscompile

自然語言問句轉錯 Q。

207.5 Lift False Positive

把合法 implication 誤判為 injection。

207.6 Metric Abuse

選錯 answer metric。

207.7 Closure Hallucination

未證明卻輸出 QRC。

207.8 Reopen Failure

新 evidence 出現後仍沿用舊 certificate。

208. Branch Explosion 的解法

使用：

\mathfrak G_Q

做 quotient。

再用：

N_{\mathrm{cov}}(\varepsilon)

做代表 branch。

209. Missing Branch 的解法

使用：

adversarial prompting；
solver；
program synthesis；
multiple models；
human experts；
perturbation；
counterfactual search。

210. Query Miscompile 的解法

保留：

q_{\mathrm{NL}} \leftrightarrow Q

雙表示。

並允許多 query candidates。

211. Lift False Positive 的解法

所有 SIL 判定都要求：

\Gamma\not\models\lambda

或至少標：

\operatorname{EntailmentStatus}=\text{unresolved}.

不能只靠語感判 illegal。

212. Closure Hallucination 的解法

exact QRC 需要：

\operatorname{CertType} \in \{ \text{proof}, \text{exhaustive-model-check}, \text{symbolic-elimination}, \text{complete-quotient} \}.

213. 若沒有完備證書

只能輸出：

\operatorname{NoCounterexampleFound}_{B}.

214. 研究資料格式

建議：

Markdown：論文與人類可讀 artifact；
YAML / JSON：結構資料；
SMT-LIB：solver；
Lean / Coq：proof；
Python / Julia / probabilistic language：simulation；
graph DB：provenance。

215. Canonical Source Rule

正式研究不可：

把渲染公式複製回 source；
把 LaTeX 轉 Unicode 後當 canonical；
做 unicode_escape round-trip；
混用 delimiter；
丟掉 branch provenance。

216. Validation Gate

每個正式 artifact：

\operatorname{Validate} \rightarrow \operatorname{Commit}.

檢查：

UTF-8；
delimiter；
syntax；
source hash；
schema；
references；
certificate links。

217. Research Directory

第一代可以：

cases/
  monty_hall/
    source/
    queries/
    models/
    countermodels/
    certificates/
    gap/
    simulations/
    formal/
    reports/

218. Case Manifest

case:
  id: MONTY-HALL-001
  source_id: MH-PARADE-STYLE-v1
  queries:
    - Q-EX-ALWAYS-SWITCH
    - Q-OBS-DOOR3-POSTERIOR
  status:
    - ...

219. Benchmark Manifest

benchmark:
  version: 0.1
  cases:
    - MONTY-HALL-001
    - BERTRAND-001
    - SLEEPING-BEAUTY-001

220. Research Questions for Phase II

RQ1

不同 AI 是否生成相同：

\Theta_Q^{+}?

RQ2

哪類模型最容易 hidden lift？

RQ3

query-directed branching 是否減少不必要澄清？

RQ4

countermodel-first 是否降低 QRC false positive？

RQ5

GAP profile 是否能預測人類爭議程度？

RQ6

formal certificate 是否能穩定重建 across models？

221. 不要先假設答案

例如 RQ5：

\text{GAP profile} \rightarrow \text{human controversy}

目前只是 hypothesis。

必須用資料測。

222. 第一階段 MVP

最小可行 runtime 不必支援所有自然語言。

只需：

case schema；
manually curated commitments；
parameterized completion；
query evaluator；
countermodel search；
gap calculation；
certificate export。

223. Monty Hall MVP

其實非常適合第一個實作。

參數：

\theta = ( p_1,p_2,p_3, \ell_1,\ell_2 ).

query：

Q_{\mathrm{obs}} = \frac{ p_2\ell_2 }{ p_1\ell_1+p_2\ell_2 }.

可以立刻做：

parameter search；
gap visualization；
closure conditions；
countermodel certificates。

224. 第二階段 MVP

再加入：

natural-language parser；
branch generator；
lift detector；
LLM cross-check。

225. 第三階段

加入：

SMT；
Lean；
probabilistic program；
causal models；
formal provenance graph。

226. SRBC 不應變成「疑心病引擎」

這是一個重要設計限制。

如果系統對每一句：

天空是藍的。

都生成一萬個 possible world，

那就失去實用性。

227. Query Relevance Filter

所有深度分析先問：

\boxed{ \text{這個歧義真的會改變 }Q\text{ 嗎？} }

若否：

\operatorname{Delay}.

228. Minimal Sufficient Semantics

理想目標：

\Gamma_{Q,\min}^{*}.

不是：

\Gamma_{\mathrm{world}}^{*}.

229. SRBC 不是世界模型終極化

它反而刻意拒絕：

\boxed{ \text{回答一題前先完整建構宇宙。} }

230. SRBC 是 query-directed epistemic compilation

可以把整個方法壓成：

\boxed{ \operatorname{EpistemicCompile} : (u,C,Q) \rightarrow ( \mathfrak I_Q, \mathsf R_Q, \operatorname{Cert}_Q ). }

231. Compilation 不保證唯一 answer

它保證：

\boxed{ \text{輸出狀態與證據型別被正確標記。} }

232. 這就是「可驗證形式化」的定義

本文中的 verifiable formalization 不等於：

\text{所有自然語言完全形式化}.

而是：

\boxed{ \text{形式化所新增、保留、排除與未決的語義責任都可被追蹤與檢驗。} }

233. 與傳統形式化的關係

傳統形式化：

u\rightarrow\phi.

SRBC 版本：

u \rightarrow ( \Gamma, \Theta, \mathfrak I, Q, \operatorname{Prov} ).

然後才可能：

\mathfrak I \rightarrow \phi_Q.

234. 這不是要取代形式語義學

形式語義學已經有：

underspecification；
DRT；
question semantics；
dynamic semantics；
pragmatics。

SRBC 的角色更偏：

\boxed{ \text{formalization audit + query closure + runtime provenance}. }

235. 也不是要取代概率論

概率論負責：

P_M.

SRBC 問：

\boxed{ \text{哪一個 }M\text{ 被 source 合法指定？} }

兩者是不同層。

236. 也不是要取代因果推論

因果推論負責：

P(Y\mid\operatorname{do}(X)).

SRBC 問：

causal graph 是 given、assumed、identified 還是 injected？

237. 也不是要取代 theorem proving

Theorem prover 負責：

\Gamma\vdash\phi.

SRBC 問：

$\Gamma$ 從哪來？

238. 所以 SRBC 是一個上層治理框架

最精確的定位之一是：

\boxed{ \text{Semantic Governance Layer for Formal Reasoning}. }

239. Governance 不是政治治理

此處 governance 指：

commitments；
provenance；
branches；
queries；
certificates；
reopen conditions。

240. 系列最終閉環

SRBC-01：

\text{symbol boundary}

SRBC-02：

\text{model family}

SRBC-03：

\text{query quotient}

SRBC-04：

\text{lift audit}

SRBC-05：

\text{gap measurement}

SRBC-06：

\text{semantic surgery}

SRBC-07：

\boxed{ \text{runtime methodology}. }

241. Formal Semantic Surgery 的最小定義

本文最終定義：

Formal Semantic Surgery 是一種 query-relative 形式化審計方法：它保留原 source，顯式建立合法語義完成族，區分 source commitment 與 completion commitment，以指定 query 對 branch 進行商化與敏感度分析，審計未證成語義升格，搜尋 countermodel，量化 query-relevant GAP，尋找最小閉合條件，並以可重放 certificate 記錄目前 resolution state 與 reopen condition。

242. 數學壓縮版

可寫：

\boxed{ \operatorname{FSS} (u,C,Q) = \operatorname{Cert} \left( \operatorname{Resolve}_Q \left( \operatorname{Audit} \left( \operatorname{Complete} ( u,C ) \right) \right) \right). }

243. 更完整的資料流

\boxed{ (u,C) \rightarrow \Gamma \rightarrow \Theta \rightarrow \mathfrak I \rightarrow Q \rightarrow \mathfrak G_Q \rightarrow \mathcal J \rightarrow \mathbf G_Q \rightarrow \Delta\Gamma^* \rightarrow \mathsf R_Q \rightarrow \operatorname{Cert}_Q \rightarrow \mathcal R_Q. }

244. QRSRC 的第一代定義

給定 semantic frame：

\Phi = ( u,C,\Lambda,\Gamma,Q,\operatorname{Adm},\mathcal V )

與 budget：

B,

若系統已建立：

source integrity；
query identity；
admissibility regime；
resolution certificate；
query-sensitive debt state；
known frontier；
reopen condition；

則稱：

\boxed{ \operatorname{QRSRC}_{\Phi,B}(Q) }

成立。

245. QRSRC 不要求 QRC

\operatorname{QRSRC}

可以包：

\operatorname{CertQRC},

\operatorname{CertQRU},

或：

\operatorname{CertQDU}.

246. 這讓「閉合」回到誠實

如果答案就是：

目前資訊不足以唯一回答。

且已被形式證明，

那就是：

\boxed{ \text{完成}. }

不必為了心理上想要單一答案而偷補假設。

247. 與 SREG PEC 的共同哲學

SREG PEC：

\boxed{ \text{有限邊界內的最大誠實完成}. }

SRBC QRSRC：

\boxed{ \text{指定 query 與 semantic frame 內的最大誠實解析完成}. }

248. 終端性仍然被拒絕

即使：

\operatorname{QRSRC}_{\Phi,B}

成立，

仍可能存在：

\Phi'

使舊結果重開。

所以：

\boxed{ \operatorname{QRSRC} \not\Rightarrow \operatorname{TerminalSemanticComplete}. }

249. 系列之後的研究優先序

七篇完成後，優先序應改為：

benchmark；
runtime；
countermodel search；
formal verification；
cross-model experiment；
measurement calibration；
才是第二代理論。

250. 第二代理論應由實驗逼出來

例如：

admissibility metric 是否可穩定？
GAP profile 哪些分量真的有用？
query compiler 最常錯在哪？
human / AI branch 差異多大？
semantic condition number 是否可預測錯誤？

這些應由資料決定。

251. 不預先創造不必要的新符號

這也回到 SRBC-01。

如果現有：

\Gamma, \Theta,\mathfrak I,Q,\mathcal J,\mathbf G_Q

已足夠，

就不應為了理論美觀無限造新 symbol。

新符號應在表示壓力真的超界時生成。

252. 系列本身也必須服從自己的規則

SRBC 不能說：

因為我們建立了這個框架，所以自然語言所有爭議都能被它解決。

這是非法全域升格。

正確說法是：

\boxed{ \text{SRBC 提供一組可測試、可失敗、可修正的語義審計方法。} }

253. 可證偽性

整個 SREG–SRBC 方法論應在以下情況被削弱或修正：

completion family 無法穩定重建；
admissibility 判定跨研究者高度不一致；
query quotient 無法有效降低 branch complexity；
lift audit 產生大量 false positive；
GAP metrics 無法預測任何實務差異；
minimal closure search 不比一般人工澄清有效；
certificates 無法跨模型 replay；
QRSRC 經 adversarial reopen 後頻繁崩潰；
runtime 成本遠高於其降低錯誤的價值；
benchmark 顯示傳統單一形式化在大多數 query-sensitive case 已足夠。

254. 成功條件

反之，如果實驗顯示：

hidden injection rate 可測；
countermodel-first 降低 false QRC；
query-directed branching 降低 clarification cost；
certificate 提高 replayability；
GAP profile 可預測脆弱性；
minimal closure 可穩定找到高資訊條件；

則 SRBC 取得更強支持。

255. 第一個正式研究里程碑

建議：

\boxed{ \text{SRBC Benchmark v0.1} }

至少 20 個 case。

每個 case 有：

source；
query；
gold branch；
QRC/QRU/QDU status；
critical lift；
countermodel；
closure candidate。

256. 第二個里程碑

\boxed{ \text{SRBC Runtime v0.1} }

支援：

YAML case；
parameterized completion；
query evaluator；
countermodel search；
GAP export；
certificate export。

257. 第三個里程碑

\boxed{ \text{SRBC Formal v0.1} }

把至少 Monty Hall 的核心命題進 Lean / Coq / SMT。

258. 第四個里程碑

\boxed{ \text{Cross-Model Semantic Surgery Experiment}. }

測不同 AI 的：

branch recall；
hidden lift；
query compilation；
certificate correctness。

259. 第五個里程碑

把 SRBC 接入：

\boxed{ \text{SREG long-horizon generation}. }

讓 SREG 每個 pulse 都帶 semantic audit snapshot。

260. 結論

SRBC 系列從一個看似很普通的問題開始：

一句自然語言是不是可能沒有把問題說完？

如果只停在這裡，答案當然是「可能」。

這不夠。

真正需要的是把「可能」拆開。

一個符號到底能承載多少？

\rightarrow \text{SRBC-01}

一段話到底允許哪些形式模型？

\rightarrow \text{SRBC-02}

多個模型是否真的改變我們正在問的問題？

\rightarrow \text{SRBC-03}

哪些看似自然的推理步驟其實偷偷增加了原句沒有承諾的結構？

\rightarrow \text{SRBC-04}

這個差異到底有多大、離閉合多遠、修補要多少成本？

\rightarrow \text{SRBC-05}

這整套東西放到經典 Monty Hall 上，是否真的能比舊式「有歧義」論證更強？

\rightarrow \text{SRBC-06}

最後：

能不能把它變成一套 AI、數學、科學與形式推理真正可以執行的研究流程？

\rightarrow \text{SRBC-07}.

因此，整個系列最後不是停在：

\boxed{ \text{Natural language is ambiguous}. }

而是進入：

\boxed{ \text{Semantic ambiguity can be represented, queried, audited, measured, certified, compressed, and reopened.} }

這就是 SRBC 與 SREG 合流後最重要的結果。

SREG 提供長時間尺度下：

\boxed{ \text{生成、探索、閉包與重開}. }

SRBC 提供每一次形式化內：

\boxed{ \text{表徵邊界、語義合法性、查詢敏感度、升格責任、GAP 與證書}. }

兩者合起來得到：

\boxed{ \text{SREG--SRBC Formal Semantic Surgery Runtime}. }

它的目標不是讓 AI 對所有問題都變得多疑。

也不是要求自然語言在進入計算前先變成一整個完整宇宙。

真正目標是：

\boxed{ \text{只在答案真正依賴未說明語義時，把那個依賴顯示出來。} }

如果不影響 query：

\operatorname{Delay}.

如果影響 query：

\operatorname{Branch}.

如果可以證唯一：

\operatorname{QRC}.

如果可以證不唯一：

\operatorname{QRU}.

如果問題本身還沒有被定義完：

\operatorname{QDU}.

最後把結果封裝成：

\operatorname{QRSRC}_{\Phi,B}.

並保存：

\operatorname{ReopenCondition}.

因此，這套方法論的最終原則不是：

\boxed{ \text{永遠不要做假設}. }

而是：

\boxed{ \text{知道哪些是假設，知道它們從哪來，知道它們改變了什麼。} }

也不是：

\boxed{ \text{所有問題都要唯一化}. }

而是：

\boxed{ \text{把「唯一、非唯一、未定義、未解」分清楚。} }

至此，SRBC 第一系列完成。

下一步不再是繼續替這套框架增加更多名詞。

下一步是：

\boxed{ \text{讓它真正接受世界、文本、AI、數學與形式系統的反覆壓測。} }

如果它能在這些壓測下持續找到真實的 hidden assumption、避免錯誤唯一化、生成可重放 countermodel、降低不必要澄清，並且讓形式結果的適用邊界更清楚，那麼它才真正從一套漂亮理論變成一套有用的方法。

參考與前置文件

SRBC 系列

Neo.K with Aletheia. 《SRBC-01｜符號表徵邊界：符號、符號域與概念承載上下限》. EveMissLab, 2026.
Neo.K with Aletheia. 《SRBC-02｜語義完成空間：從單一表述到形式模型族》. EveMissLab, 2026.
Neo.K with Aletheia. 《SRBC-03｜查詢相對完備性：自然語言歧義的形式判準》. EveMissLab, 2026.
Neo.K with Aletheia. 《SRBC-04｜語義越界與隱含結構注入：量詞、策略、時序與因果的非法升格》. EveMissLab, 2026.
Neo.K with Aletheia. 《SRBC-05｜語義缺口的測度：歧義寬度、完備距離與閉合代價》. EveMissLab, 2026.
Neo.K with Aletheia. 《SRBC-06｜Monty Hall 的語義手術：三門問題的模型族、完備條件與概率分岔》. EveMissLab, 2026.

SREG 與內部前置

Neo.K with Aletheia. 《SREG-F01｜從符號遊戲到數學宇宙實驗》. EveMissLab, 2026.
Neo.K with Aletheia. 《SREG-F03｜形式化壓縮與低歧義數學生成》. EveMissLab, 2026.
Neo.K with Aletheia. 《SREG-F04｜脈衝窮盡閉包》. EveMissLab, 2026.
Neo.K with Aletheia. 《SREG-F07｜脈衝閉包的廣義 Gödel 邊界》. EveMissLab, 2026.
Neo.K with Aletheia. 《符號操作性與可構造空間：從結構再激活到表示系統擴展》. EveMissLab, 2026.
Neo.K with Aletheia. 《OWER-07｜The Formalization Gap》. EveMissLab, 2026.

外部理論背景

Tarski, A. Logic, Semantics, Metamathematics. Oxford University Press, 1956.
Kamp, H., & Reyle, U. From Discourse to Logic. Kluwer Academic Publishers, 1993.
Reyle, U. "Dealing with Ambiguities by Underspecification: Construction, Representation and Deduction." Journal of Semantics, 10(2), 123-179, 1993.
Copestake, A., Flickinger, D., Pollard, C., & Sag, I. A. "Minimal Recursion Semantics: An Introduction." Research on Language and Computation, 3, 281-332, 2005.
Pearl, J. Causality: Models, Reasoning, and Inference. 2nd ed., Cambridge University Press, 2009.
Shannon, C. E. "A Mathematical Theory of Communication." Bell System Technical Journal, 27, 379-423 and 623-656, 1948.
Kolmogorov, A. N., & Tikhomirov, V. M. "ε-Entropy and ε-Capacity of Sets in Functional Spaces." Uspekhi Matematicheskikh Nauk, 14(2), 3-86, 1959.
Grice, H. P. "Logic and Conversation." In Syntax and Semantics, Vol. 3, 1975.

版本註記

v0.1 / 2026-09-23

完成 SRBC 01--07 全系列方法論閉環；
將 SRBC 正式接回 SREG Explore--Branch--Formalize--Verify--Merge--Compress--Reopen 循環；
建立統一 semantic research state $\mathfrak S_t$ ；
建立 Source Freeze 與 Source Version Graph；
建立 Representation Audit、Semantic Frame Extraction、Open Slot Detection、Completion Branching；
建立 Branch Legality Gate 與 branch provenance；
建立 Query Canonicalization 與 Query Versioning；
建立 Query Quotient、Query-Directed Compression 與 reversible merge；
建立 query-sensitive slot analysis 與 delayed commitment rule；
建立 Lift Ledger；
建立 QRC / QRU / QDU / UNRESOLVED resolution classifier；
建立 adversarial countermodel search；
建立 GAP Measurement 與 Minimal Closure Search；
建立多層 Verification State；
正式提出 Query-Relative Semantic Resolution Closure（QRSRC）；
明確允許 QRC、QRU、QDU 三種成功閉合；
建立 Conditional Closure 與 epsilon closure；
建立 semantic pulse 與 SREG PEC 接口；
建立 QRSRC Closure Artifact、Closure Gate、Debt Gate、Frontier Ledger 與 Budget Ledger；
建立 Semantic Adversarial Reopening Test（SART）；
建立 runtime state machine；
建立 Source Registry、Semantic Parser、Commitment Extractor、Completion Generator、Admissibility Checker、Query Compiler、Branch Quotient Engine、Lift Guard、Evaluator、Countermodel Searcher、GAP Analyzer、Closure Optimizer、Certificate Builder、Reopen Manager 十四模組；
建立 canonical YAML artifact schema；
建立 reversible semantic compression、branch DAG、semantic ledger、semantic diff；
建立 Formalization Compiler 的 family-valued 定義；
建立 fast path / slow path adaptive SRBC；
建立 solver / SMT / probabilistic program / proof assistant 接口；
建立 mixed-evidence certificate 與 closure maturity levels；
建立 Formal Semantic Surgery 的正式定義；
建立 QRSRC frame-bound nonterminal closure 定義；
建立 Phase II benchmark、runtime、formal verification、cross-model experiment 五階段研究綱領；
正式宣告 SRBC 第一系列由「理論建立期」進入「實驗與 runtime 研究期」。

從自然語言到可驗證形式化：SREG–SRBC 語義分支與閉合方法論

從自然語言到可驗證形式化

SREG–SRBC 語義分支與閉合方法論

Canonical Source Note

摘要

0. 系列收束：SRBC 到底完成了什麼？

1. 七篇論文的功能分解

SRBC-01：Symbolic Representation Bounds

SRBC-02：Semantic Completion Space

SRBC-03：Query-Relative Completeness

SRBC-04：Semantic Illegal Lifts

SRBC-05：Semantic GAP Measurement

SRBC-06：Monty Hall Semantic Surgery

SRBC-07：Methodology and Runtime

2. SREG 提供了什麼？

3. SRBC 補給 SREG 的內容

4. 統一架構

5. 第一代統一狀態 tuple

6. 為什麼 source 必須是一等物件？

7. Source Freeze

8. Source Version Graph

9. 第一階段：Representation Audit

10. Representation Audit Output

11. 第二階段：Semantic Frame Extraction

12. 不允許 provenance-free commitment

13. 第三階段：Open Slot Detection

14. Open Slot 不等於問題

15. 第四階段：Completion Branching

16. Completion Branch 必須自帶 provenance

17. Branch Legality Gate

18. 第五階段：Query Canonicalization

19. Query Schema

20. Query Versioning

21. 第六階段：Query Quotient

22. Query Quotient 的工程價值

23. Query-Directed Compression

24. 不可過度 merge

25. 第七階段：Query-Sensitive Slot Analysis

26. Delayed Commitment Rule

27. Clarification Rule

28. 第八階段：Lift Audit

29. Lift Ledger

30. Lift 不一定要刪除

31. 第九階段：Evaluate Branches

32. 計算工具不能決定 source semantics

33. 第十階段：Resolution Classification

34. QRC

35. QRU

36. QDU

37. UNRESOLVED

38. 第十一階段：Countermodel Search

39. Adversarial Semantic Search

40. Countermodel Priority

41. 第十二階段：GAP Measurement

42. GAP Measurement 不要求全量

43. 第十三階段：Minimal Closure Search

44. Minimal Closure 不是強迫 source 改寫

45. Closure Candidate Types

46. 第十四階段：Verification

47. Source Verification

48. Logical Verification

49. Model Verification

50. Numerical Verification

51. Simulation Verification

52. Provenance Verification

53. Replay Verification

54. 第十五階段：Closure

55. Resolution Closure

56. QRSRC 的三種成功狀態

56.1 Unique Closure

56.2 Underdetermination Closure

56.3 Undefinability Closure

57. 不能把 QRU 視為「研究失敗」

58. Conditional Closure

59. Epsilon Closure

60. QRSRC 不等於 Terminal Completeness

61. 與 SREG PEC 對接

62. Semantic Pulse

63. Closure Artifact

64. Closure Gate