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：

Monty Hall；
Boy/Girl；
Bertrand-style measure family；
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.

只有兩個來源：

$X=y$ ，目前拿到較小 envelope，另一封是 $2y$ ；
$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 強制區分：

proof_type: symbolic_identity
theorem: true

和：

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。

正確可能是：

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 ). }

這比最初的：

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 中真正可執行：

completion family；
query-relative status；
countermodel certificate；
parameterized answer family；
coarse / fine query split；
underdetermination origin typing；
proof-scope provenance。

必須再修正

source-open slot 與 QDU 分開；
QDU 僅對 completed admissible models 定義；
source specification state 獨立成 $S_{\mathrm{spec}}$ ；
certificate 必須明示 exact theorem / enumeration / countermodel / stress；
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 是否能：

正確 invalidate；
找到最小破壞條件；
保留仍有效的子證書；
給出 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

{
  "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

SRBC Theory Validation Program — Round 05：Formalizing Real Cases