---
title: "TCGCT × TCGQT v0.5：型別化證明義務圖、精確調和證書與局部失效重驗"
english_title: "Typed Proof-Obligation DAGs, Exact Harmonic Certificates, and Incremental Revalidation"
version: "0.5 / research prototype"
date: "2026-11-02"
author: "Neo.K / EveMissLab"
research_collaboration: "GPT-6"
status: "DRAFT / SCOPE-BOUNDED MATHEMATICS / EXECUTABLE PROTOTYPE / NOT A BSD PROOF"
canonical_source: "UTF-8 Markdown, LF, canonical dollar math delimiters only"
---

# TCGCT × TCGQT v0.5：型別化證明義務圖、精確調和證書與局部失效重驗

**作者：** Neo.K / EveMissLab  
**機構：** EveMissLab／一言諾科技有限公司  
**日期：** 2026-11-02  
**版本：** 0.5 / research prototype  
**研究協作（原稿所載）：** GPT-6  
**原稿狀態：** DRAFT / SCOPE-BOUNDED MATHEMATICS / EXECUTABLE PROTOTYPE / NOT A BSD PROOF  

## 摘要

本輪承接 v0.2 的有限循環群投影與循環多項式、v0.3 的有限交換群/Galois 軌道與連續尾項估計、v0.4 的有理週期分段線性函數及已證頻帶的連續提升。研究目標不是改造計算機速度，也不是聲稱證明 Birch–Swinnerton-Dyer 猜想，而是：在前提、對象型別、來源版本與驗證規格相同時，**已驗證的數學義務能否合法重用；變動時，能否精確失效並只重做受影響的證書檢查**。

實作一個有向無環證明圖。葉節點是完整的有型別精確數學來源，內部節點是明確的定理應用或精確判定；每個節點指向其直接前提，並包含來源、前提及驗證規格的內容摘要。初次檢查對目標的閉包逐一計算；同一活驗證器程序內，若版本、內容及程式契約均未變，可重用此前由驗證器實際計算過的結果。外部傳入的序列化證書不構成快取權威，必須從原始來源重新計算並逐位元組比對。

在 240 點週期模輪、有理三角折線、12 段帳篷函數和顯式有理 Laurent 三角多項式的共同範例中，11 個相依節點初次執行 11 次檢查；完全相同的再次查核重新執行 0 次；只更改三角折線來源，重新執行 4 次，另外 7 個重用。這些是**檢查函式執行次數**，不是端到端效能、複雜度或跨程序持久化速度證明。

## 1. 形式化責任邊界

本版把四件事分離：

- **來源給定**：數列、精確折點或 Laurent 係數由外界提供，格式與型別可查，來源本身的真實作者身份未獲證實；結果狀態為 `SOURCE_GIVEN` 而不是數學命題 `PASS`。
- **單項證書**：數學義務指定算子、適用域與精確前提。其結論標成 `PASS`、`REFUTED` 或 `UNRESOLVED`。
- **證明圖合取**：僅當所有子義務皆 `PASS` 才 `PASS`，不會因為其中一個不明而猜測成立；合取不是一條新的 BSD 定理。
- **重驗快取**：只接納本程序這個驗證器已執行過、內容與程式指紋未改的節點。磁碟上附有 hash 的外部 JSON receipt 不可直接授權跳過數學檢查。

每個來源有 `source_id`、`revision`、完整精確 `payload`。這些欄位是資料追溯標籤，而非發行者數位簽章。所有值保留精確有理數或整數，不接收 float 作為數學原始輸入。

## 2. 從有限拓樸纖維到調和支撐：嚴格可重用的定理

令 $N$ 為正整數， $m\mid N$， $G=\mathbb Z/N\mathbb Z$， $H=m\mathbb Z/N\mathbb Z$。對有型別的有限函數 $f:G\to\mathbb Z$，定義沿商映射纖維的平均：

$$
(P_m f)(r)=\frac{m}{N}\sum_{j=0}^{N/m-1} f(r+mj).
$$

若明確檢查了 $f(n+m)=f(n)$ （模 $N$ ），則 $f=P_m f$，故 $f$ 可經 $G/H\cong\mathbb Z/m\mathbb Z$ 因子化。以標準離散傅立葉變換表示：

$$
\widehat f(k)=\sum_{n=0}^{N-1}f(n)\exp(-2\pi i kn/N).
$$

把 $n=r+mj$ 代入並提取公比得：

$$
\widehat f(k)=\sum_{r=0}^{m-1}f(r)\exp(-2\pi i kr/N)\sum_{j=0}^{N/m-1}\exp(-2\pi i kj/(N/m)).
$$

第二個和只有當 $(N/m)\mid k$ 才可能不為零。故：

$$
(N/m)\nmid k\quad\Longrightarrow\quad\widehat f(k)=0.
$$

這不是實驗推論，而是有限循環群角色正交定理。若纖維恆定已獲精確檢查，則**一個有限群正交證書**合法給出 $N-m$ 個頻率的精確零結論，無需逐頻率使用浮點 FFT。

### 實例：模 6 候選函數

