title: SRBC Theory Validation Program — Round 01：形式核心壓測與第一輪反例
author: Neo.K with Aletheia (GPT-5.6 Sol)
institution: EveMissLab / 一言諾科技有限公司
version: v0.1
date: 2026-09-23
language: zh-TW
document_type: Theory Validation Report / Formal Stress Test
status: Round 01 completed

SRBC Theory Validation Program — Round 01

形式核心壓測、定義型別檢查與 Monty Hall 計算 sanity test

作者： Neo.K with Aletheia (GPT-5.6 Sol)
機構： EveMissLab / 一言諾科技有限公司
日期： 2026-09-23
版本： v0.1

Canonical Source Note

本報告以 UTF-8 Markdown 保存。數學 source 僅使用 $...$ 與 $$...$$。所有計算可由同包內 srbc_validation_round01.py 使用固定 seed 7777 重放；原始機器結果保存在 results_round01.json。

0. 本輪目的

本輪不是再用 SRBC 寫一篇應用論文，而是直接攻擊 SRBC 自己。

測試分三層：

有限形式空間窮舉：檢查 SRBC-03 / SRBC-05 的核心命題是否在小型離散模型中出現反例；
邊界與型別測試：專門找 partial query、空 completion、近似等價等定義漏洞；
Monty Hall 計算 sanity test：檢查 SRBC-06 的一般式、區間與 tie-breaking 敏感性是否經直接計算與模擬支持。

本輪原則：

\boxed{ \text{找到反例就改理論，不替理論護航。} }

1. 執行摘要

1.1 通過壓測的核心

有限 total-query 空間共檢查：

3,279

個 query assignments，以及：

332,643

個非空 constraint-strengthened 子空間。

找到核心反例：

\boxed{0}.

未被打穿的命題包括：

\operatorname{QRC} \iff \Delta_Q=0

在 completion space 非空、 $Q$ total、 $d_Q$ 為 metric 的條件下；

M_i,M_j\in\mathfrak I, \quad Q(M_i)\neq Q(M_j) \Rightarrow \neg\operatorname{QRC};

以及固定 query / metric 下：

\mathfrak I' \subseteq \mathfrak I \Rightarrow \Delta_Q(\mathfrak I') \le \Delta_Q(\mathfrak I).

Query hierarchy 另檢查：

8,736

組合成映射，也未找到：

Q_2\text{ 完備} \land Q_1=f\circ Q_2 \land Q_1\text{ 不完備}

的反例。

1.2 第一輪直接找到的形式問題

本輪找到三個必須修補的核心問題，外加一個 theorem boundary。

Bug A：QDU 與 QRU 不是互斥

對三個 completion 的 partial query：

Q(M_1)=\bot, \quad Q(M_2)=0, \quad Q(M_3)=1,

同時有：

\operatorname{QDU}=1

與：

\operatorname{QRU}=1.

枚舉全部：

3^3=27

個 {undefined,0,1} 配置後，有：

\boxed{6}

種同時為 QDU 與 QRU。

所以：

\operatorname{QRC}, \operatorname{QRU}, \operatorname{QDU}

不能被設計成單一互斥 enum。

Bug B：partial query 下 quotient 與 diameter 型別不完整

若：

Q: \mathfrak I \rightharpoonup \mathcal A_Q

是部分函數，而：

\sim_Q

只在：

\operatorname{Dom}(Q)

上有定義，則應先定義：

\boxed{ \mathfrak I_Q^{\mathrm{def}} = \mathfrak I \cap \operatorname{Dom}(Q). }

再定義：

\boxed{ \mathfrak G_Q^{\mathrm{def}} = \mathfrak I_Q^{\mathrm{def}}/{\sim_Q}. }

同理，歧義直徑應改為：

\boxed{ \Delta_Q^{\mathrm{def}} = \operatorname{diam} Q[ \mathfrak I_Q^{\mathrm{def}} ]. }

如果：

\mathfrak I_Q^{\mathrm{def}} = \varnothing,

則 $\Delta_Q^{\mathrm{def}}$ 應標 undefined / not-applicable，而不是默認成 $0$ 。

Bug C： $\varepsilon$ -proximity 不是一般等價關係

若定義：

M_i\approx_{Q,\varepsilon}M_j \iff d_Q(Q(M_i),Q(M_j)) \le \varepsilon,

它一般不具遞移性。

最小反例之一：

a=0, \quad b=0.6, \quad c=1.2, \quad \varepsilon=0.7.

有：

a\approx b,

b\approx c,

但：

a\not\approx c.

所以它只能叫 proximity relation，不能直接拿來做 quotient。

容差完備應保留：

\boxed{ \operatorname{QRC}_{\varepsilon} \iff \Delta_Q^{\mathrm{def}} \le \varepsilon. }

Boundary D：QRC 與零直徑等價需要非空 completion

若：

\mathfrak I=\varnothing,

則答案像也是空集合，QRC 依原定義不成立；但空集合直徑依數學 convention 可能被設為 $0$ 、 $-\infty$ 或未定義。

因此 theorem 必須明示：

