---
title: "SRBC Theory Validation Program — Round 05：Formalizing Real Cases"
author: "Neo.K with Aletheia (GPT-5.6 Sol)"
institution: "EveMissLab / 一言諾科技有限公司"
version: "v0.1"
date: "2026-09-23"
language: "zh-TW"
document_type: "Machine-Replayable Real-Case Formalization Report"
status: "Round 05 completed"
---

# SRBC Theory Validation Program — Round 05

## Formalizing Real Cases：從真實文本 transfer 到可重放機器證書

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

---

## Canonical Source Note

本報告以 UTF-8 Markdown 保存；數學 source 僅使用 ` $...$ ` 與 `$$...$$`。Round 05 不再新增 taxonomy，而是把四類 real-text case 轉成 machine-replayable model / symbolic certificate：

1. Monty Hall；
2. Boy/Girl；
3. Bertrand-style measure family；
4. Two Envelopes。

每一項 certificate 都區分 source / completion assumptions、query、proof scope、proof type，以及 exact theorem 與 stress evidence。

---

# 0. 本輪目的

Round 04 已證明 SRBC 的 closure machinery 可以 transfer 到真實經典問題，但 underdetermination origin 需要分層。

Round 05 進一步問：

$$
\boxed{
\text{這些 real-text cases 能不能真的被轉成可執行模型與可重放證書？}
}
$$

答案是：

$$
\boxed{
\text{可以，但 formalization 又逼出一個 v0.5 型別修正。}
}
$$

---

# 1. Machine certificates

本輪產生：

$$
\boxed{
14
}
$$

個 machine-readable certificates。

| claim | case | proof type | status |
|---|---|---|---|
| MH-C1 | MH | symbolic_identity | PASS |
| MH-C2 | MH | symbolic_substitution | PASS |
| MH-C3 | MH | symbolic_substitution | PASS |
| MH-C4 | MH | symbolic_family | PASS |
| MH-C5 | MH | finite_enumeration | PASS |
| BG-C1 | BG | finite_enumeration | PASS |
| BG-C2 | BG | finite_observation_protocol | PASS |
| BG-C3 | BG | finite_enumeration | PASS |
| BG-C4 | BG | symbolic_likelihood_family | PASS |
| BER-C1 | BER | symbolic_change_of_parameter | PASS |
| BER-C2 | BER | symbolic_monotonicity | PASS |
| TE-C1 | TE | symbolic_bayes_expectation | PASS |
| TE-C2 | TE | exact_countermodel_pair | PASS |
| TE-C3 | TE | symbolic_symmetry_plus_random_stress | PASS |

使用兩種 backend：

- Python `Fraction`：exact finite enumeration；
- SymPy：symbolic identity / parameter-family algebra。

本環境沒有 Z3，因此本輪沒有假裝產生 SMT-solver proof。這不影響有限枚舉與 symbolic identity 的可重放性，但也意味著「SMT certificate」仍是未來工作。

---

# 2. Monty Hall：finite kernel + symbolic posterior

一般 observed-door posterior：

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

SymPy 代入 standard symmetric：

$$
p_1=p_2=\frac13,
\quad
\ell_1=\frac12,
\quad
\ell_2=1
$$

得到：

$$
\boxed{
\frac23.
}
$$

random-unchosen：

$$
\ell_1=\ell_2=\frac12
$$

得到：

$$
\boxed{
\frac12.
}
$$

standard goat family：

$$
\ell_1=\alpha,
\quad
\ell_2=1
$$

得到：

$$
\boxed{
Q_{\mathrm{obs}}(\alpha)
=
\frac1{1+\alpha}.
}
$$

而：

$$
\frac{dQ}{d\alpha}
=
-\frac1{(1+\alpha)^2}
<
0.
$$

所以：

$$
\alpha\in[0,1]
\Rightarrow
Q_{\mathrm{obs}}
\in
\left[
\frac12,1
\right].
$$

---

# 3. Monty Hall：ex-ante query 的有限證書

標準 goat-opening protocol 下，車只可能在：

$$
d_1,d_2,d_3.
$$

player 先選：

$$
d_1.
$$

always-switch：

- $C=d_1$：輸；
- $C=d_2$：贏；
- $C=d_3$：贏。

等先驗：

$$
\boxed{
P(\text{always-switch wins})
=
\frac23.
}
$$

此 finite certificate 完全沒有用：

$$
\alpha.
$$

所以再次確認：

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

---

# 4. Boy/Girl：observation protocol 被真正機器化

完整 ordered family：

$$
\{
BB,BG,GB,GG
\}
$$

