# 可觀測性、可驗證性與反證框架
## 廣義相位交流中的觀測等價、性質可辨識、形式證書、模型落差與可證偽科學

**英文題名：** Observability, Verifiability, and Falsification: Observational Equivalence, Property Identifiability, Formal Certificates, Model Gaps, and Falsifiable Science in Generalized Phase Communication  
**系列：** 廣義相位交流與載體安全（Generalized Phase Communication and Carrier Safety, GPC-CS）  
**Paper：** 10  
**作者：** Neo.K（許筌崴）  
**機構：** EveMissLab／一言諾科技有限公司  
**理論協作：** Aletheia（GPT-5.6 Sol）  
**版本：** v1.0  
**日期：** 2026-08-14  
**狀態：** Public Theoretical Paper / Core-Series Closure / Non-operational Safety Theory

---

## 摘要

Paper 00–09 已建立廣義相位交流與載體安全的一套形式語言：載體狀態 $\mathcal X$ 、安全域 $\mathcal S$ 、跨載體轉導 $T$ 、重建 $D$ 、容量域 $\mathfrak C$ 、狀態算子 $O$ 、雙向耦合 $\Gamma_{AB}$ 、歷史與恢復、身份相關連續向量、共模失效，以及全域網路級聯 $\Gamma_G$。然而，這些對象大多被寫在「真實內部狀態」層。本文處理整個核心系列最後一個問題：

> **外部觀察者究竟能不能從有限輸出、有限實驗、形式模型與部署紀錄，判斷前九篇定義的內部性質真的成立？**

本文首先定義觀測映射：

$$
\boxed{
H:
\mathcal X
\rightarrow
\mathcal Y,
}
$$

以及觀測等價：

