# Series C / Paper 04
# 計算機作為相對客觀認知載體：跨判定域驗證、信任鏈與異質錯誤通道
## Computers as Relatively Objective Epistemic Carriers: Cross-Domain Verification, Trust Chains, and Heterogeneous Error Channels

版本：v0.1  
日期：2026-08-14  
狀態：Theory + executable counterexample paper

## 摘要

大型語言模型可以生成自然語言 claim、程式、資料分析、測試、形式化敘述與 proof artifact；但「模型生成了一個看似合理的結果」與「某個外部判定系統實際接受或執行了該 artifact」具有不同的認識論地位。本文提出 **Relatively Objective Epistemic Carrier（相對客觀認知載體）**，用以描述程式執行器、編譯器、測試框架、reproducible build system、formal verifier、theorem prover 與獨立 proof checker 在 AI 研究閉環中的角色。

本文中的「相對客觀」不表示計算機完備、不出錯或等於真理。相反地，本文將計算驗證明確建模為條件信任鏈：

$$
\text{world claim}
\rightarrow
\text{formalization/specification}
\rightarrow
\text{artifact}
\rightarrow
\text{compiler/interpreter}
\rightarrow
\text{runtime}
\rightarrow
\text{verifier}
\rightarrow
\text{certificate}.
$$

若 specification fidelity、verifier soundness、semantic preservation、runtime/environment assumptions 均成立，則 machine acceptance 可被提升為對原 claim 的條件性支持；若其中任一關鍵邊界失效，machine acceptance 不再保證 world-level correctness。

本文證明四個基礎結果。

第一，**Conditional Carrier Soundness**：若每個 translation / execution / verification link 都 sound，則 carrier acceptance 對原 claim sound。

第二，**Trust-Boundary Union Bound**：若 false certificate 只能在至少一個信任邊界失效時發生，則 false-certificate event 的機率被各 boundary failure probability 的 union bound 所控制。

第三，**Reproducibility Orthogonality**：deterministic reproducibility 只能證明固定 artifact 在固定 capture 條件下可重放，不能單獨推出 artifact 符合正確 specification；因此錯誤程式可以穩定、精確而可重現地產生錯誤答案。

第四，**Heterogeneous Carrier Suppression**：在 false-accept events 條件獨立時，多個異質 carrier 同時錯誤接受 false claim 的機率乘法下降；但若存在 common-mode failure，該收益會被共同失效機率形成下限。

公開技術系統提供了這一理論的現實對照。Lean 以小型 trusted kernel 檢查 core terms，並提供 independent checker / comparator 路徑以進一步降低單一實作錯誤的風險；CompCert 將 compiler passes 的 semantic preservation 機器化證明；Nix reproducible-build infrastructure 把 dependency 與 sandbox 納入重建條件；AlphaEvolve、AgentForge 與 Agentic Verifier 則將程式執行與 automated evaluation 直接放入 AI 的生成—驗證閉環。

同時，反例同樣重要。Lean 官方在 2026 年 7 月的 4.32.1 與 4.32.2 point releases 分別修正 kernel soundness bugs，直接證明「formal checker」本身仍有 implementation-level trust boundary。VeriAct 的 2026 研究又顯示，大量 verifier-accepted formal specifications 可能實際上錯誤或不完整，說明 verifier pass 不等於 specification fidelity。

因此本文的核心命題是：

$$
\boxed{
\text{Computer verification does not create absolute truth;
it moves a claim into a different, inspectable, replayable, and often less-correlated error channel.}
}
$$

這種跨錯誤通道轉譯，正是多 AI 自主研究閉環能夠降低單純語言幻覺風險的主要機制之一。

**關鍵詞：** epistemic carrier；formal verification；execution feedback；reproducibility；trusted computing base；specification gap；semantic preservation；AI agents；cross-domain verification

---

## 1. 問題：為什麼「跑過」和「說過」不一樣？