各先驗：

$$
\frac14.
$$

## 4.1 Condition on family event

「至少一個 boy」的 likelihood：

$$
(1,1,1,0).
$$

因此：

$$
\boxed{
P(BB\mid \text{at least one boy})
=
\frac13.
}
$$

## 4.2 Random-child reporting protocol

隨機挑一個孩子並回報該孩子為 boy。

report likelihood：

$$
\left(
1,\frac12,\frac12,0
\right).
$$

因此：

$$
\boxed{
P(BB\mid \text{reported boy})
=
\frac12.
}
$$

## 4.3 Older-child query

older child is girl：

$$
(0,0,1,1).
$$

因此：

$$
\boxed{
P(GG\mid \text{older child is girl})
=
\frac12.
}
$$

---

# 5. Boy/Girl 的一般 observation formula

令：

$$
a=P(R\mid BB),
$$

$$
b=P(R\mid BG),
$$

$$
c=P(R\mid GB),
$$

且：

$$
P(R\mid GG)=0.
$$

等先驗下：

$$
\boxed{
P(BB\mid R)
=
\frac{a}{a+b+c}.
}
$$

因此：

$$
\boxed{
\text{同一個被回報的 proposition}
\neq
\text{唯一 information-generation protocol}.
}
$$

這和 Monty Hall 的 host action likelihood 具有同一高階結構。

---

# 6. Bertrand-style cube：measure family 的 symbolic certificate

令：

$$
L\in[0,1]
$$

為 cube side length。

不直接假設 $L$ uniform，而令：

$$
U=L^r
$$

在：

$$
[0,1]
$$

上 uniform，其中：

$$
r>0.
$$

則：

$$
P(L<x)=x^r.
$$

所以：

$$
\boxed{
P\left(L<\frac12\right)
=
2^{-r}.
}
$$

具體：

$$
r=1
\Rightarrow
\frac12
$$

是 uniform length；

$$
r=2
\Rightarrow
\frac14
$$

是 uniform face area；

$$
r=3
\Rightarrow
\frac18
$$

是 uniform volume。

而：

$$
\frac{d}{dr}2^{-r}
=
-\log(2)2^{-r}
<
0.
$$

所以 $r>0$ 時，這個 family 的 answer image 是：

$$
\boxed{
(0,1).
}
$$

---

# 7. Round 05 第一個理論修正：measure-open 不等於 QDU

這個 formalization 把一件事逼得很清楚。

source：

> randomly produce a cube

沒有固定：

$$
r.
$$

但每一個 completion：

$$
M_r
$$

都已經是一個完整 probability model，而且：

$$
Q(M_r)=2^{-r}
$$

完全有定義。

所以：

$$
\boxed{
\Theta_{\mathrm{measure}}\neq\varnothing
}
$$

可以造成：

$$
\boxed{
\operatorname{QRU}=1
}
$$

但不必有：

$$
\operatorname{QDU}=1.
$$

因此：

$$
\boxed{
\text{source specification openness}
\neq
\text{query undefinability}.
}
$$

這就是 v0.5 的核心修正。

---

# 8. Two Envelopes：general prior formula

令：

$$
X
$$

為較小 envelope amount，具有 prior：

$$
p_X.
$$

隨機拿一封 envelope 後觀察：

$$
Y=y.
$$

只有兩個來源：

1. $X=y$，目前拿到較小 envelope，另一封是 $2y$ ；
2. $X=y/2$，目前拿到較大 envelope，另一封是 $y/2$。

因此：

$$
\boxed{
E[O\mid Y=y]
=
y
\frac{
2p_X(y)+\frac12p_X(y/2)
}{
p_X(y)+p_X(y/2)
}.
}
$$

減掉留下的：

$$
y
$$

得到：

$$
\boxed{
E[O-Y\mid Y=y]
=
y
\frac{
p_X(y)-\frac12p_X(y/2)
}{
p_X(y)+p_X(y/2)
}.
}
$$

所以 switch beneficial 當且僅當：

$$
\boxed{
2p_X(y)>p_X(y/2).
}
$$

---

# 9. Two Envelopes：exact countermodel pair

固定：

$$
Y=4.
$$

## Prior A

$$
p_X(2)=\frac1{10},
\quad
p_X(4)=\frac6{10},
$$

其餘 finite support 合法補滿。

得到：

$$
\boxed{
E[O\mid Y=4]
=
\frac{50}{7}
>
4.
}
$$

所以 switch。

## Prior B

$$
p_X(2)=\frac6{10},
\quad
p_X(4)=\frac1{10}.
$$

得到：