$$
x
\sim_H
x'
\iff
H(x)=H(x').
$$

若安全性由指示函數：

$$
\chi_{\mathcal S}(x)
$$

表示，本文證明一個基本**性質可觀測判準**：存在只依賴觀測值的分類器：

$$
g:
H(\mathcal X)
\rightarrow
\{0,1\}
$$

使：

$$
\boxed{
\chi_{\mathcal S}
=
g\circ H
}
$$

當且僅當 $\chi_{\mathcal S}$ 在 $H$ 的每一個 fiber 上為常數。等價地，不存在同一觀測值同時對應安全與不安全狀態。本文定義安全歧義輸出集：

$$
\boxed{
\mathcal A_H^{\mathcal S}
=
\left\{
y:
H^{-1}(y)\cap\mathcal S\neq\varnothing,
\;
H^{-1}(y)\cap(\mathcal X\setminus\mathcal S)\neq\varnothing
\right\}.
}
$$

若：

$$
\mathcal A_H^{\mathcal S}
\neq\varnothing,
$$

則任何只看當前 $y$ 的 deterministic safety classifier 都不可能對所有狀態完全正確。

第二，本文把靜態觀測提升成時間窗觀測。對確定動力學：

$$
x_{t+1}=F(x_t),
$$

定義：

$$
\boxed{
\mathcal O_T(x_0)
=
\left(
H(x_0),
H(F(x_0)),
\ldots,
H(F^T(x_0))
\right).
}
$$

兩個初始狀態若具有相同 $\mathcal O_T$，則在 $T$ 步輸出窗內不可區分。經典 Kalman 線性可觀測性正是此概念在：

$$
x_{t+1}=Ax_t,
\qquad
y_t=Cx_t
$$

下的有限維版本：觀測矩陣：

$$
\boxed{
\mathscr O_n
=
\begin{pmatrix}
C\\
CA\\
\vdots\\
CA^{n-1}
\end{pmatrix}
}
$$

滿列秩 $n$ 當且僅當初始狀態可由長度 $n$ 的無雜訊輸出序列唯一辨識。Hermann–Krener 則將 observability 推廣到非線性系統的微分幾何設定。Takens delay embedding 提供另一條成熟鄰近路線：在特定 generic dynamical assumptions 下，單一觀測的 delay coordinates 可以重建 attractor 的嵌入結構。但本文明確不把 Takens theorem 誤寫成「任意黑箱只靠時間序列就能完整知道內部狀態」。

第三，本文區分**狀態可觀測性**與**性質可觀測性**。安全判定未必需要重建完整 $x$ ；只要所有 observationally equivalent states 對安全規格具有同一真值即可。這使驗證問題可以直接在 quotient：

$$
\mathcal X/\sim_H
$$

上研究，而不必把完整心智、模型或網路內部狀態全部反演。

第四，本文建立**有限測試不推出全域安全**的最小 no-go theorem。若測試只覆蓋有限集合：

$$
D
=
\{x_1,\ldots,x_n\}
\subsetneq
\mathcal X,
$$

且規格類沒有額外結構限制，則對任意未測點：

$$
x^\star\in\mathcal X\setminus D,
$$

總可構造兩個候選 safety predicates $s_1,s_2$，它們在 $D$ 上完全相同，卻在 $x^\star$ 上相反。因此任何只依賴有限測試結果、且沒有額外模型假設的程序，都不能由「全部測試通過」推出對所有 $\mathcal X$ 的 universal safety。這不是反對測試，而是把 testing、probabilistic certification 與 formal proof 的證明強度分開。

第五，本文證明 universal safety 的**反例不對稱性**。對命題：

$$
\forall x\in K,\quad P(x),
$$

只要找到一個：

$$
x^\star\in K
$$

使：

$$
\neg P(x^\star),
$$

即可否證全稱命題；但任意有限個滿足 $P$ 的樣本，在 $K$ 無限或尚未完全枚舉時，一般不能證明全稱命題。Temporal-logic falsification、S-TaLiRo、robustness-guided search 等既有工作正是在此邏輯不對稱下，將「找一個違反軌跡」與「證明沒有違反軌跡」明確區分。

第六，本文定義三值 verifier：

$$
\boxed{
V(M,\varphi)
\in
\{
\mathrm{PROVED},
\mathrm{REFUTED},
\mathrm{UNKNOWN}
\}.
}
$$

其中 $M$ 是明確模型， $\varphi$ 是明確規格。Soundness 要求：

$$
V(M,\varphi)=\mathrm{PROVED}
\Rightarrow
M\models\varphi,
$$

而：

$$
V(M,\varphi)=\mathrm{REFUTED}
$$

必須伴隨可驗證 counterexample 或其他有效反證。 $\mathrm{UNKNOWN}$ 是合法結果，不能被靜默改寫成「大概安全」。本文以 barrier certificates、reachability、SMT / neural-network verification 作為不同形式證書的成熟背景。

第七，本文正式處理**模型—部署落差**。設 verified model 為 $\widehat M$，實際系統為 $M^\star$。即使：

$$
\widehat M\models\varphi,
$$

也不自動推出：

$$
M^\star\models\varphi.
$$

2025 年對 deployed neural-network verification 的研究已明確區分 theoretical soundness 與 practical soundness，指出浮點、隨機部署環境與執行細節可以破壞「理論 verifier 的 soundness」到實際 runtime guarantee 的直接推論。本文因而引入 model discrepancy：

$$
d_{\mathrm{mdl}}
(
x_t^\star,
\hat x_t
)
\le
\varepsilon_t.
$$

若 safety margin function $h$ 為 $L_h$ -Lipschitz，且 model trajectory 已證明：

$$
h(\hat x_t)\ge m_t>0,
$$

只要：

$$
\boxed{
L_h\varepsilon_t<m_t,
}
$$

便可推出：

$$
h(x_t^\star)>0.
$$

這形成一個最小的**robust verification transfer theorem**：形式證明要從模型移到部署系統，必須有足夠大的規格 margin 吸收 model discrepancy。

第八，本文建立證據強度階梯：形式證明／證書、有限域完整枚舉、機率性保證、反例／falsification、系統化測試、案例觀察，分別支持不同強度的命題。對 iid Bernoulli failure trials，若 $n$ 次測試觀察到零失敗，則 one-sided exact confidence calculation 給出：

$$
\boxed{
p
\le
1-\delta^{1/n}
}
$$

作為 confidence $1-\delta$ 的 zero-failure 上界形式。這再次顯示「零失敗測試」可以提供統計上界，但不能證明 $p=0$。2025 年的 probabilistic / probably-approximately-global verification 工作正代表形式保證與抽樣保證之間仍在持續發展的中間層。

第九，本文把整個 GPC-CS 改寫成一個**可反證研究計畫**。每個理論層都必須指定：

$$
\boxed{
(\text{claim},
\text{scope},
\text{observation map},
\text{assumptions},
\text{certificate or test},
\text{countercondition}).
}
$$

沒有 observation map 的內部變量只是 latent theoretical object；沒有 countercondition 的陳述不是完整可證偽命題；沒有 scope 的驗證結果不能合法被擴張成全域安全。

本文不提供任何高風險實驗刺激、攻擊測試、身份操控或級聯誘發方法。它只建立防禦性、抽象化的驗證語言。Paper 10 的最終原則是：

$$
\boxed{
\text{A formal safety theory becomes science only when its claims are connected to observable evidence and possible refutation.}
}
$$

**關鍵詞：** 可觀測性、驗證、反證、觀測等價、Kalman observability、nonlinear observability、Takens embedding、barrier certificate、formal verification、falsification、model discrepancy、practical soundness

---

# 0. 文獻定位與非目標

Observability 是控制理論的經典核心概念。Kalman 1960 年的工作將 controllability 與 observability 系統化帶入線性 state-space theory；Hermann–Krener 1977 年則以 differential-geometric tools 發展 nonlinear controllability and observability。

Takens 1981 年的 delay embedding theorem 則提供另一種非常不同的可觀測性直覺：在特定 generic assumptions 下，系統 attractor 的狀態幾何可由單一 observable 的延遲座標重建。這不等同於控制理論 observability，也不等同於任意黑箱 state recovery。

形式安全驗證方面，Prajna–Jadbabaie–Pappas 的 barrier-certificate framework、後續 temporal verification、reachability，以及 Reluplex 等 neural-network verifier 都展示「證明一個 property」與「只測試很多案例」具有不同邏輯強度。

Temporal-logic robustness 與 falsification 文獻則提供 counterexample-driven verification 的成熟方法：Fainekos–Pappas、Donzé–Maler 與 S-TaLiRo 等工作把 specification satisfaction、robustness margin 與 falsification 搜尋連在一起。

本文不重新發明 observability、model checking、barrier certificates、SMT verification、temporal logic 或 statistical certification。

本文的工作是將它們接到前九篇 GPC-CS 所定義的 latent carrier-state theory。

---

# 1. 真實狀態與可見輸出

設真實載體狀態：

$$
x
\in
\mathcal X.
$$

外部觀察：

$$
\boxed{
y
=
H(x),
}
$$

其中：

$$
H:
\mathcal X
\rightarrow
\mathcal Y
$$

為 observation map。

若有 measurement noise：

$$
y
=
H(x)+\nu
$$

或更一般：

$$
y
\sim
P(\cdot\mid x).
$$

本文先從 deterministic $H$ 開始。

---

# 2. Observational Equivalence

定義：

$$
\boxed{
x
\sim_H
x'
\iff
H(x)=H(x').
}
$$

這是一個等價關係。

因此狀態空間可被 quotient：

$$
\boxed{
\mathcal X/\sim_H.
}
$$

外部觀察者若只看到當前 $y$，最多能區分不同 observation fibers，而不能區分同一 fiber 內部的 states。

---

# 3. Observation Fiber

對：

$$
y\in H(\mathcal X),
$$

定義 fiber：

$$
\boxed{
\mathcal F_H(y)
=
H^{-1}(y).
}
$$

若：

$$
|\mathcal F_H(y)|>1,
$$

則該輸出對應多個內部狀態。

這本身不一定是問題。

真正問題是：

> 這些不可區分狀態在我們關心的 property 上是否仍然相同？

---

# 4. 性質可觀測性

令：

$$
P:
\mathcal X
\rightarrow
\mathcal Z_P
$$

為某個 property map。

例如 safety：

$$
P(x)
=
\chi_{\mathcal S}(x)
\in
\{0,1\}.
$$

定義：

> $P$ 對 observation $H$ 可完全辨識，若存在
> $$
> g:
> H(\mathcal X)
> \rightarrow
> \mathcal Z_P
> $$
> 使
> $$
> P=g\circ H.
> $$

---

# 5. Property Observability Fiber Theorem

## 定理 5.1

存在：

$$
g:
H(\mathcal X)
\rightarrow
\mathcal Z_P
$$

使：

$$
\boxed{
P
=
g\circ H
}
$$

當且僅當 $P$ 在 $H$ 的每個 fiber 上為常數：

$$
\boxed{
H(x_1)=H(x_2)
\Rightarrow
P(x_1)=P(x_2).
}
$$

### 證明

若：

$$
P=g\circ H,
$$

則：

$$
H(x_1)=H(x_2)
$$

立即給出：

$$
P(x_1)=g(H(x_1))=g(H(x_2))=P(x_2).
$$

反之，若 $P$ 在每個 fiber 上為常數，對：

$$
y\in H(\mathcal X)
$$

任選：

$$
x\in H^{-1}(y)
$$

定義：

$$
g(y)=P(x).
$$

由 fiber 常數性， $g$ 良定義。

證畢。

---

# 6. Safety Observability

取：

$$
P
=
\chi_{\mathcal S}.
$$

則存在純 observation-based exact safety classifier：

$$
g(y)
$$

的充要條件是：

$$
\boxed{
H(x_1)=H(x_2)
\Rightarrow
\chi_{\mathcal S}(x_1)
=
\chi_{\mathcal S}(x_2).
}
$$

這是一個比「完整 state observable」更弱、也更實用的條件。

---

# 7. 安全歧義輸出

定義：

$$
\boxed{
\mathcal A_H^{\mathcal S}
=
\left\{
y:
H^{-1}(y)\cap\mathcal S\neq\varnothing,
\;
H^{-1}(y)\cap
(
\mathcal X\setminus\mathcal S
)
\neq\varnothing
\right\}.
}
$$

若：

$$
\mathcal A_H^{\mathcal S}
\neq\varnothing,
$$

則存在外部看起來完全相同、但 safety truth 不同的 states。

---

# 8. Observation-Only Safety Impossibility

## 推論 8.1

若：

$$
\mathcal A_H^{\mathcal S}
\neq\varnothing,
$$

則不存在：

$$
g:
H(\mathcal X)
\rightarrow
\{0,1\}
$$

能對所有：

$$
x\in\mathcal X
$$

完全正確判斷：

$$
x\in\mathcal S.
$$

此結果直接由定理 5.1 得到。

---

# 9. 看起來正常不等於內部安全

因此：

$$
\boxed{
\text{normal-looking output}
\not\Rightarrow
\text{safe hidden state}
}
$$

只要安全歧義 fiber 存在。

這並不是說外部行為觀測無用。

而是說：

> 任何 output-only safety claim 都需要先證明或假設 property observability。

---

# 10. 完整 State Observability 與 Property Observability

完整 state observability 要求：

$$
H(x_1)=H(x_2)
\Rightarrow
x_1=x_2
$$

或在時間展開後能唯一辨識 state。

Property observability 只要求：

$$
H(x_1)=H(x_2)
\Rightarrow
P(x_1)=P(x_2).
$$

因此：

$$
\boxed{
\text{state observability}
\Rightarrow
\text{property observability},
}
$$

但反向一般不成立。

這是 GPC-CS 驗證可大幅簡化的重要入口。

---

# 11. 時間窗觀測

設 deterministic dynamics：

$$
x_{t+1}
=
F(x_t).
$$

定義：

$$
\boxed{
\mathcal O_T(x_0)
=
\left(
H(x_0),
H(F(x_0)),
\ldots,
H(F^T(x_0))
\right).
}
$$

若：

$$
\mathcal O_T(x)
=
\mathcal O_T(x'),
$$

則兩個初始狀態在長度 $T$ 的 observation window 中不可區分。

---

# 12. 有限時間 Observational Equivalence

定義：

$$
x
\sim_{H,T}
x'
$$

當且僅當：

$$
\mathcal O_T(x)
=
\mathcal O_T(x').
$$

隨：

$$
T
$$

增加，等價類通常可以變細。

但不保證有限 $T$ 必然足以完全識別所有系統。

---

# 13. Linear Observability

對離散線性系統：

$$
x_{t+1}
=
Ax_t,
$$

$$
y_t
=
Cx_t,
$$

有：

$$
y_t
=
CA^tx_0.
$$

堆疊前 $n$ 個輸出：

$$
\begin{pmatrix}
y_0\\
y_1\\
\vdots\\
y_{n-1}
\end{pmatrix}
=
\boxed{
\mathscr O_n
}
x_0,
$$

其中：

$$
\boxed{
\mathscr O_n
=
\begin{pmatrix}
C\\
CA\\
\vdots\\
CA^{n-1}
\end{pmatrix}.
}
$$

---

# 14. Kalman Rank Criterion

## 定理 14.1

對 $n$ 維離散 LTI 系統，初始狀態可由長度 $n$ 的無雜訊輸出序列唯一辨識，當且僅當：

$$
\boxed{
\operatorname{rank}
(
\mathscr O_n
)
=
n.
}
$$

### 證明

若：

$$
\operatorname{rank}
(
\mathscr O_n
)
=
n,
$$

則線性映射：

$$
x_0
\mapsto
\mathscr O_nx_0
$$

單射，故輸出唯一決定 $x_0$。

若 rank 小於 $n$，存在非零：

$$
v
\in
\ker\mathscr O_n.
$$

則：

$$
x_0
$$

與：

$$
x_0+v
$$

產生相同前 $n$ 步輸出。

故不可唯一辨識。

證畢。

---

# 15. Nonlinear Observability

對：

$$
\dot x=f(x),
$$

$$
y=h(x),
$$

Hermann–Krener 1977 的 nonlinear observability theory 使用由：

$$
h,
L_fh,
L_f^2h,
\ldots
$$

生成的 observation codistribution，以及 rank conditions 判定局部弱可觀測性。

本文不重新推導完整 differential-geometric theorem。

其在 GPC-CS 的意義是：

> 當 carrier dynamics 非線性時，是否能由輸出識別內部狀態本身就是一個結構性數學問題，不是「多記錄一點 log」就自然解決。

---

# 16. Delay Coordinates 與 Takens Boundary

Takens 類 delay embedding 使用：

$$
\boxed{
\mathcal D_m(x)
=
\left(
h(x),
h(F(x)),
\ldots,
h(F^{m-1}(x))
\right).
}
$$

在適當 smoothness、genericity、compact-manifold / attractor assumptions 下，delay map 可以形成 embedding。

但本文明確不做以下錯誤推論：

$$
\boxed{
\text{Takens theorem}
\not\Rightarrow
\text{arbitrary hidden carrier state is reconstructible}.
}
$$

因為 theorem scope 與 generic assumptions 必須成立。

---

# 17. 網路 Observation Map

對 Paper 09 的全域狀態：

$$
\mathbf X
=
(x_1,\ldots,x_N),
$$

定義：

$$
\boxed{
H_G:
\mathcal X_G
\rightarrow
\mathcal Y_G.
}
$$

它可以只觀察：

- 部分節點輸出；
- aggregate statistics；
- logs；
- external behavior；
- relation measurements。

全域 safety property：

$$
P_G(\mathbf X)
=
\chi_{\mathcal S_G^\star}(\mathbf X).
$$

---

# 18. Global Safety Observability

由定理 5.1，存在只依賴全域觀測：

$$
g_G(H_G(\mathbf X))
$$

的 exact global-safety classifier，當且僅當：

$$
\boxed{
H_G(\mathbf X)
=
H_G(\widetilde{\mathbf X})
\Rightarrow
P_G(\mathbf X)
=
P_G(\widetilde{\mathbf X}).
}
$$

因此：

> 局部 telemetry 很完整，仍不代表全域 relation safety 可觀測。

---

# 19. Relation-Blind Observation

如果：

$$
H_G
$$

只輸出每個節點的本地健康值，

卻不觀察：

$$
\mathcal C_G
$$

所需的相位、延遲、同步、共享依賴或 cross-gain，

則可能存在：

$$
\mathbf X,
\widetilde{\mathbf X}
$$

本地輸出相同，

但：

$$
\mathbf X\in\mathcal S_G^\star,
$$

$$
\widetilde{\mathbf X}\notin\mathcal S_G^\star.
$$

此時 global safety 不可由該 observation map 完全判定。

---

# 20. Verification Object 必須完整寫出

本文定義一個 verification claim：

$$
\boxed{
\mathfrak V
=
(
M,
\varphi,
K,
H,
A
).
}
$$

其中：

- $M$：被驗證模型；
- $\varphi$：規格；
- $K$：驗證域；
- $H$：觀測／可測映射；
- $A$：模型假設集合。

因此不能只說：

> 「系統已證明安全」。

更精確的是：

> 在假設 $A$ 下，模型 $M$ 對 domain $K$ 滿足 specification $\varphi$。

---

# 21. Specification Before Verification

形式驗證永遠驗的是：

$$
\varphi.
$$

如果：

$$
\varphi
$$

沒有包含某個真正重要的安全條件，

即使：

$$
M\models\varphi,
$$

也不能推出：

> 所有未寫進 $\varphi$ 的安全要求都成立。

因此：

$$
\boxed{
\text{verification quality}
\le
\text{specification quality}.
}
$$

這不是數值不等式，而是邏輯依賴原則。

---

# 22. 三值 Verifier

定義：

$$
\boxed{
V(M,\varphi)
\in
\{
\mathrm{PROVED},
\mathrm{REFUTED},
\mathrm{UNKNOWN}
\}.
}
$$

PROVED 表示 verifier 建立有效證書或完整推導。

REFUTED 表示找到有效 counterexample / proof of violation。

UNKNOWN 表示方法未能決定。

---

# 23. Soundness

若 verifier 對 PROVED sound：

$$
\boxed{
V(M,\varphi)
=
\mathrm{PROVED}
\Rightarrow
M\models\varphi.
}
$$

若對 REFUTED sound：

$$
\boxed{
V(M,\varphi)
=
\mathrm{REFUTED}
\Rightarrow
M\not\models\varphi.
}
$$

在 counterexample-based verifier 中，REFUTED 通常應附：

$$
c
$$

使：

$$
c\models\neg\varphi.
$$

---

# 24. UNKNOWN 是合法答案

如果 solver timeout、

over-approximation 太寬、

state space 太大、

specification 太複雜，

得到：

$$
\mathrm{UNKNOWN}
$$

不等於：

$$
\mathrm{SAFE}.
$$

也不等於：

$$
\mathrm{UNSAFE}.
$$

因此：

$$
\boxed{
\text{inconclusive}
\neq
\text{negative result}
\neq
\text{positive result}.
}
$$

---

# 25. Barrier Certificate 的位置

Prajna–Jadbabaie–Pappas 類 barrier certificate 研究：

若找到一個函數：

$$
B(x)
$$

滿足適當：

- initial-set；
- unsafe-set；
- dynamics；

條件，

就可以證明某些軌跡不會從 initial region 到達 unsafe region。

在 GPC-CS 中，barrier certificate 是 Paper 01 safe-domain verification 的**證書工具之一**。

它不是安全規格本身。

---

# 26. Verification Certificate 不是 Reality Certificate

如果 verifier 證明：

$$
\widehat M\models\varphi,
$$

它首先只是一個：

$$
\boxed{
\text{model-level theorem}.
}
$$

要移到 deployed system：

$$
M^\star,
$$

還需要：

$$
\boxed{
\widehat M
\approx
M^\star
}
$$

的 conformance / model-error 證據。

---

# 27. Model Discrepancy

設 nominal model trajectory：

$$
\hat x_t,
$$

actual trajectory：

$$
x_t^\star.
$$

定義：

$$
\boxed{
\varepsilon_t
=
d
(
x_t^\star,
\hat x_t
).
}
$$

若：

$$
\varepsilon_t
$$

沒有已知上界，

則 model proof 一般不能直接變成 runtime state proof。

---

# 28. Safety Margin Function

設：

$$
h:
\mathcal X
\rightarrow
\mathbb R
$$

定義：

$$
\mathcal S
=
\{
x:
h(x)\ge0
\}.
$$

假設：

$$
h
$$

為 $L_h$ -Lipschitz：

$$
|
h(x)-h(y)
|
\le
L_hd(x,y).
$$

若 nominal model 證明：

$$
h(\hat x_t)
\ge
m_t>0,
$$

則 model trajectory 距離安全邊界至少具有 certificate margin。

---

# 29. Robust Verification Transfer Theorem

## 定理 29.1

若：

$$
h(\hat x_t)
\ge
m_t>0,
$$

$$
d(x_t^\star,\hat x_t)
\le
\varepsilon_t,
$$

且：

$$
\boxed{
L_h\varepsilon_t
<
m_t,
}
$$

則：

$$
\boxed{
h(x_t^\star)>0.
}
$$

因此：

$$
x_t^\star
\in
\operatorname{Int}(\mathcal S).
$$

### 證明

由 Lipschitz：

$$
h(x_t^\star)
\ge
h(\hat x_t)
-
L_h
d(x_t^\star,\hat x_t).
$$

故：

$$
h(x_t^\star)
\ge
m_t
-
L_h\varepsilon_t
>
0.
$$

證畢。

---

# 30. Verification Margin 會被 Model Gap 消耗

定理 29.1 可以改寫為：

$$
\boxed{
m_t^{\mathrm{runtime}}
\ge
m_t^{\mathrm{model}}
-
L_h\varepsilon_t.
}
$$

因此模型證書離 boundary 越遠，

越有空間吸收：

- discretization；
- floating-point；
- calibration；
- deployment；
- unmodeled-dynamics error。

---

# 31. Practical Soundness

2025 年 deployed neural-network verification 研究明確指出：

> theoretical soundness under an abstract/full-precision model does not automatically imply practical soundness under actual floating-point and potentially stochastic execution environments.

GPC-CS 對此採用一般原則：

$$
\boxed{
\text{proof soundness}
+
\text{model conformance}
=
\text{runtime guarantee bridge}.
}
$$

沒有第二項，

不能只靠第一項。

---

# 32. Temporal Logic Robustness

對時間訊號：

$$
y(t),
$$

以及 temporal-logic specification：

$$
\varphi,
$$

Fainekos–Pappas、Donzé–Maler 類 robustness semantics 不只給出：

$$
y\models\varphi
$$

或否，

而定義一個 robustness value：

$$
\rho_\varphi(y).
$$

正 robustness 可以被理解為距離 violation boundary 的某種規格 margin。

---

# 33. Robust Satisfaction Transfer

如果某 specification robustness metric 對 signal distance 具有相應 Lipschitz / robustness guarantee：

$$
|
\rho_\varphi(y)
-
\rho_\varphi(\tilde y)
|
\le
L_\rho
d_Y(y,\tilde y),
$$

且：

$$
\rho_\varphi(\hat y)
>
L_\rho\varepsilon,
$$

則任何：

$$
d_Y(y^\star,\hat y)\le\varepsilon
$$

的 actual signal 仍滿足：

$$
\rho_\varphi(y^\star)>0.
$$

這與定理 29.1 同一結構。

---

# 34. 有限測試集

令測試集：

$$
D
=
\{
x_1,\ldots,x_n
\}
\subset
K.
$$

測試結果：

$$
P(x_i)=1
$$

對所有：

$$
i.
$$

如果：

$$
K
$$

尚未完全枚舉，

是否能推出：

$$
\forall x\in K,
\quad
P(x)=1?
$$

一般不能。

---

# 35. Finite-Test Non-Universality Theorem

## 定理 35.1

設：

$$
D
\subsetneq
K
$$

為有限測試集合，

且候選 property class 允許所有：

$$
K\rightarrow\{0,1\}
$$

函數。

則對任意未測：

$$
x^\star
\in
K\setminus D,
$$

存在兩個 predicates：

$$
P_1,
P_2
$$

使：

$$
P_1(x)
=
P_2(x)
=
1
$$

對所有：

$$
x\in D,
$$

但：

$$
P_1(x^\star)=1,
$$

$$
P_2(x^\star)=0.
$$

### 證明

令：

$$
P_1(x)=1
$$

對所有：

$$
x\in K.
$$

令：

$$
P_2(x)
=
\begin{cases}
0,
&
x=x^\star,\\
1,
&
\text{otherwise}.
\end{cases}
$$

則兩者在所有測試點完全一致，但全域命題不同。

證畢。

---

# 36. 定理 35.1 的正確解讀

這不是說：

> testing 沒有價值。

它說：

> testing 之所以能 generalize，必須依賴額外結構。

例如：

- smoothness；
- Lipschitz bound；
- coverage；
- finite-state exhaustiveness；
- probabilistic sampling assumption；
- symbolic model；
- inductive invariant。

沒有這些，

「沒測到失敗」不能被提升成 universal theorem。

---

# 37. Counterexample Asymmetry

考慮 universal claim：

$$
\boxed{
\forall x\in K,
\quad
P(x).
}
$$

只要存在：

$$
x^\star\in K
$$

使：

$$
\neg P(x^\star),
$$

全稱命題立即為假。

---

# 38. Falsification Asymmetry Theorem

## 定理 38.1

一個合法 counterexample：

$$
x^\star\in K
$$

且：

$$
P(x^\star)=0
$$

足以 refute：

$$
\forall x\in K,\;P(x).
$$

但當 $K$ 未被完全枚舉且沒有額外結構定理時，任意有限數量：

$$
P(x_i)=1
$$

不構成該全稱命題的邏輯證明。

### 證明

第一部分由 universal quantifier 的語義直接成立。

第二部分由定理 35.1。

證畢。

---

# 39. Falsification 不是 Verification 的弱版本

Falsification 的目標是：

$$
\exists x\in K:
\neg P(x).
$$

Verification 的 universal safety 目標是：

$$
\forall x\in K:
P(x).
$$

兩者量詞方向相反。

因此：

$$
\boxed{
\text{failure to falsify}
\neq
\text{verification}.
}
$$

---

# 40. Temporal-Logic Falsification

S-TaLiRo 與 robustness-guided falsification 等方法正是搜尋：

$$
\rho_\varphi(y)<0
$$

的輸入／軌跡。

若找到有效軌跡，

即可反證：

$$
\varphi
$$

在指定模型與 domain 下的 universal satisfaction。

若沒有找到，

只表示：

> 在該搜尋預算與方法下未找到反例。

不自動變成：

$$
M\models\varphi.
$$


---

# 41. Zero-Failure Testing 仍只能給機率上界

假設每次測試獨立同分布，

失敗機率為：

$$
p.
$$

做：

$$
n
$$

次測試都沒有觀察到失敗。

則：

$$
P
(
\text{zero failures}
\mid p
)
=
(1-p)^n.
$$

若希望構造 confidence level：

$$
1-\delta,
$$

令：

$$
(1-p_U)^n
=
\delta.
$$

得到：

$$
\boxed{
p_U
=
1-\delta^{1/n}.
}
$$

---

# 42. Zero-Failure Confidence Bound

## 定理 42.1

在 iid Bernoulli testing 假設下，

若 $n$ 次測試觀察到零失敗，

則 one-sided exact frequentist upper-confidence construction 可寫成：

$$
\boxed{
p
\le
1-\delta^{1/n}
}
$$

於 confidence level：

$$
1-\delta.
$$

此式等價於 zero-failure Clopper–Pearson upper bound。

### 解釋

它不是：

$$
p=0.
$$

而是：

> 在 iid sampling model 與指定 confidence interpretation 下，資料支持一個 failure-probability upper bound。

因此：

$$
\boxed{
\text{zero observed failures}
\neq
\text{zero failure probability}.
}
$$

---

# 43. Statistical Certification 的 Scope

若測試分布：

$$
X\sim\mathcal D
$$

則統計結論通常是：

$$
P_{X\sim\mathcal D}
[
\text{failure}
]
\le
\varepsilon
$$

with some confidence。

它不自動推出：

$$
\forall x\in K,
\quad
\text{safe}.
$$

因為 distributional safety 與 worst-case safety 是不同命題。

---

# 44. Probabilistic Guarantee 與 Worst-Case Guarantee

因此至少要分開：

$$
\boxed{
P_{\mathcal D}
(
\text{unsafe}
)
\le
\varepsilon
}
$$

與：

$$
\boxed{
\operatorname{Reach}(K)
\cap
\mathcal U
=
\varnothing.
}
$$

前者允許低機率 unsafe states。

後者要求指定域中完全不可達。

兩者都可能有價值，

但不能互相改寫。

---

# 45. Probably-Approximately-Global 類保證的位置

近年的 neural robustness verification 研究開始建立：

- local formal oracle；
- sampling；
- coverage；
- probabilistic relaxation；

之間的中間層。

這說明 verification 並非只有：

$$
\text{formal global proof}
$$

與：

$$
\text{ordinary empirical testing}
$$

兩個極端。

GPC-CS 因此允許：

$$
\boxed{
\text{probabilistic certificate}
}
$$

成為明確證據類型。

但它必須寫清：

- probability space；
- confidence；
- approximation scope；
- local verifier assumptions。

---

# 46. 證據強度階梯

本文定義一個**命題相對**的 evidence ladder，而不是普遍排名所有研究方法。

對 universal property：

$$
\forall x\in K,\;P(x),
$$

可區分：

### E0 — Anecdotal Observation

觀察少數案例。

### E1 — Systematic Testing

依明確 test plan 掃描大量案例。

### E2 — Statistical Guarantee

在明確抽樣模型下給 probabilistic bound。

### E3 — Falsification / Counterexample

找到一個有效違反例即可否證 universal claim。

### E4 — Bounded Exhaustive Verification

對有限／明確 bounded domain 完整枚舉或 solver-complete 驗證。

### E5 — Formal Certificate / Proof

在模型與假設下建立 universal theorem。

### E6 — Runtime-Transferred Guarantee

除了 E5，還有可證 model-to-runtime conformance margin。

這些層不是所有研究問題中的絕對線性排名。

例如 E3 對反證全稱命題具有決定性，但不能證明其相反全稱命題。

---

# 47. Evidence Type 必須對應 Claim Type

若 claim 是：

$$
\exists x:
\neg P(x),
$$

一個 counterexample 已經是完整證明。

若 claim 是：

$$
P_{\mathcal D}(\neg P)\le\varepsilon,
$$

需要統計／機率證明。

若 claim 是：

$$
\forall x\in K:
P(x),
$$

通常需要 exhaustive argument、formal proof 或足以覆蓋 $K$ 的結構性證書。

因此：

$$
\boxed{
\text{evidence strength is quantifier-relative}.
}
$$

---

# 48. Verification Coverage

定義被真正驗證的集合：

$$
K_{\mathrm{ver}}
\subseteq
K_{\mathrm{claim}}.
$$

若：

$$
K_{\mathrm{ver}}
\neq
K_{\mathrm{claim}},
$$

就存在 coverage gap：

$$
\boxed{
\mathcal G_{\mathrm{cov}}
=
K_{\mathrm{claim}}
\setminus
K_{\mathrm{ver}}.
}
$$

任何 proof / test report 都應明確標出：

$$
K_{\mathrm{ver}}.
$$

---

# 49. Scope Inflation Error

如果只證明：

$$
\forall x\in K_{\mathrm{ver}},
\quad
P(x),
$$

卻寫成：

$$
\forall x\in K_{\mathrm{claim}},
\quad
P(x),
$$

且：

$$
K_{\mathrm{ver}}
\subsetneq
K_{\mathrm{claim}},
$$

本文稱為：

$$
\boxed{
\text{scope inflation}.
}
$$

這不是數學反例本身，

而是證據陳述錯誤。

---

# 50. Assumption Ledger

令模型依賴假設：

$$
A
=
\{
a_1,\ldots,a_m
\}.
$$

例如：

- dynamics class；
- bounded noise；
- observation calibration；
- independent sampling；
- fixed topology；
- Lipschitz constant；
- no hidden mode；
- arithmetic semantics。

本文要求 proof statement 寫成：

$$
\boxed{
A
\Rightarrow
(M\models\varphi).
}
$$

而不是隱去 $A$。

---

# 51. Assumption Failure

如果 runtime：

$$
M^\star
$$

不滿足：

$$
A,
$$

則原 theorem 可能完全仍然正確，

只是：

$$
M^\star
$$

不在 theorem scope。

因此：

$$
\boxed{
\text{assumption violation}
\neq
\text{proof error}.
}
$$

但對部署安全而言，

兩者同樣可能讓保證失效。

---

# 52. Model Error 與 Specification Error

至少需要分開：

### Model Error

$$
\widehat M
\neq
M^\star.
$$

### Specification Error

$$
\varphi
$$

沒有捕捉真正需要的 property。

即使模型完美，

錯規格仍可：

$$
\widehat M\models\varphi
$$

但實際需求失敗。

即使規格完美，

錯模型也可讓 proof 無法轉移。

---

# 53. Observation Error

第三種是：

$$
H_{\mathrm{model}}
\neq
H_{\mathrm{runtime}}.
$$

例如：

- sensor drift；
- telemetry omission；
- hidden state；
- quantization；
- aggregation。

因此 verification stack 至少包含：

$$
\boxed{
\text{model correctness}
+
\text{specification adequacy}
+
\text{observation adequacy}.
}
$$

---

# 54. Deployment Arithmetic 也是模型的一部分

如果 verification 假設 real arithmetic / exact floating-point abstraction，

而部署系統使用不同：

- precision；
- ordering；
- hardware kernels；
- stochastic implementation；

則 runtime semantics 已經改變。

2025 年 neural verification 的 practical-soundness work 正是對這條 gap 提出直接警告。

GPC-CS 因此把 execution semantics 納入：

$$
A.
$$

---

# 55. 可觀測安全證書

除了 state-level certificate：

$$
B(x),
$$

有時希望從：

$$
y=H(x)
$$

直接建立：

$$
\widetilde B(y).
$$

若：

$$
B
=
\widetilde B\circ H,
$$

則 certificate 是 observation-factorizable。

由定理 5.1，

這要求 $B$ 在 $H$ fibers 上保持相同值。

---

# 56. Certificate Observability

定義 certificate $C(x)$ 對 $H$ 可觀測，若存在：

$$
\tilde C
$$

使：

$$
C=\tilde C\circ H.
$$

因此：

$$
\boxed{
\text{property observable}
}
$$

與：

$$
\boxed{
\text{certificate observable}
}
$$

不是同一件事。

安全 property 可以可觀測，

但某個特定 proof certificate 仍不可從 telemetry 重建。

---

# 57. Runtime Monitoring

若完整 universal proof 不可得，

可以使用 runtime monitor：

$$
M_t
=
\mathcal M
(
y_{0:t}
).
$$

monitor 可以判斷：

- observed property；
- margin；
- anomaly；
- specification violation。

但若：

$$
\mathcal A_{H,T}^{\mathcal S}
\neq\varnothing,
$$

即時間窗 observation fiber 仍跨越 safe/unsafe states，

runtime monitor 也無法對 hidden safety truth 完全正確。

---

# 58. Runtime Monitoring 不等於 Offline Verification

Offline verification 問：

$$
\forall
\text{ admissible trajectories},
\quad
\varphi?
$$

Runtime monitoring 問：

$$
\text{目前已觀察軌跡前綴是否符合／接近違反 }\varphi?
$$

因此：

$$
\boxed{
\text{monitoring}
\neq
\text{verification}.
}
$$

但 monitoring 可以提供：

- conformance evidence；
- assumption checks；
- runtime falsification。

---

# 59. GPC-CS Claim Record

本文建議未來每一個 GPC-CS 可實驗命題都存成：

$$
\boxed{
\mathfrak R_{\mathrm{claim}}
=
(
C,
K,
A,
H,
M,
E,
R
).
}
$$

其中：

- $C$：claim；
- $K$：scope；
- $A$：assumptions；
- $H$：observation map；
- $M$：model；
- $E$：supporting evidence；
- $R$：refutation / countercondition。

這是理論資料庫最小 provenance schema。

---

# 60. Paper 00 的可反證接口

Paper 00 的核心條件命題：

> 若 GPC-like technologies emerge，carrier-state safety becomes relevant.

其反證／收縮方向包括：

- communication never causes persistent carrier-state update；
- carrier-relative safety effects negligible；
- symbol layer remains cleanly separated from persistent state dynamics。

因此 Paper 00 本身不是：

$$
\boxed{
\text{future must become GPC}.
}
$$

而是 conditional research program。

---

# 61. Paper 01 的可反證接口

Paper 01 主張：

$$
\mathcal S_G^\star
=
\left(
\prod_i
\mathcal S_i
\right)
\cap
\mathcal C_G
$$

在存在 relation constraints 時比單純 product 更完整。

若所有實際重要系統都發現：

$$
\mathcal C_G
=
\mathcal X_G,
$$

則 relational-safety extension 收縮。

可觀測需求：

$$
H_G
$$

必須足以辨識：

$$
\mathcal C_G
$$

是否成立。

---

# 62. Paper 02 的可反證接口

Paper 02 的核心是：

$$
T,
D,
\text{fibers},
\text{side information}.
$$

可測對象包括：

- task observable fidelity；
- representation / function mismatch；
- reconstruction dependence on receiver state。

若：

$$
D(u,x_1)
\approx
D(u,x_2)
$$

對所有相關 states 都成立，

state-dependent reconstruction importance 下降。

---

# 63. Paper 03 的可反證接口

Paper 03 定義：

$$
\mathfrak C(x).
$$

可驗證問題：

- throughput；
- active-memory limit；
- temporal resolution；
- service/backlog；
- capacity–fidelity envelope。

若單一資源即可預測全部 behavior，

多維容量模型可簡化。

---

# 64. Paper 04 的可反證接口

Paper 04 的核心：

$$
O_\alpha
$$

與：

$$
\langle\mathfrak O\rangle.
$$

可觀測：

- repeated-update trajectory；
- fixed points；
- order defect；
- switching behavior。

如果所有 relevant operators 幾乎 idempotent / commuting，

recursive and order-sensitive risk importance 收縮。

---

# 65. Paper 05 的可反證接口

Paper 05 定義 cross-gains：

$$
\gamma_{AB},
\qquad
\gamma_{BA}.
$$

如果成熟系統：

$$
\gamma_{BA}\approx0
$$

或：

$$
\gamma_{AB}\approx0,
$$

bidirectional-loop analysis 退化成單向。

generalized synchronization：

$$
\mathcal M_h
$$

也必須有可測 $h$ 與 transverse error。

---

# 66. Paper 06 的可反證接口

Paper 06 的核心是：

- noninjective update；
- history dependence；
- recovery language；
- safe recovery path。

若：

$$
\Phi|_K
$$

普遍穩定可逆，

且 recovery path 始終安全，

irreversibility layer importance 下降。

---

# 67. Paper 07 的可反證接口

Paper 07 的 observable claims：

$$
\Psi,
\mathbf C,
B_\tau.
$$

可測：

- representation drift；
- information recoverability；
- functional continuity；
- lineage branching。

但：

$$
\mathfrak F
$$

first-person continuity 目前不在 identified observable model 中。

因此它不能被 Paper 07 的外部資料直接證成或證偽。

---

# 68. Paper 08 的可反證接口

Paper 08 可測：

$$
p_i,
\Sigma_F,
\Omega_{ij},
D_i,
\text{higher-order joint failures}.
$$

若實證顯示 failure dependence 可忽略，

common-mode layer 可弱化。

若 structural heterogeneity 與 failure independence 有穩定關係，

依賴模型可簡化。

---

# 69. Paper 09 的可反證接口

Paper 09 可測／估計：

$$
G_t,
A_H,
S_t,
G(S_t).
$$

核心反證條件包括：

- influence truly local；
- no state-dependent network reconfiguration；
- no meaningful transient amplification；
- cascade map nonmonotone under claimed theorem scope。

因此：

$$
\boxed{
\text{cascade theory must be tested as dynamics, not inferred from correlation alone}.
}
$$

---

# 70. 系列統一 Verification Matrix

整個 GPC-CS 可壓成：

| 理論層 | Latent object | 可觀測／證據接口 |
|---|---|---|
| Carrier safety | $x,\mathcal S$ | state proxy, barrier/reachability, violation |
| Transduction | $T,D$ | task fidelity, side-information dependence |
| Capacity | $\mathfrak C$ | rate, memory, latency, backlog |
| Operator | $O_\alpha$ | repeated-update trajectories |
| Coupling | $\Gamma_{AB}$ | cross-response, synchronization error |
| History | $h,\Phi_w$ | path dependence, recovery residual |
| Continuity | $\Psi,\mathbf C$ | observable/function/lineage measures |
| Common mode | $\Sigma_F,D_i$ | joint failures, dependency structure |
| Cascade | $G(S),\mathcal C$ | transient response, mode changes, closure |
| Verification | $H,M,\varphi$ | proofs, counterexamples, conformance |

此表不是說每個 latent object 都必然能被完全識別。

它只是要求每個 claim 說清楚：

> 你到底打算用什麼 evidence 連到它？

---

# 71. Verification Dependency Graph

驗證結論本身也有依賴鏈：

$$
\boxed{
\text{observation}
\rightarrow
\text{identification}
\rightarrow
\text{model}
\rightarrow
\text{specification}
\rightarrow
\text{certificate}
\rightarrow
\text{deployment transfer}.
}
$$

任一層失效，

都可能讓最終 runtime claim 需要降級。

---

# 72. Claim Strength Degradation

因此可以定義：

### Strongest

$$
M^\star\models\varphi
$$

有 runtime-transfer proof。

### Model-level

$$
\widehat M\models\varphi.
$$

### Probabilistic

$$
P(\neg\varphi)\le\varepsilon
$$

在明確 distribution 下。

### Tested

在有限 test set 未見 violation。

### Anecdotal

少數觀察支持。

本文要求語言與 evidence level 對齊。

---

# 73. 可重現性不是 Validity 的同義詞

即使一個實驗可以 bit-for-bit 重現，

它仍可能：

- 規格錯；
- 模型錯；
- scope 太小；
- observation map 不足。

因此：

$$
\boxed{
\text{reproducible}
\neq
\text{valid for claimed theorem}.
}
$$

但 reproducibility 是 evidence auditing 的重要必要層。

---

# 74. 驗證包應保存什麼

對未來 GPC-CS 實驗／形式驗證，

至少應保存：

- model version；
- specification；
- scope；
- assumptions；
- solver / proof artifact；
- observation schema；
- dataset / trace provenance；
- random seeds if relevant；
- numerical precision；
- runtime environment；
- counterexamples；
- unresolved cases。

本文不規定具體儲存格式。

---

# 75. UNKNOWN 的透明度

若：

$$
V(M,\varphi)
=
\mathrm{UNKNOWN},
$$

應保存原因：

- timeout；
- unsupported operator；
- numerical uncertainty；
- overapproximation；
- state explosion；
- incomplete observation。

這能避免「沒有結果」在後續 handoff 中被誤傳成 positive result。

---

# 76. Falsification Record

若找到 counterexample：

$$
c,
$$

應區分：

### Model Counterexample

$$
c
$$

違反：

$$
\widehat M\models\varphi.
$$

### Runtime Counterexample

真實部署 trace 違反：

$$
\varphi.
$$

### Specification Counterexample

事件顯示：

$$
\varphi
$$

即使成立也沒有捕捉真正安全需求。

三者修正方向不同。

---

# 77. Model Refutation 不等於 Theory Refutation

如果某個具體：

$$
\widehat M
$$

被反例推翻，

只代表：

$$
\widehat M
$$

不足。

GPC-CS 的更高層 framework 只有在其 structural claims 也被系統性否定時才需要收縮。

因此必須分開：

$$
\boxed{
\text{instance falsification}
}
$$

與：

$$
\boxed{
\text{framework falsification}.
}
$$

---

# 78. Framework Falsification

例如若大量成熟跨載體系統都顯示：

- carrier state 幾乎不影響 reconstruction；
- cross-gains negligible；
- history irrelevant；
- failure independence high；
- network reconfiguration absent；

那麼 GPC-CS 的廣義強版本就被實證壓縮成較接近傳統通信安全的窄版本。

這就是一個真正可被世界修正的理論。

---

# 79. 理論成功也不要求所有風險都出現

反過來，

如果只觀察到：

- carrier-relative reconstruction；
- capacity dependence；

但沒有：

- identity-related drift；
- cascades；

也不表示前兩層失效。

GPC-CS 是模組化條件理論。

不是：

$$
\boxed{
R_C,R_T,R_K,R_O,R_B,R_I,R_U,R_M,R_G
\text{ 必須全部同時存在}.
}
$$

---

# 80. 科學性來自可收縮性

一個好的前瞻安全理論不應只能：

> 無論發生什麼都說自己對。

因此本文要求每個強主張都具有：

$$
\boxed{
\text{conditions under which it becomes unnecessary}.
}
$$

也就是：

> 未來資料若顯示某風險機制沒有實質作用，理論應縮小，而不是重新解釋到永遠無法被反駁。

---

# 81. Paper 10 的十二個主命題

## 命題 A：Property observability 是 fiber constancy

$$
\boxed{
P=g\circ H
\iff
P
\text{ 在 }H\text{ fibers 上為常數}.
}
$$

## 命題 B：Safety ambiguity fiber 使 observation-only exact safety classification 不可能

$$
\mathcal A_H^{\mathcal S}\neq\varnothing.
$$

## 命題 C：完整 state observability 比 property observability 強

安全驗證不一定需要完整重建所有 latent state。

## 命題 D：Linear observability 可由 Kalman rank criterion 精確判定

$$
\operatorname{rank}(\mathscr O_n)=n.
$$

## 命題 E：有限測試在沒有額外結構時不推出 universal safety

由定理 35.1。

## 命題 F：一個 counterexample 足以反證 universal safety，而 failure-to-falsify 不等於 verification

由量詞不對稱。

## 命題 G：Formal verification 必須明確綁定 model、specification、scope 與 assumptions

$$
\mathfrak V=(M,\varphi,K,H,A).
$$

## 命題 H：UNKNOWN 必須保留為第三種合法驗證結果

不能靜默升級。

## 命題 I：Model-level proof 不自動轉移到 runtime

需要 model discrepancy / conformance bound。

## 命題 J：足夠 specification margin 可以吸收 bounded model error

$$
\boxed{
L_h\varepsilon_t<m_t
\Rightarrow
h(x_t^\star)>0.
}
$$

## 命題 K：零失敗測試提供 statistical upper bound，而非 $p=0$

$$
\boxed{
p_U=1-\delta^{1/n}.
}
$$

## 命題 L：GPC-CS 必須是可反證、可收縮的條件理論

沒有反證條件的強主張不屬於本系列最終公共版本。

---

# 82. 可證偽性

Paper 10 本身也可以被修正。

## 82.1 所有重要 GPC properties 都由簡單 telemetry 完全決定

若：

$$
\mathcal A_H^P=\varnothing
$$

對所有重要 properties 與成熟系統都成立，

hidden-state observability problem 的實際重要性下降。

## 82.2 Runtime 與 verified model 幾乎完全一致

若可證：

$$
\varepsilon_t\approx0
$$

且 arithmetic/runtime semantics 完全等價，

model-to-deployment gap 可以忽略。

## 82.3 有限測試域本身就是完整有限 domain

若：

$$
D=K
$$

且已完全枚舉，

定理 35.1 的未測點限制不適用。

## 82.4 形式驗證取得完整 scalability

若未來所有 relevant GPC models 都能被 sound-and-complete verifier 在可接受成本內決定，

probabilistic / falsification / incomplete methods 的必要性會下降。

---

# 83. Core Series Closure：Paper 00–10

至此核心系列形成十一篇：

### Paper 00
廣義相位交流與載體安全總論。

### Paper 01
載體狀態空間與安全域。

### Paper 02
跨載體轉導與重建錯配。

### Paper 03
容量向量、維度錯配與更新速率。

### Paper 04
算子誘發風險與遞歸動力學。

### Paper 05
雙向相位耦合與反向影響。

### Paper 06
不可逆更新與路徑依賴安全。

### Paper 07
身份漂移與跨載體連續性。

### Paper 08
共模失效與異質載體韌性。

### Paper 09
全域相位網路與級聯動力學。

### Paper 10
可觀測性、可驗證性與反證框架。

這十一篇構成 GPC-CS 第一個完整理論閉環。

---

# 84. 整體數學骨架

整個核心系列可壓縮成：

$$
\boxed{
x
\xrightarrow{E}
z
\xrightarrow{T}
u
\xrightarrow{D(\cdot,x)}
r
\xrightarrow{F}
x^+
}
$$

單載體安全：

$$
\boxed{
x\in\mathcal S.
}
$$

容量：

$$
\boxed{
q\in\mathfrak C(x).
}
$$

算子：

$$
\boxed{
x^+=O_\alpha(x).
}
$$

雙向：

$$
\boxed{
(x_A^+,x_B^+)
=
\Gamma_{AB}(x_A,x_B).
}
$$

歷史：

$$
\boxed{
x_w=\Phi_w(x_0).
}
$$

群體：

$$
\boxed{
\mathbf X_{t+1}
=
\Gamma_G(\mathbf X_t).
}
$$

全域安全：

$$
\boxed{
\Gamma_G
(
\mathcal S_G^\star
)
\subseteq
\mathcal S_G^\star.
}
$$

觀測：

$$
\boxed{
y=H(x).
}
$$

驗證：

$$
\boxed{
V(M,\varphi)
\in
\{
\mathrm{PROVED},
\mathrm{REFUTED},
\mathrm{UNKNOWN}
\}.
}
$$

---

# 85. 核心系列的最終問題

Paper 00 一開始問：

> 如果未來交流不再只是訊息，而是狀態耦合，安全問題會變成什麼？

Paper 10 現在可以給出完整答案。

我們至少必須知道：

1. **狀態是什麼？**
2. **什麼狀態叫安全？**
3. **轉導保留了什麼？**
4. **載體能承受多少？**
5. **輸入誘發了什麼更新算子？**
6. **雙方是否形成閉環？**
7. **歷史是否可逆、可恢復？**
8. **哪些 identity-related quantities 持續？**
9. **多個載體是否共享失效模式？**
10. **局部擾動是否變成網路動力學？**
11. **以上這些東西，我們到底觀察得到、驗證得到、反駁得到嗎？**

第十一問是前十問成為科學研究，而不只是形式敘事的條件。

---

# 86. 最終結論

一套安全理論可以在紙上定義非常漂亮的：

$$
\mathcal X,
\quad
\mathcal S,
\quad
T,
\quad
D,
\quad
O,
\quad
\Gamma,
\quad
G.
$$

但如果真實系統只輸出：

$$
y=H(x),
$$

而：

$$
H
$$

把安全與不安全狀態壓在同一 fiber 中，

那麼外部觀察者根本不能從 $y$ 完整判斷 safety truth。

因此 Paper 10 的第一個根本結果是：

$$
\boxed{
P=g\circ H
\iff
P
\text{ is constant on observation fibers}.
}
$$

第二個根本限制是：

$$
\boxed{
\text{finite successful testing}
\not\Rightarrow
\text{universal safety}.
}
$$

第三個則是量詞不對稱：

$$
\boxed{
\text{one valid counterexample}
\Rightarrow
\text{universal claim refuted},
}
$$

但：

$$
\boxed{
\text{failure to find a counterexample}
\not\Rightarrow
\text{universal claim proved}.
}
$$

第四個是 deployment boundary：

$$
\boxed{
\widehat M\models\varphi
\not\Rightarrow
M^\star\models\varphi
}
$$

除非我們另外控制 model gap。

若：

$$
h(\hat x)\ge m,
$$

$$
d(x^\star,\hat x)\le\varepsilon,
$$

以及：

$$
L_h\varepsilon<m,
$$

才得到一個最簡潔的 robust transfer：

$$
\boxed{
h(x^\star)>0.
}
$$

因此，GPC-CS 第一個核心系列的最終原則不是：

> 我們已經知道未來一定會出現這些危險。

而是：

$$
\boxed{
\text{If such coupling structures emerge, define them clearly enough that they can be observed, verified, or refuted before they become invisible assumptions.}
}
$$

這正是本系列最初的目的：

> 不等技術完成之後才第一次問下一步會發生什麼。

但同樣重要的是：

> 也不因為我們提前提出了數學框架，就把未來尚未觀測到的機制寫成既成事實。

所以 GPC-CS 的公共理論應永久保留三個出口：

$$
\boxed{
\text{PROVE},
\qquad
\text{REFUTE},
\qquad
\text{REVISE}.
}
$$

若未來資料支持某一層，就把它提升為更強的實證理論。

若資料反對某一層，就收縮它。

若觀測能力不足，就標記 unknown。

這不是理論的退讓。

這是它能夠真正活到未來技術出現時，仍然具有科學價值的必要條件。

---

# 參考文獻

1. Kalman, R. E. (1960). Contributions to the Theory of Optimal Control. *Boletín de la Sociedad Matemática Mexicana*, 5, 102–119.
2. Hermann, R., & Krener, A. J. (1977). Nonlinear Controllability and Observability. *IEEE Transactions on Automatic Control*, 22(5), 728–740. DOI: 10.1109/TAC.1977.1101601.
3. Takens, F. (1981). Detecting Strange Attractors in Turbulence. In *Dynamical Systems and Turbulence, Warwick 1980*, Lecture Notes in Mathematics 898, 366–381. DOI: 10.1007/BFb0091924.
4. Prajna, S., Jadbabaie, A., & Pappas, G. J. (2007). A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates. *IEEE Transactions on Automatic Control*, 52(8), 1415–1428. DOI: 10.1109/TAC.2007.902736.
5. Fainekos, G. E., & Pappas, G. J. (2009). Robustness of Temporal Logic Specifications for Continuous-Time Signals. *Theoretical Computer Science*, 410(42), 4262–4291. DOI: 10.1016/j.tcs.2009.06.021.
6. Donzé, A., & Maler, O. (2010). Robust Satisfaction of Temporal Logic over Real-Valued Signals. In *FORMATS 2010*, LNCS 6246, 92–106. DOI: 10.1007/978-3-642-15297-9_9.
7. Annpureddy, Y., Liu, C., Fainekos, G. E., & Sankaranarayanan, S. (2011). S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In *TACAS 2011*, LNCS 6605.
8. Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv:1702.01135; CAV 2017.
9. Xiang, W., Tran, H.-D., & Johnson, T. T. (2017/2018). Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations. arXiv:1712.08163.
10. Szász, A., Bánhelyi, B., & Jelasity, M. (2025). No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks. *Proceedings of ICML 2025*, PMLR 267, 58088–58105.
11. Blohm, P., Indri, P., Gärtner, T., & Malhotra, S. (2025). Probably Approximately Global Robustness Certification. *Proceedings of ICML 2025*, PMLR 267, 4570–4587.
12. Boetius, D., Leue, S., & Sutter, T. (2025). Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound. *Proceedings of ICML 2025*, PMLR 267, 4660–4699.
13. Kresse, F., Yu, E., Lampert, C. H., & Henzinger, T. A. (2025). Logic Gate Neural Networks are Good for Verification. *Proceedings of the International Conference on Neuro-symbolic Systems*, PMLR 288, 90–103.
14. Chehade, M. F. E. H., Li, W., Bell, B. W., Bent, R., Kazi, S. R., & Zhu, H. (2025). LEVIS: Large Exact Verifiable Input Spaces for Neural Networks. *Proceedings of ICML 2025*, PMLR 267, 7634–7647.

---

# 系列狀態

**Series:** Generalized Phase Communication and Carrier Safety  
**Paper:** 10  
**Version:** v1.0  
**Canonical source encoding:** UTF-8  
**Canonical mathematics delimiters:** ` $...$ ` and `$$...$$` only  
**Operational high-risk experiment details:** Excluded  
**Governance/deployment prescriptions:** Out of scope  
**Depends on:** Paper 00–09  
**Core Series Status:** CLOSED — Foundation Cycle 00–10 complete