取 $N=240$ 、 $m=6$，令 $f(n)$ 對 $n\bmod6\in\{1,5\}$ 為 1，其餘為 0。檢查 240 個精確值後，頻譜的可能非零位置僅有 $0,40,80,120,160,200$，其餘 234 個頻率被群論證明為零。注意這是 **模輪候選函數**，不是質數指示函數。

真實的 $0\le n<240$ 質數指示函數在模 6 纖維上**不恆定**；例如 1 和 7 在同一餘類而其質數性不同。該證書對它回報 `REFUTED`，其調和支撐推論回報 `UNRESOLVED`。因此，不能將 234 個零頻率的結論非法移植到真正的質數訊號。

## 3. 將有理折線的分析義務化為整數多項式

對完整給出的週期分段線性函數 $f$，折點 $t_j=a_j/L$ 均有理，跨折點斜率跳躍記作 $\Delta s_j$。對任意非零整數 $k$，分布導數及傅立葉積分分部給出：

$$
\widehat f(k)=-\frac{1}{4\pi^2 k^2}\sum_j\Delta s_j\exp(-2\pi i k t_j).
$$

取公共分母將斜率跳躍整數化，在 $\mathbb Z[X]$ 構造相應多項式 $A_k(X)$ ；指數模 $L$ 化約後， $\widehat f(k)=0$ 當且僅當 $A_k(X)$ 可以被第 $L$ 個循環多項式 $\Phi_L(X)$ 整除。這裡的等價只針對**已完整給出折點的週期分段線性函數，且 $k\ne0$**；零頻率須另以有理梯形積分計算。

v0.5 沿用 v0.4 的精確跳躍多項式法，並用分段端點的另一種求和構造及獨立的有理多項式長除法交叉核查。對 12 段重複帳篷函數：第 11 頻率精確為零，第 12 頻率精確非零；即使 12 個等距樣本全部為零，也不得否定連續函數的非零頻率。

## 4. 分析尾項與低頻存在性：由數值比較轉成有理嚴格不等式

對連續週期分段線性函數，Parseval 與導數能量給出：