$$
\boxed{
E[O\mid Y=4]
=
\frac{20}{7}
<
4.
}
$$

所以 stay。

因此：

$$
\boxed{
\text{同一 observed amount}
+
\text{不同 proper prior}
\Rightarrow
\text{相反 recommendation}.
}
$$

這是一個 exact finite countermodel certificate。

---

# 10. Two Envelopes：ex-ante query 反而閉合

尚未打開 envelope 前，若：

$$
E[X]<\infty,
$$

隨機拿到的 envelope 期望：

$$
E[Y]
=
\frac12E[X]
+
\frac12E[2X]
=
\frac32E[X].
$$

另一封 envelope 的 ex-ante 期望因交換對稱性也為：

$$
\frac32E[X].
$$

所以：

$$
\boxed{
E[\text{switch gain before observing}]
=
0.
}
$$

本輪另外生成：

$$
\boxed{
10000
}
$$

組 proper finite-support rational priors 做 exact `Fraction` implementation stress，全數通過。

這再次得到：

$$
\boxed{
\text{ex-ante query closed}
}
$$

而：

$$
\boxed{
\text{observed-value query prior-relative}.
}
$$

---

# 11. Stress evidence 不得冒充 theorem

10,000 組 prior 全通過，不是 theorem 的來源。

真正 theorem 來自 envelope symmetry：

$$
E[Y]
=
E[O]
=
\frac32E[X].
$$

random stress 只是：

$$
\boxed{
\text{implementation sanity evidence}.
}
$$

因此 v0.5 certificate schema 強制區分：

```yaml
proof_type: symbolic_identity
theorem: true
```

和：

```yaml
proof_type: randomized_stress
theorem: false
```

---

# 12. QDU 必須 completion-relative

v0.5 將 QDU 的型別邊界固定為：

$$
\boxed{
\operatorname{QDU}(u,C;Q)
\iff
\exists M\in\mathfrak I(u,C):
M\notin\operatorname{Dom}(Q).
}
$$

其中：

$$
M
$$

必須已是 admissible completion。

所以：

> source 沒寫 prior

不是 QDU。

正確可能是：

```yaml
source_specification: open
open_slots:
  - prior
qru: true
qdu: false
```

若未來 completion family 納入：

- infinite expectation；
- non-integrable utility；
- genuinely undefined conditional；

才會真正進 QDU。

---

# 13. Source Specification Status

新增：

$$
S_{\mathrm{spec}}
\in
\{
\operatorname{CLOSED},
\operatorname{OPEN},
\operatorname{CONFLICT}
\}.
$$

因此目前完整 state 可寫：

$$
\boxed{
\mathbf S_Q
=
(
F_{\mathrm{src}},
S_{\mathrm{spec}},
O_{\mathrm{und}},
D_Q,
V_Q,
A_Q,
E_Q
).
}
$$

這比最初的：

```text
QRC | QRU | QDU
```

已經嚴格很多。

---

# 14. 四案例 machine status

## Monty Hall

- open slots：protocol / prior；
- observed-door query：QRU across protocol completions；
- standard ex-ante query：QRC；
- proof：symbolic + finite enumeration。

## Boy/Girl

- open slot：information-generation protocol；
- report query：QRU；
- protocol fixed 後：QRC；
- proof：finite enumeration + symbolic likelihood family。

## Bertrand

- open slot：probability measure；
- query 在每個 $r>0$ completion 中有定義；
- across measures：QRU；
- QDU：false in this completion family；
- proof：symbolic parameter family。

## Two Envelopes

- open slots：prior / expectation regime；
- proper finite-support prior family：observed query QRU；
- finite-expectation ex-ante query：QRC；
- proof：symbolic identity + exact countermodel pair。

---

# 15. 本輪對 SRBC 的結果

## 得到更強支持

以下結構已在 real-case machine formalization 中真正可執行：

1. completion family；
2. query-relative status；
3. countermodel certificate；
4. parameterized answer family；
5. coarse / fine query split；
6. underdetermination origin typing；
7. proof-scope provenance。

## 必須再修正

1. source-open slot 與 QDU 分開；
2. QDU 僅對 completed admissible models 定義；
3. source specification state 獨立成 $S_{\mathrm{spec}}$ ；
4. certificate 必須明示 exact theorem / enumeration / countermodel / stress；
5. countermodel pair 只證非唯一與 GAP lower bound，不能自動宣稱完整 answer range。

---

# 16. Round 05 最重要的結構

現在 SRBC 的流程可以排成：