\boxed{ \mathfrak I\neq\varnothing. }

2. 建議的新 resolution 結構

不要再用：

QRC | QRU | QDU | UNRESOLVED

作為單一 enum。

改成三軸：

2.1 Definability

D_Q \in \{ \operatorname{TOTAL}, \operatorname{PARTIAL}, \operatorname{NONE} \}.

2.2 Answer variation

V_Q \in \{ \operatorname{NONE}, \operatorname{SINGLE}, \operatorname{MULTIPLE} \}.

2.3 Evidence state

E_Q \in \{ \operatorname{PROVED}, \operatorname{REFUTED}, \operatorname{UNKNOWN} \}.

因此：

\boxed{ \mathbf R_Q = (D_Q,V_Q,E_Q). }

並定義：

\operatorname{QRC} \iff D_Q=\operatorname{TOTAL} \land V_Q=\operatorname{SINGLE}.

\operatorname{QRU} \iff V_Q=\operatorname{MULTIPLE}.

\operatorname{QDU} \iff D_Q\neq\operatorname{TOTAL}.

因此：

\operatorname{QRU}\land\operatorname{QDU}

是合法狀態。

而 UNRESOLVED 應屬於 $E_Q$ ，不是與 QRC / QRU / QDU 同層的世界語義類別。

3. Constraint-strengthening 壓測

對：

n=1,\ldots,7

與答案字母表：

\{0,1,2\},

窮舉所有 total query assignment，再窮舉每個 completion space 的所有非空子集。

總檢查：

query assignments：3,279
nonempty subsets：332,643
failures：0

因此計算壓測支持固定 $Q$ 、固定 metric、單純縮小 completion space 時：