$$
\sum_{|k|>K}|\widehat f(k)|^2
\le \frac{\int_0^1|f'(t)|^2\,dt}{4\pi^2(K+1)^2}
<\frac{\int_0^1|f'(t)|^2\,dt}{36(K+1)^2}.
$$

另外，若 $V$ 為週期斜率總跳躍絕對值，對 $K\ge1$ 有可獨立檢查的上界：

$$
\sum_{|k|>K}|\widehat f(k)|^2\le\frac{V^2}{1944K^3}.
$$

由有理折點、端點值與斜率可精確計算均值、變異、導數能量及 $V$，並取兩個上界較小者。如果變異嚴格大於尾項上界，則 $1\le|k|\le K$ 必有至少一個非零傅立葉係數。這只是一個**存在性證書**，並不指定特定非零頻率。

對三角折線 $(0,0),(1/2,1/2),(1,0)$，其變異為 $1/48$ ；取 $K=1$，本版的尾項上界為 $1/144$，所以低頻必有非零項。改成全零折線後，嚴格不等式不再成立；相應節點必須轉為 `UNRESOLVED`。

## 5. 頻帶已知與頻帶猜測，不得混同

若資料源*本身*完整列出了有限 Laurent 三角多項式：

$$
F(t)=\sum_{|k|\le K}a_k\exp(2\pi i kt),\qquad a_k\in\mathbb Q,
$$

並能精確檢查 $n>2K$ 個不同等距樣本均為零，則乘以 $\exp(2\pi i Kt)$ 後得到一個至多 $2K$ 次的多項式，有 $n$ 個不同根，只能恆零，因此連續 $F$ 恆零。這是多項式根數的定理，不是有限取樣憑空發現頻帶。

反例取 $F(t)=\cos(24\pi t)-1$。對 $n=12$ 個等距樣本它處處為零，但 $K=12$ 且 $12\not>24$，所以絕不能提升。證書回報 `UNRESOLVED` 和 `ALIASING_GRID_ZERO_NOT_CONTINUUM_ZERO`。完整零係數來源和充足取樣則可以 PASS。

## 6. 證書依賴圖與內容定址

圖中每個節點 $v$ 包含節點 ID、型別、固定參數及直接依賴。以有序 canonical UTF-8 JSON 表示節點資料，遞迴計算摘要：

$$
h_v=\operatorname{SHA256}(\operatorname{Canonical}(\mathcal S,v,h_{d_1},\ldots,h_{d_r})).
$$

 $\mathcal S$ 是本版固定語義契約。實際可重用的快取鍵另含**驗證程式碼的 SHA-256 指紋**，所以相同來源資料不能跨不同核查程式版本直接重用 PASS。`SOURCE_GIVEN`、`PASS`、`REFUTED`、`UNRESOLVED` 類型分開；合取證書不能把來源存在或未知狀態當作數學證明。

### 6.1 局部失效原理

若依賴圖是 DAG，來源 $s$ 改變，只有 $s$ 的可達下游節點可能受到該變動影響；對來源及依賴摘要未改的其餘節點，可在**同一個未更改程式的活驗證器**內重用已驗證的輸出。其正確性來自定義：一個節點的確定性檢查只讀其固定 payload、參數和前提證書，且這些在雜湊一致下未變；沒有證據的任意外部副作用不在本版適用域。

這是一個帶假設的**快取正確性命題**，不是雜湊演算法自動證明所有程式正確。其前提包括：SHA-256 抗碰撞假設、程序內程式語義不變、來源完整、檢查器自身沒有未處理錯誤。對外部更改過的 JSON receipt，一律新建驗證器從完整來源重算；即使 receipt 數據有相同 hash 也不能跳過。

### 6.2 防護條件

- 依賴圖有環、缺失前提、同一 ID 重複、前提型別錯、非整數模數／頻率、浮點輸入：直接拒絕。
- 模數不整除群階數：不得推論角色支撐。
- 在已釘選的圖物件上偷偷原地改動：完整性守衛拒絕使用舊快取。
- 只改一個來源的 revision 但數值一樣：當成版本變動，使全部下游摘要失效。
- 外部快取、使用者附上的 PASS、來源路徑或雜湊字串：不構成可以跳過核查的授權。
- 僅有有限樣本、缺少完整頻帶或折點：不能冒充連續分析證據。

## 7. 可重播實驗與驗證義務計數

| 測試情境 | 本次實際執行的節點檢查 | 在同一程序內重用 | 結果 |
| --- | ---: | ---: | --- |
| `joint` 冷驗證 | 11 | 0 | PASS |
| `joint` 相同來源、第二次 | 0 | 11 | PASS |
| `joint_alt` 已有共同前提 | 2 | 7 | PASS |
| 三角折線由非零改成零，revision 升版 | 4 | 7 | UNRESOLVED |
| 恢復原釘選快照 | 0 | 11 | PASS |

這些不是固定規模的速度加速倍數。圖驗證仍必須重算 lightweight 的節點與依賴雜湊；本實驗也未提供跨程序簽章授權快取。只要進入新進程、驗證器程式變動，所有數學證書都必須 fresh replay。具體負擔可能取決於證書大小、頻譜基底、磁碟 I/O、記憶體與作業系統排程，尚未測量。

## 8. 反例與真正未解的問題

1. **共同錯誤仍可能存在。** 兩個計算器若用了相同錯誤的數學前提，測試全 PASS 仍不能上升為正確定理。本版以獨立有理多項式 oracle 對照有限頻譜與折線零判定，但不等於形式化 proof assistant 完全核證。
2. **雜湊不證明原稿作者。** source ID 和 SHA-256 只是追溯與完整性；未建立簽章、ACL、不可回滾日誌或多代理一致性。
3. **不能從群有限域跳到解析無限域。** 本版只在 v0.4 所列的有理折線/顯式有限頻帶等狹義函數類建立解析證書，不能從有限樣本推演任意解析或測度對象。
4. **沒有量測真正的驗證用時。** 已減少的只是重複調用的精確檢查義務，未量化 cold/warm 端到端速度。下輪應設獨立重播門檻與實際 CPU、記憶體、證書大小的可比較基準。
5. **無 BSD 結果。** 此包不修改 AMRAL 的 BSD 結論，不解決解析首項、Selmer/Heegner/Kato 等相關障礙，也不宣稱 rank-2 或高秩公式成立。

## 9. 接續方向

下一階段可以研究：跨程序的可信可重用證書（正式署名與審查金鑰、版本固定的 proof-checker、有限性界線），以及將本版子群平均/頻譜結構擴展到一般有限交換群的多層證書；也可以研究在可認證的函數類上傳播 Fourier 尾界，而不是每個上游微小變動都從頭推導。

若要把它接入 TCGCT／TCGQT 正式倉庫，應透過明確版號 adapter、隔離分支與本地代理測試，不要直接覆寫 P20/R0/R1 研究正本。

## 10. 原始資料及可執行接口

- `src/proof_dag.py`：型別化圖、精確計算、程序內安全重用、被動失效、保守狀態。
- `src/independent_oracle.py`：另寫的有理多項式/循環多項式 oracle，僅用於有界負例與交叉檢查。
- `src/rational_pl_spectrum.py`、`src/cyclotomic_exact.py`、`src/bandlimited_lift.py`：自凍結 v0.4 複製的精確檢查模組，不變更原作。
- `scripts/build_examples.py`：生成整個圖、受範圍限制的證據與 cold/warm/失效/恢復紀錄。
- `tests/`：型別錯誤、環、浮點、版本、來源、偽造 receipt、共因錯誤與獨立數學核查。
- `upstream_v04/`：64 份檔案，完整保留前代 v0.4 與嵌套 v0.3/v0.2 快照及其原始雜湊清單。

全部正式數學原始碼採 UTF-8 Markdown，且公式只用 ` $...$ ` 與 `$$...$$`。此檔本身是可保存的正式研究草稿**原始檔**，非聊天畫面渲染結果。文內定理均應依其明示定義域讀取，不作一般數學或物理世界的越界聲明。