$$
\boxed{
\text{Source}
\rightarrow
\text{Open Slots}
\rightarrow
\text{Admissible Completions}
\rightarrow
\text{Query Domain}
\rightarrow
\text{Answer Variation}.
}
$$

其中：

$$
\boxed{
\text{Open Slots}
\neq
\text{QDU}.
}
$$

以及：

$$
\boxed{
\text{multiple completions}
\neq
\text{QRU}
}
$$

除非答案真的分岔。

最後：

$$
\boxed{
\text{QRU}
\neq
\text{source-language defect}
}
$$

除非 origin analysis 確實指向 source / protocol / measure 等 specification layer。

到 Round 05，最早較直覺式的 SRBC 已經被四輪驗證逐步修成 typed framework。

---

# 17. Round 06

下一輪最自然的不是再加 puzzle，而是：

$$
\boxed{
\text{Certificate Mutation / Proof Robustness}.
}
$$

對本輪 14 個 certificates 主動做：

- 刪 assumption；
- 加錯 assumption；
- 改 query；
- 改 support；
- 改 prior；
- 改 observation likelihood；
- 把 stress evidence 冒充 theorem。

直接測 certificate system 是否能：

1. 正確 invalidate；
2. 找到最小破壞條件；
3. 保留仍有效的子證書；
4. 給出 reopen reason。

這才真正開始測 QRSRC / SART 本身。

---

# 參考錨點

- Adam Elga, *Self-locating belief and the Sleeping Beauty problem*, Analysis 60(2), 143–147, 2000.
- Stanford Encyclopedia of Philosophy, *Infinity: Tacitly Infinite Decision Problems — Two Envelopes*.
- Stanford Encyclopedia of Philosophy, *Causal Decision Theory* / Newcomb's Problem.
- Scientific American / Martin Gardner two-child problem historical formulation.
- SRBC-06 Monty Hall Semantic Surgery.

---

# 附錄 A：Machine results

```json
{
  "monty_hall": {
    "general_posterior": "l2*p2/(l1*p1 + l2*p2)",
    "standard_symmetric": "2/3",
    "random_unchosen": "1/2",
    "standard_goat_family": "1/(alpha + 1)",
    "family_derivative": "-1/(alpha + 1)**2",
    "family_range_alpha_0_1": [
      "1/2",
      "1"
    ],
    "ex_ante_always_switch": "2/3",
    "ex_ante_tie_break_dependency": false
  },
  "boy_girl": {
    "at_least_one_boy": "1/3",
    "random_child_report_boy": "1/2",
    "older_child_girl": "1/2",
    "general_report_formula": "a/(a + b + c)"
  },
  "bertrand_cube": {
    "family": "U=L^r Uniform(0,1), r>0",
    "P_L_lt_half": "2**(-r)",
    "derivative": "-log(2)/2**r",
    "r_1_2_3": {
      "1": "1/2",
      "2": "1/4",
      "3": "1/8"
    },
    "range_r_positive": "(0,1)"
  },
  "two_envelopes": {
    "conditional_expected_other": "y*(p_half + 4*p_y)/(2*(p_half + p_y))",
    "conditional_gain": "-y*(p_half - 2*p_y)/(2*(p_half + p_y))",
    "switch_condition": "2*p_y > p_half",
    "prior_A_E_other_given_Y4": "50/7",
    "prior_B_E_other_given_Y4": "20/7",
    "prior_A_switch": true,
    "prior_B_switch": false,
    "ex_ante_expected_gain": "0",
    "random_rational_priors_checked": 10000,
    "stress_pass": true
  },
  "formal_status": {
    "MH": {
      "open_slots": [
        "host policy",
        "tie-breaking",
        "prior"
      ],
      "status": "QRU for observed-door query across protocol completions; QRC ex-ante under standard protocol."
    },
    "BG": {
      "open_slots": [
        "information-generation protocol"
      ],
      "status": "QRU across report protocols; QRC after protocol is fixed."
    },
    "BER": {
      "open_slots": [
        "probability measure"
      ],
      "status": "QRU across completed measures; source openness alone is not QDU."
    },
    "TE": {
      "open_slots": [
        "prior distribution",
        "expectation regime"
      ],
      "status": "QRU across proper finite priors for observed-value query; ex-ante query QRC under finite expectation."
    }
  }
}
```

---

# 附錄 B：Artifacts

- `SRBC_Theory_Validation_Round05_Report_v0.1_2026-09-23.md`
- `SRBC_Core_Patch_v0.5_2026-09-23.md`
- `results_round05.json`
- `certificate_index.json`
- `certificates/*.json`
- `round05_replay.py`
- `manifest.yaml`
- `validation.json`