\boxed{ \Delta_Q' \le \Delta_Q. }

這不是以有限枚舉取代一般證明；一般證明仍然只是「子集的直徑不大於母集合直徑」。本輪作用是檢查定義與實作沒有藏住小型反例。

4. Query hierarchy 壓測

若：

Q_1=f\circ Q_2,

則 $Q_2$ 是更細的 query。

本輪窮舉：

8,736

組 finite query / coarse-map，結果：

\boxed{ \operatorname{QRC}(Q_2) \Rightarrow \operatorname{QRC}(Q_1) }

沒有反例。

反向不成立。

最小例：

Q_2(M_1)=0, \quad Q_2(M_2)=1,

但取常數 coarse map：

f(0)=f(1)=0,

就有：

Q_1(M_1)=Q_1(M_2)=0.

因此 coarse query 可完備，而 fine query 不完備。

5. 「沒找到反例」的抽樣風險

設 completion population 有 $1000$ 個模型，其中只有 $1\%$ 是 divergent branch。

隨機不放回抽樣完全 miss divergent branch 的概率：

sample size	miss probability
5	95.089%
10	90.397%
25	77.543%
50	59.731%
100	34.693%
200	10.616%

也就是即使抽 $100$ 個 completion，仍有約：

34.69\%

機率完全沒看到那 $1\%$ 的反例族。

如果反例族只有 $0.1\%$ ，抽 $100$ 個仍有：

90.00\%

機率 miss。

因此計算直接支持：

\boxed{ \text{sampling agreement} \not\Rightarrow \text{QRC proof}. }

6. Monty Hall 直接計算 sanity test

6.1 一般後驗式

測試：

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

隨機生成 $10,000$ 組：

(p_1,p_2,p_3,\ell_1,\ell_2)

並用直接事件權重重建 Bayes 後驗。

最大差：

\boxed{ 0.0 }.

6.2 Standard symmetric

p_1=p_2=p_3=\frac13,

\ell_1=\frac12, \quad \ell_2=1.

得到：

\boxed{ Q_{\mathrm{obs}} = \frac23. }

6.3 Random-unchosen completion

\ell_1=\ell_2=\frac12

得到：

\boxed{ Q_{\mathrm{obs}} = \frac12. }

6.4 Standard goat family

掃描：

\alpha\in[0,1]

共 $1001$ 點，得到：

\boxed{ Q_{\mathrm{obs}} \in \left[ \frac12,1 \right]. }

機器值：

[0.5, 1.0]

6.5 Broad policy family

對：

\ell_1,\ell_2 \in \{0,0.01,\ldots,1\}

掃描 $101\times101$ 網格，排除 $(0,0)$ ，得到：

\boxed{ Q_{\mathrm{obs}} \in [0,1]. }

機器值：

[0.0, 1.0]

7. Tie-breaking 對 ex ante query 的模擬

在 standard goat-opening protocol 中改變：

\alpha = P(H=d_3\mid C=d_1).

每一個 $\alpha$ 各跑 $200,000$ 次：

alpha	always-switch win rate	door3 open rate
0.0	0.667090	0.334455
0.1	0.668405	0.368085
0.5	0.667270	0.498405
0.9	0.667745	0.633090
1.0	0.666520	0.666335

always-switch win rate 都穩定在：

\frac23

附近，而 door3_open_rate 隨 $\alpha$ 明顯變化。

這直接支持 SRBC-06 的 query 分離：

\boxed{ Q_{\mathrm{ex}} \text{ 對 tie-breaking 不敏感} }

但：

\boxed{ Q_{\mathrm{obs}} \text{ 對 tie-breaking 敏感}. }

8. Monte Carlo 後驗 sanity check

四組不同 $(p,\ell_1,\ell_2)$ 各跑 $200,000$ 次。

p	l1	l2	analytic	simulation	abs error
`(0.3333, 0.3333, 0.3333)`	0.500	1.000	0.666667	0.666753	0.000087
`(0.3333, 0.3333, 0.3333)`	0.500	0.500	0.500000	0.500218	0.000218
`(0.5, 0.3, 0.2)`	0.200	0.900	0.729730	0.728298	0.001432
`(0.2, 0.7, 0.1)`	0.800	0.100	0.304348	0.305201	0.000853

最大模擬誤差小於 $0.0015$ 。

此處 simulation 只驗證：

Q(M)

的計算，不拿來證：

u\mapsto M

的唯一性。

9. Round 01 正式修補提案

Patch 01 — Partial Query Core

新增：

\mathfrak I_Q^{\mathrm{def}} = \mathfrak I\cap\operatorname{Dom}(Q).

所有 exact answer quotient 建在：

\mathfrak I_Q^{\mathrm{def}}

上。

Patch 02 — Orthogonal Resolution State

將 runtime 狀態從單一 enum 改成：

\mathbf R_Q=(D_Q,V_Q,E_Q).

Patch 03 — Defined-Answer Diameter

改：

\Delta_Q^{\mathrm{def}} = \operatorname{diam} Q[ \mathfrak I_Q^{\mathrm{def}} ].

若沒有 defined completion，值標 N/A。

Patch 04 — Exact QRC Boundary

使用：

\operatorname{QRC} \iff \Delta_Q=0

前必須明示：

\mathfrak I\neq\varnothing,

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

以及 $d_Q$ 是 metric。

Patch 05 — Epsilon Proximity

把：

\sim_{Q,\varepsilon}

改為：

\approx_{Q,\varepsilon}

並明示其只是 proximity。

不建立 quotient。

容差 closure 用：

\Delta_Q^{\mathrm{def}} \le \varepsilon.

Patch 06 — QRSRC Schema

建議：

resolution:
  definability: total | partial | none
  answer_variation: single | multiple | none
  proof_status: proved | refuted | unknown

  qrc: true | false | unknown
  qru: true | false | unknown
  qdu: true | false | unknown

其中：

qru: true
qdu: true

是合法組合。

10. 本輪總判定

暫時得到支持

在本輪範圍內未被打穿：

total-query 下 QRC 與零直徑等價；
countermodel theorem；
fixed-query constraint-strengthening 單調性；
QRC 對非空子空間保持；
fine-query complete $\Rightarrow$ coarse-query complete；
SRBC-06 Monty Hall 的核心後驗公式；
standard goat family 的 $[1/2,1]$ ；
broad policy family 的 $[0,1]$ ；
ex ante $2/3$ 對 tie-breaking 的不敏感性。

必須修正

已找到：

\boxed{3}

個核心形式問題：

QDU / QRU overlap；
partial-query quotient / diameter domain typing；
$\varepsilon$ -proximity non-transitivity。

以及一個 theorem boundary：

QRC-- $\Delta_Q=0$ 需明示 nonempty completion。

11. 研究意義

第一輪最重要的結果不是「大部分過了」。

而是：

\boxed{ \text{SRBC 已經開始承受真正的反例壓力。} }

而且第一次就找到了定義層 bug，不是文風問題。

所以接下來的正確節奏應保持：

\boxed{ \text{命題} \rightarrow \text{計算／窮舉／形式驗證} \rightarrow \text{反例} \rightarrow \text{canonical patch} \rightarrow \text{再測}. }

12. 下一輪：Synthetic Semantic Worlds

Round 02 不再只測抽象集合定理。

直接生成具有已知 ground truth 的世界：

W_i,

再從每個世界自動產生：

完整描述；
欠規格描述；
hidden-lift trap；
query-neutral ambiguity；
query-sensitive ambiguity；
partial-query case。

因為 ground truth 已知，可以真正在資料上測：

completion recall；
false completion rate；
hidden-lift detection；
QRC false positive；
QRU recall；
QDU detection；
minimal closure accuracy；
clarification efficiency。

這會第一次測：

\boxed{ \text{SRBC 是否真的能從語言恢復該恢復的語義結構。} }

而不只是測內部數學一致性。

附錄 A：機器摘要

assignments checked: 3,279
nonempty subsets checked: 332,643
core failures: 0
query-hierarchy cases: 8,736
QDU+QRU overlap: 6 / 27
Monty random analytic cases: 10000
Monty max analytic reconstruction error: 0.0
standard-goat range: [0.5, 1.0]
broad-policy range: [0.0, 1.0]

附錄 B：重放

同包包含：

srbc_validation_round01.py
results_round01.json

執行：

python srbc_validation_round01.py

即可重新產生機器結果。

SRBC Theory Validation Program — Round 01：形式核心壓測與第一輪反例