令 Agent：

$$
A_i
$$

產生自然語言 claim：

$$
c.
$$

如果另一個 Agent 只閱讀 $c$ 再回答：

$$
\text{agree / disagree},
$$

兩者仍可能共享：
- 相同語言模型偏差；
- 相同 retrieval error；
- 相同錯誤 premise；
- 相同自然語言歧義。

若 Agent 反而生成一個 artifact：

$$
a
$$

並將其送入執行器：

$$
E(a,x;\eta)=o,
$$

其中：
- $x$ 是輸入；
- $\eta$ 是執行環境；
- $o$ 是實際 output；

則系統得到一項不同型態的 evidence。

一旦 $a$ 、 $x$ 與 $\eta$ 固定，執行 output 不再由「哪一個 Agent 比較有說服力」直接決定。

這是本文稱計算機為**相對客觀載體**的第一個意義。

---

## 2. 定義：Epistemic Carrier

### 定義 1：認知載體

令原始 claim space 為：

$$
\mathcal C.
$$

一個 epistemic carrier 定義為：

$$
\mathfrak C
=
(
\Sigma,
\tau,
\mathcal A,
\mathcal E,
V,
\mathcal T
),
$$

其中：
- $\Sigma$：carrier 可判定的 specification language；
- $\tau:\mathcal C\rightarrow\Sigma$：claim translation / formalization；
- $\mathcal A$：artifacts；
- $\mathcal E$：execution / evaluation semantics；
- $V$：verification operator；
- $\mathcal T$：trusted assumptions / trusted computing base。

carrier 不必是 theorem prover。

它可以是：
- unit test；
- compiler；
- interpreter；
- database query；
- numerical solver；
- simulation；
- formal checker；
- proof assistant；
- independent verifier；
- reproducible-build infrastructure；
- physical sensor interface。

---

## 3. 相對客觀性

### 定義 2：Source-Conditional Objectivity

令 artifact $a$ 已固定，來源 Agent identity 為：

$$
I\in\{A_1,\ldots,A_N\}.
$$

若 carrier output 滿足：

$$
P(
O
\mid
a,x,\eta,I=A_i
)
=
P(
O
\mid
a,x,\eta,I=A_j
)
$$

對所有 $i,j$ 成立，則稱該 carrier 對固定 artifact 具有 source-conditional objectivity。

在 deterministic setting：

$$
O
=
E(a,x;\eta),
$$

此條件退化為：

$$
O
\perp I
\mid
(a,x,\eta).
$$

這並不表示：

$$
O
=
\text{truth}.
$$

它只表示：

$$
\boxed{
\text{同一個 artifact 的 carrier result
不再由來源 Agent 的語言權威直接決定。}
}
$$

---

## 4. 認知轉譯階梯

本文區分至少七個層級。

### L0. Linguistic Claim

$$
c.
$$

只有自然語言敘述。

### L1. Executable Artifact

$$
c
\rightarrow
a.
$$

claim 被轉成程式、query 或其他 machine-readable artifact。

### L2. Executed Claim

$$
(a,x,\eta)
\rightarrow
o.
$$

artifact 被真正執行。

### L3. Tested Claim

存在 test suite：

$$
T=\{t_1,\ldots,t_m\}
$$

且：

$$
a\models T.
$$

### L4. Reproducible Claim

獨立或重建環境得到相同 artifact / output：

$$
R_1(a,x)
=
R_2(a,x).
$$

### L5. Formally Checked Claim

存在 formal specification：

$$
\sigma
$$

與 verifier：

$$
V(a,\sigma)=\mathrm{accept}.
$$

### L6. Independently Cross-Checked Claim

多個具有不同 implementation lineage 的 checker：

$$
V_1,\ldots,V_k
$$

共同接受。

### L7. World-Grounded Claim

formal specification 本身另有理由被認為忠實表達原始 world claim：

$$
\mathrm{Faithful}(c,\sigma).
$$

核心順序為：

$$
\boxed{
\text{linguistic}
\rightarrow
\text{executable}
\rightarrow
\text{reproducible}
\rightarrow
\text{formally checked}
\rightarrow
\text{world-grounded}.
}
$$

但這不是保證每一層必然比前一層更真。

它只是逐步增加不同種類的可檢查結構。

---

## 5. Trust Chain

令原始命題為：

$$
\phi.
$$

其 formal specification：

$$
\sigma=\tau(\phi).
$$

令 artifact 為：

$$
a.
$$

要把：

$$
V(a,\sigma)=\mathrm{accept}
$$

提升成：

$$
\phi
$$

的支持，需要多個 link。

### A1. Specification Fidelity

$$
\mathrm{Sem}(a)\models\sigma
\Rightarrow
\phi.
$$

或者更強：

$$
\phi
\iff
\sigma.
$$

### A2. Verifier Soundness

$$
V(a,\sigma)=\mathrm{accept}
\Rightarrow
\mathrm{Sem}_{\mathrm{src}}(a)\models\sigma.
$$

### A3. Compilation / Translation Preservation

若 artifact 經編譯：

$$
a
\rightarrow
a',
$$

則要求：

$$
\mathrm{Sem}_{\mathrm{src}}(a)
\sim
\mathrm{Sem}_{\mathrm{exec}}(a').
$$

### A4. Runtime Fidelity

實際執行必須符合被驗證的 machine semantics：

$$
\mathrm{Exec}(a',x;\eta)
\in
\mathrm{Sem}_{\mathrm{exec}}(a').
$$

### A5. Environment Assumptions

相關 dependency、configuration、numerical mode、input data、hardware 與 sandbox assumptions 沒有破壞前述語義。

因此完整鏈條為：

$$
\boxed{
\phi
\leftarrow
\sigma
\leftarrow
a
\leftarrow
\mathrm{compiler}
\leftarrow
\mathrm{runtime}
\leftarrow
\eta.
}
$$

---

## 6. 定理 1：Conditional Carrier Soundness

### 定理

若 A1–A5 全部成立，且：

$$
V(a,\sigma)=\mathrm{accept},
$$

則：

$$
\phi
$$

成立。

### 證明

由 A2：

$$
V(a,\sigma)=\mathrm{accept}
\Rightarrow
\mathrm{Sem}_{\mathrm{src}}(a)\models\sigma.
$$

由 A3 與 A4，source-level verified behavior 被保留到實際 execution semantics。

由 A5，實際環境滿足上述 preservation 所需 assumptions。

因此實際 artifact behavior 滿足：

$$
\sigma.
$$

由 A1：

$$
\sigma
\Rightarrow
\phi.
$$

故：

$$
\phi.
$$

證畢。

### 解讀

這個結果不是：

$$
\boxed{
\text{computer says yes}
\Rightarrow
\text{absolute truth}.
}
$$

而是：

$$
\boxed{
\text{computer says yes}
+
\text{trust-chain assumptions}
\Rightarrow
\text{conditional guarantee}.
}
$$

---

## 7. CompCert：Semantic Preservation 作為中間鏈條

CompCert 的核心意義不是「C 程式因此絕對正確」。

它證明的是 compiler translation 的一個特定關係。

若 source program：

$$
S
$$

滿足一組 acceptable behaviors：

$$
\Sigma,
$$

且 CompCert 將：

$$
S
\rightarrow C,
$$

則編譯後 code $C$ 保留被證明的 source-level property。

這對本文非常重要。

因為它顯示：

$$
\boxed{
\text{formal verification can close one trust boundary
without pretending to close all trust boundaries.}
}
$$

若 source-level specification 本身錯誤：

$$
\Sigma\neq\Sigma^\star,
$$

CompCert 的 semantic preservation 不會神奇地修正它。

---

## 8. Lean：Small Kernel 與 Independent Checkers

Lean 的 architecture 提供另一個典型例子。

高階 tactics、elaborator 與 automation 可以非常複雜，但最終新增到 environment 的 core definitions / proof terms 由較小的 trusted kernel 檢查。

因此：

$$
\text{tactic bug}
\nRightarrow
\text{proof soundness failure}
$$

只要錯誤結果無法通過 kernel。

更高風險情況下，Lean 官方文件進一步建議使用：
- sandboxed build；
- comparator；
- exported proof representation；
- official kernel；
- independently implemented external checker。

這是：

$$
\boxed{
\text{TCB minimization}
+
\text{implementation diversity}.
}
$$

但它仍不是 absolute truth。

Lean 官方明確列出 remaining assumptions，包括：
- Lean logic 本身的 soundness；
- comparator plumbing；
- sandbox security；
- 不存在同時影響所有 checkers 的共同 bug；
- theorem statement 沒有人為或表示層誤導。

---

## 9. Formal Checker 也不是絕對 Oracle

這一點在 2026 年變得尤其清楚。

Lean 4.32.1 的官方 release notes 修正一個 kernel soundness bug。

Lean 4.32.2 又修正另一個 kernel soundness bug；後者甚至可在某些情況下影響 comparator 路徑，而 independent checker `nanoda` 不受同一 kernel bug 影響。

因此：

$$
\boxed{
\text{formal verification}
\neq
\text{implementation infallibility}.
}
$$

更精確地：

$$
\boxed{
\text{formal guarantee}
=
\text{theorem}
+
\text{logic}
+
\text{proof object}
+
\text{checker implementation}
+
\text{trusted boundary}.
}
$$

這不削弱 formal methods 的價值。

恰好相反，它說明為什麼：
- small kernel；
- independent implementation；
- exported proof object；
- reproducible checking；

會實質增加 epistemic strength。

---

## 10. Specification Gap

Verifier 回答的問題通常是：

> artifact 是否滿足 specification？

而不是：

> specification 是否正確描述使用者真正想問的世界？

令 intended specification 為：

$$
\sigma^\star.
$$

實際提交給 verifier 的 specification 為：

$$
\tilde\sigma.
$$

即使：

$$
V(a,\tilde\sigma)=\mathrm{accept},
$$

也可能：

$$
\tilde\sigma\neq\sigma^\star.
$$

因此：

$$
\boxed{
\text{verification success}
\nRightarrow
\text{specification fidelity}.
}
$$

VeriAct 的 2026 結果正直接針對此問題：研究發現一大批 verifier-accepted specifications 實際上錯誤或不完整，可能 over-constrain 或 under-constrain inputs / outputs，而普通 verifier pass 無法發現。

所以本文將 specification fidelity 放在 trust chain 的第一層，而不是最後才補一句 limitation。

---

## 11. 命題 2：Reproducibility Orthogonality

### 命題

存在 artifact $a$ 與錯誤 specification relation，使得：

$$
R_1(a,x)=R_2(a,x)=\cdots=R_k(a,x)=o
$$

對所有重放環境成立，但：

$$
o
$$

仍不滿足 intended world-level claim。

### 證明

取一個 deterministic but wrong program 即可。

例如 intended function：

$$
f(x)=x^2.
$$

實作：

$$
\tilde f(x)
=
\begin{cases}
x^2,&x\geq0,\\
-x,&x<0.
\end{cases}
$$

對：

$$
x=-2,
$$

有：

$$
\tilde f(-2)=2,
$$

但：

$$
f(-2)=4.
$$

若所有重放環境 deterministic 地執行同一 $\tilde f$，則每次都得到：

$$
2.
$$

因此結果完全 reproducible，但仍然錯誤。

證畢。

所以：

$$
\boxed{
\text{reproducibility}
\perp
\text{semantic correctness}
}
$$

在邏輯上不能互相推出。

---

## 12. Reproducible Builds 的真正認知價值

Nix 的 reproducible-build model 特別清楚地顯示這個區分。

若獨立 infrastructure 從同一 source 與 dependencies 得到 bit-for-bit identical artifact，這會增加：

$$
\boxed{
\text{artifact provenance confidence}.
}
$$

它有助於檢查：
- build infrastructure 是否偷偷修改輸出；
- source 與 binary 是否一致；
- dependency closure 是否可重建。

但 Nix 自身文件也指出：
- repeated build 兩次並不能證明 reproducibility；
- timestamps 與其他 nondeterminism 仍可能洩漏進 build。

更重要的是，即使 binary 完全 reproducible，也不能推出：

$$
\boxed{
\text{the program implements the right idea}.
}
$$

因此 reproducibility 解的是：

$$
\text{provenance / reconstruction problem},
$$

不是完整的：

$$
\text{world-truth problem}.
$$

---

## 13. Execution Grounding

對 LLM Agent 而言，execution 的主要價值是把：

$$
\text{predicted behavior}
$$

轉成：

$$
\text{observed machine behavior}.
$$

AlphaEvolve 將候選程式交給 automated evaluator 實際 verify、run 與 score。

AgentForge 將 sandboxed execution 設為 code change 傳播前的 mandatory verification。

Agentic Verifier 則主動搜尋高區分度的 test inputs，以實際 execution 找出 candidate programs 的 behavioral discrepancy。

共同結構都是：

$$
\boxed{
\text{generate}
\rightarrow
\text{execute}
\rightarrow
\text{observe}
\rightarrow
\text{revise}.
}
$$

這正是 Series C 所說 autonomous research closure 的基礎回授。

---

## 14. 定理 3：Trust-Boundary Union Bound

令：

$$
F_1,\ldots,F_m
$$

為 trust chain 中不同 failure events。

假設：

$$
\{
V=\mathrm{accept}
\land
\neg\phi
\}
\subseteq
\bigcup_{j=1}^{m}F_j.
$$

亦即：若 carrier 錯誤接受 false claim，至少有一個 trust boundary 必須失效。

若：

$$
P(F_j)\leq q_j,
$$

則：

$$
P(
V=\mathrm{accept}
\land
\neg\phi
)
\leq
\sum_{j=1}^{m}q_j.
$$

### 證明

由 event inclusion：

$$
P(
V=\mathrm{accept}
\land
\neg\phi
)
\leq
P\left(
\bigcup_jF_j
\right).
$$

再由 union bound：

$$
P\left(
\bigcup_jF_j
\right)
\leq
\sum_jP(F_j)
\leq
\sum_jq_j.
$$

證畢。

### 意義

增加一個 formal verifier 並不是把：

$$
q=0.
$$

而是把原本模糊的：

$$
\text{LLM may be wrong}
$$

拆成一組更可定位的 failure surfaces：

$$
\boxed{
\text{specification}
+
\text{translation}
+
\text{checker}
+
\text{compiler}
+
\text{runtime}
+
\text{environment}.
}
$$

這就是「認知載體」的工程價值。

---

## 15. 異質錯誤通道

假設 false claim：

$$
\neg\phi
$$

被 $k$ 個 carriers 檢查。

第 $i$ 個 carrier false accept event：

$$
F_i.
$$

若：

$$
P(F_i\mid\neg\phi)\leq q_i
$$

且條件獨立，則：

$$
P(
F_1\cap\cdots\cap F_k
\mid
\neg\phi
)
\leq
\prod_{i=1}^{k}q_i.
$$

因此：

$$
\boxed{
\text{heterogeneous independent carriers}
}
$$

有機會產生乘法式錯誤抑制。

例如：
- LLM reasoning；
- Python execution；
- symbolic algebra；
- Lean checker；
- independent external checker；
- empirical dataset；

若 failure ancestry 足夠不同，聯合 evidence 比「再叫同一模型想一次」更強。

---

## 16. Common-Mode Failure

但 carriers 也可能共享共同失效。

令：

$$
C
$$

為 common-mode failure event，且：

$$
P(C\mid\neg\phi)=q_c.
$$

在：

$$
\neg C
$$

條件下，剩餘 carrier failures 獨立，機率為 $q_i$。

則：

$$
P(
\text{all accept}
\mid
\neg\phi
)
\leq
q_c
+
(1-q_c)
\prod_iq_i.
$$

當：

$$
q_c
$$

很大時，即使：

$$
k\rightarrow\infty,
$$

也有：

$$
P(
\text{all false accept}
\mid
\neg\phi
)
\gtrsim
q_c.
$$

因此：

$$
\boxed{
\text{carrier count}
\neq
\text{carrier independence}.
}
$$

典型 common-mode failure 包括：
- 所有 tools 依賴同一錯誤 dataset；
- 所有 verifiers 使用同一錯誤 specification；
- 多個 checkers 共享同一核心 bug；
- 所有 simulations 使用同一錯誤 physical model；
- 多個 Agents 直接複製同一上游 claim。

---

## 17. Relative Objectivity Index

本文不宣稱存在唯一客觀性 scalar，但可定義工程型指標。

令：
- $R$：replayability；
- $P$：provenance completeness；
- $I$：implementation independence；
- $S$：specification fidelity evidence；
- $T$：trusted-base compactness；
- $G$：external grounding。

定義：

$$
\mathrm{ROI}
=
w_RR
+
w_PP
+
w_II
+
w_SS
+
w_TT
+
w_GG.
$$

其中：

$$
w_j\geq0,
\qquad
\sum_jw_j=1.
$$

這不是 universal truth metric。

它只是一個工程排序：

> 哪一個 evidence carrier 更容易被重放、追溯、交叉檢查與獨立審計？

---

## 18. Epistemic Carrier Certificate

一項 machine-grounded claim 不應只保存：

$$
\text{output}.
$$

本文建議最小 certificate：

$$
\boxed{
\chi
=
(
c,
\sigma,
a,
x,
o,
\eta,
V,
h_a,
h_\eta,
p,
t
)
}
$$

其中：
- $c$：原始 claim；
- $\sigma$：formal / executable specification；
- $a$：artifact；
- $x$：input；
- $o$：output；
- $\eta$：environment；
- $V$：verifier；
- $h_a$：artifact hash；
- $h_\eta$：environment / dependency fingerprint；
- $p$：provenance；
- $t$：timestamp。

若有 independent checker：

$$
V_1,V_2,\ldots,V_k,
$$

也應一起寫入 certificate。

---

## 19. 與 Paper 03 的 Admissible Worlds 接合

Paper 03 定義：

$$
\mathcal A_t
$$

為目前仍被 evidence 允許的 world set。

一個 carrier certificate：

$$
\chi
$$

應被轉成 constraint：

$$
K_\chi
\subseteq
\Omega.
$$

若 $\chi$ 的 trust chain 尚未完整，系統不應直接使用：

$$
\mathcal A_{t+1}
=
\mathcal A_t\cap K_\chi
$$

做 hard contraction。

而可採 weighted / provisional constraint：

$$
K_\chi^{(\omega)}.
$$

只有當：
- provenance 足夠；
- verifier 被信任；
- specification fidelity 有外部支持；
- common-mode risk 可接受；

才升級為較強 world elimination。

因此：

$$
\boxed{
\text{machine result}
\rightarrow
\text{epistemic certificate}
\rightarrow
\text{admissible-world update}.
}
$$

---

## 20. 計算機為何特別適合作為 AI 的外部載體？

不是因為計算機無錯。

而是因為它具有幾項 LLM 自然語言輸出不總是具有的性質：

### 20.1 Determinate Interface

明確 input / output。

### 20.2 Replayability

相同 artifact 可以重跑。

### 20.3 Inspectable State

程式碼、logs、diff、test result 可以保存。

### 20.4 Executable Counterexample

一個 failing input 可以直接推翻某些 behavioral claim。

### 20.5 Independent Implementation

同一 proof object 可以交給不同 checker。

### 20.6 Formal Semantics

部分 domain 可以明確定義：

$$
\text{what counts as correct}.
$$

因此計算機是：

$$
\boxed{
\textbf{high verification-density epistemic substrate}.
}
$$

而不是：

$$
\boxed{
\textbf{complete epistemic substrate}.
}
$$

---

## 21. 失敗模式

### 21.1 Wrong Specification

$$
V(a,\tilde\sigma)=\mathrm{accept}
$$

但：

$$
\tilde\sigma\neq\sigma^\star.
$$

### 21.2 Test Overfitting

$$
a\models T
$$

但存在：

$$
x^\star\notin T
$$

使：

$$
a(x^\star)
$$

錯誤。

### 21.3 Reproducibly Wrong

每次 execution 都一致，但一致地錯。

### 21.4 Checker Bug

formal kernel 或 verifier implementation 存在 soundness bug。

### 21.5 Compiler / Runtime Mismatch

被證明的 source semantics 與實際執行 artifact 不一致。

### 21.6 Numerical / Environment Drift

dependency、floating semantics、random seed、hardware 或 configuration 改變結果。

### 21.7 Shared Grounding Failure

不同 carriers 最終都依賴同一錯誤 source 或 assumption。

### 21.8 Malicious Artifact

artifact 可能利用 verifier、build process 或 sandbox vulnerability。

---

## 22. 本篇可執行 Counterexample Checker

本文附帶一個純 Python structural checker。

它不冒充 Lean 或 formal proof assistant。

它檢查四件事。

### 22.1 Test Pass 不等於 Specification Correctness

intended function：

$$
f(x)=x^2.
$$

buggy implementation：

$$
\tilde f(x)
=
\begin{cases}
x^2,&x\geq0,\\
-x,&x<0.
\end{cases}
$$

若 test suite 只有：

$$
\{0,1,2,3\},
$$

則全部通過。

但：

$$
x=-2
$$

時：

$$
\tilde f(-2)=2\neq4.
$$

### 22.2 Reproducibly Wrong

對：

$$
x=-2,
$$

重跑多次永遠得到：

$$
2.
$$

因此：

$$
\text{reproducible}=1
$$

但：

$$
\text{correct}=0.
$$

### 22.3 Wrong Specification Can Be Verified

若錯誤 specification 只要求：

$$
\tilde f(x)\geq0,
$$

buggy implementation 在有限檢查 domain 上完全通過。

但它仍不滿足 intended specification：

$$
\tilde f(x)=x^2.
$$

### 22.4 Heterogeneous Carrier Bound

取：

$$
q_1=0.1,
\quad
q_2=0.05,
\quad
q_3=0.02.
$$

若獨立：

$$
q_{\mathrm{all}}
=
0.1\times0.05\times0.02
=
0.0001.
$$

若存在：

$$
q_c=0.1
$$

common-mode failure，則：

$$
q_{\mathrm{all}}
\leq
0.1
+
0.9\times0.0001
=
0.10009.
$$

直接顯示：

$$
\boxed{
\text{heterogeneity helps only when failure correlation is actually reduced}.
}
$$

---

## 23. 與自主研究閉環的關係

一個只有語言生成的系統：

$$
\text{hypothesis}
\rightarrow
\text{paper}.
$$

較弱。

加入 carrier：

$$
\text{hypothesis}
\rightarrow
\text{code}
\rightarrow
\text{execution}
\rightarrow
\text{data}
\rightarrow
\text{verification}
\rightarrow
\text{revision}
$$

後，系統開始把自己的 claim 投射到不同判定域。

因此 AI 自主研究真正重要的能力不只是：

$$
\boxed{
\text{generate new claims}.
}
$$

而是：

$$
\boxed{
\text{manufacture new evidence channels for its own claims}.
}
$$

這是從 LLM 到 autonomous research system 的關鍵轉變之一。

---

## 24. 結論

本文提出「計算機作為相對客觀認知載體」的條件理論。

「相對客觀」不表示：
- 計算機完備；
- formal methods 絕不出錯；
- verifier pass 等於 world truth；
- reproducibility 等於 correctness。

它表示：

$$
\boxed{
O
\perp
I_{\mathrm{source}}
\mid
(a,x,\eta)
}
$$

以及 machine carrier 可以提供：
- 固定接口；
- 重放；
- provenance；
- executable counterexample；
- independent checker；
- formal semantics。

完整可信度仍依賴：

$$
\boxed{
\text{specification fidelity}
+
\text{verifier soundness}
+
\text{semantic preservation}
+
\text{runtime fidelity}
+
\text{environment assumptions}.
}
$$

因此本文最重要的結論不是：

$$
\text{Computer}
=
\text{Truth}.
$$

而是：

$$
\boxed{
\textbf{Computer}
=
\textbf{a relatively objective, conditionally trusted,
high-verification-density epistemic carrier}.
}
$$

對 AI 系統而言，真正重要的認知躍遷是：

$$
\boxed{
\text{claim}
\rightarrow
\text{artifact}
\rightarrow
\text{execution}
\rightarrow
\text{certificate}
\rightarrow
\text{cross-carrier comparison}.
}
$$

下一篇將正式把這些元件組成一個最小自主研究閉環：

**Series C / Paper 05 — Minimal Closure Conditions for Autonomous Research.**

---

## 參考文獻

1. Lean FRO. *The Lean Language Reference: Elaboration and Compilation — The Kernel*. Current documentation, accessed 2026-08-14.
2. Lean FRO. *Validating a Lean Proof*. Current documentation, accessed 2026-08-14.
3. Lean FRO. *Lean 4.32.1 Release Notes*. 2026-07-22.
4. Lean FRO. *Lean 4.32.2 Release Notes*. 2026-07-28.
5. Leroy, X. et al. *The CompCert C Verified Compiler* / CompCert project documentation and semantic-preservation proofs. Current CompCert 3.17 documentation, 2026.
6. NixOS. *Reproducible Builds*. Current project documentation.
7. Google DeepMind. *AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms*. 2025.
8. Misu, M. R. H., Ma, I., & Lopes, C. V. *VeriAct: Beyond Verifiability — Agentic Synthesis of Correct and Complete Formal Specifications*. arXiv:2604.00280, 2026.
9. Kumar, R. et al. *AgentForge: Execution-Grounded Multi-Agent LLM Framework for Autonomous Software Engineering*. arXiv:2604.13120, 2026.
10. Ma, Z. et al. *Scaling Agentic Verifier for Competitive Coding*. arXiv:2602.04254, 2026.
11. *OpenProver: Agentic and Interactive Theorem Proving with Lean 4*. arXiv:2607.09217, 2026.

## 狀態標記

- **Definitions:** Epistemic Carrier、Source-Conditional Objectivity、Trust Chain、Relative Objectivity Index、Carrier Certificate。
- **Proved:** Conditional Carrier Soundness、Reproducibility Orthogonality、Trust-Boundary Union Bound、Heterogeneous Carrier Suppression under independence。
- **External technical grounding:** Lean kernel / external checker model、CompCert semantic preservation、Nix reproducibility、AlphaEvolve execution evaluation、VeriAct specification-gap result、AgentForge / Agentic Verifier execution grounding。
- **Counterexamples:** wrong specification、test overfitting、reproducibly wrong artifact、formal-checker implementation bug、common-mode failure。
- **Not claimed:** computer completeness、absolute machine objectivity、formal verification infallibility、verifier acceptance implies world truth without specification fidelity。