---
title: "TCGCT × TCGQT：型別化最小充分前提集、結構式下界與調和命題證書"
english_title: "TCGCT–TCGQT v1.6: Typed Minimal Sufficient Premises, Structural Lower Bounds, and Harmonic Proof Certificates"
author: "Neo.K / EveMissLab"
collaboration: "GPT-6"
date: "2026-11-03"
version: "v1.6"
status: "RESEARCH PROTOTYPE / FINITE SCOPE / NOT A BSD PROOF"
canonical_source: "UTF-8 Markdown; inline math $...$ ; display math $$...$$"
upstream: "byte-identical v1.5 frozen source, 523 files"
---

**作者：** Neo.K / EveMissLab  
**機構：** EveMissLab／一言諾科技有限公司  
**日期：** 2026-11-03  
**版本：** v1.6  
**研究協作（原稿所載）：** GPT-6  
**原稿狀態：** RESEARCH PROTOTYPE / FINITE SCOPE / NOT A BSD PROOF  

# 摘要

研究目標是減少**數學驗證時必須獨立核查的充分前提數量**，不是直接提高數值運算速度，也不是假定較少證書一定具有較低的實際執行成本。本版接續 v1.5 的商群表示與型別化等價橋，建立兩套獨立的前提集算法（產生端的前向閉包，驗證端的等價類／不相交集合閉包）、兩種最小性核查，以及一條不宣稱最小性的輕量充分性驗證路徑。

在三種完整定義的模環表示（模 6、模 30、模 60）上，共九項跨表示的整數和與有限傅立葉命題，可由三個直接數學前提及兩個精確表示等價前提共同支撐。所需前提數從九個降至五個。嚴格的候選庫窮舉核查排除 794 組大小小於五的候選；更重要的是，對本例「所有定義都需要同一批命題型別」的矩形目標，存在簡短結構下界，不必逐一枚舉這 794 組。本研究把這個下界形式化、實作、加上型別與來源閘道，並獨立檢查其合法適用範圍。

**主張限度：** 所稱最小，只針對本稿規定的原子證書、有限集合、精確表示相等及相同命題的等價轉移規則。不能推論為任意形式系統的最短證明、最少位元、最低時間成本、新質數定理或 Birch–Swinnerton-Dyer 猜想的證明。

## 1. 問題與驗證模型

固定一個有限交換群 $G$。每個有型別的定義 $D_i$ 都給出一個完整函數 $f_i:G\to\mathbb Z$，其值可經有限商群 $Q_i$ 決定；完整定義的來源版本與內容指紋被另外釘選。定義 $E_{ij}$ 表示兩個函數在全部 $G$ 上外延相同。此事實必須經精確數學核查，不能只因名稱、總和或統計指標一致就宣稱相等。

可允許的原子前提只有以下兩類：

1. **直接性質前提** $P(i,c)$：在定義 $D_i$ 上，型別化命題 $c$ 經凍結的精確算術／調和核心驗證。
2. **定義等價前提** $E(i,j)$：在共同週期上證明 $f_i=f_j$，且二者具有相同的底層群與合法轉換範圍。

本版唯一能移轉命題的規則，是外延性質對相等對象的保留：

$$
E(i,j)\land P(i,c)\implies P(j,c).
$$

等價關係可以使用對稱及傳遞性，**但不能**跨越命題型別，更不能把相同總和當成相同函數。型別白名單承接凍結 v1.5：`global_sum_equals`、`fourier_zero`、`fourier_nonzero`、`wheel6_candidate`；若輸入來源或前提所需的版本、群、頻率或命題內容不一致，必須拒絕。`wheel6_candidate` 不等於質數判定。

給定有限候選前提庫 $A$，目標集合 $T$，以及上述閉包 $\mathrm{Cl}(S)$，我們定義**限定系統中的最小充分前提問題**：

$$
\mathrm{OPT}_{A}(T)=\min\{\lvert S\rvert:S\subseteq A,\ T\subseteq\mathrm{Cl}(S)\}.
$$

此處 $\lvert S\rvert$ 計數的是原子數學前提，不是推理步數、證書 JSON 位元組、原始資料量或 CPU 指令。若候選庫不存在充分集合，就回報 `NO_SUFFICIENT_PREMISE_SET_IN_CATALOGUE`，不能捏造最小性。

## 2. 一般候選庫的窮舉最小性核查

在明確限制的候選庫（不超過 16 個原子前提）內，可以依基數遞增枚舉子集。只有當一個集合確實支撐全部目標，且所有**嚴格更小**集合皆不充分，才有資格稱為候選庫內的基數最小。

本版讓生產端與驗證端使用不同的推理實作：

- 生產端以前向規則閉包判定哪些目標能被涵蓋，選出依固定字典序的第一組最小集合。
- 驗證端獨立計算等價圖的連通分量，用分量上的同型別事實覆蓋目標；其後逐一排除每一個更小子集，而不信任生產端提交的最小性標記。
- 驗證端逐一核查被宣稱的前提，以及逐目標的前提來源與等價路徑；對需要全域候選庫最小性的模式，**所有候選數學前提也會重新驗證**，而不是只檢查選出的前提。

若候選庫較大或輸入要求超出上限，本版不宣稱一般可解。一般最小支撐／集合覆蓋問題可能具有組合複雜性，不能把本版上限外的情況冒稱廉價驗證。

## 3. 簡短的結構式最小下界

以下定理是本版與之前「只做局部證書重用」最主要的不同。它是一個關於**限定證書語言**的組合引理，不是原創的普遍證明複雜度定律。

**命題 3.1（矩形目標的原子數下界）。** 設有 $d\ge1$ 個不同的定義位置，每個位置都要求同樣的 $k\ge1$ 類互不相同的型別化命題。准許的前提只有單一位置上的單一命題、或連接兩個定義的等價橋；准許的推理只有等價關係傳遞與同型別命題沿等價關係的轉移。任何足以證成全部 $dk$ 項目標的前提集合至少有

$$
\lvert S\rvert\ge d+k-1.
$$

**證明。** 取所選等價橋構成的無向圖，設其在全部 $d$ 個定義位置上有 $c$ 個連通分量。每個分量都包含至少一個定義位置，而每個位置需要全部 $k$ 個不同的命題型別。轉移規則只搬運同型別命題，不會生出新型別。因此每個分量至少需要 $k$ 個直接性質前提，總數至少 $kc$。由於 $d$ 個頂點形成 $c$ 個連通分量，所選的等價橋至少有 $d-c$ 條。合計至少 $kc+d-c=d+(k-1)c$ ；因 $c\ge1$ 且 $k\ge1$，得到 $d+k-1$。證畢。

$$
\lvert S\rvert\ge kc+(d-c)=d+(k-1)c\ge d+k-1.
$$

此引理**不要求**逐一列出所有可能的較小子集。若一份前提集恰好有 $d+k-1$ 個已驗證原子、每個目標都有可重播的推導路徑，便在上述語言中達到嚴格的基數下界。

**不可省略的適用條件：** 目標必須是全部 $d$ 個定義與同一組 $k$ 個命題類別的完整直積；前提必須都是一證一原子；不允許其他能一次推出多個命題的複合推理規則；跨域轉移必須使用已證明的**完整函數等價**，不能用數值恰巧相同代替。條件不成立時，此快捷核查必須回報不可適用，而非給予 PASS。

## 4. 實例：三種模環表示與九個調和／算術目標

在有限循環群 $G=\mathbb Z/600\mathbb Z$ 上，取模 6 基底向量

$$
(a_0,a_1,a_2,a_3,a_4,a_5)=(2,-1,4,0,3,0).
$$

讓定義 $A$ 直接重複此六項，定義 $B$ 以模 30 表示同一週期，定義 $D$ 以模 60 表示同一週期。三者是**完整指定的數學生成函數**，不是外部採集到的任意資料表。共同週期的數學核查可建立 $E(A,B)$ 及 $E(A,D)$。

每個定義各需三項命題：

1. 整數總和等於 $800$。
2. 第 $1$ 頻率的傅立葉係數等於零。
3. 第 $100$ 頻率的傅立葉係數非零。

在這個完整定義上，單一六項週期的和是 $8$，故 $600$ 點總和為 $800$ ；頻率 $1$ 在商群角色湮滅條件之外，因此係數精確為零；頻率 $100$ 對應六次單位根，在整係數循環多項式 $\Phi_6(X)=X^2-X+1$ 模下，週期多項式

$$
F(X)=2-X+4X^2+3X^4
$$

同餘於 $-2$，所以在 $600$ 點上對應的係數是 $-200$，明確非零（採用未規範化的離散傅立葉慣例）。全部檢查均使用整數與精確代數條件，不需浮點 FFT。

將三個 $A$ 的直接性質前提與 $E(A,B),E(A,D)$ 合併，只需五個原子便可推出三個定義上的全部九項目標。由命題 3.1 的 $d=3,k=3$，任何集合至少需要五個原子；五項方案確實充分，故達到下界。獨立窮舉核查另行排除 $794$ 個不足五項的候選庫子集。

同一套完整生成定義也在 $G=\mathbb Z/60000\mathbb Z$ 上重播：三類目標的頻率與總和按定義更新，最小充分前提仍是五個，而不是宣稱外部六萬筆資料已被免除完整來源認證。

## 5. 三種不同驗證強度

| 模式 | 數學前提檢查 | 最小性核查 | 可合法宣稱 |
| --- | ---: | --- | --- |
| `sufficient` | 所選 5 個 | 不執行 | 九項目標由五項已驗證前提支撐；**不宣稱最小** |
| `structural` | 所選 5 個 | 矩形目標下界 $d+k-1$ | 在限定規則語言中已達原子數最小 |
| `minimum` | 候選庫全部 12 個 | 窮舉所有嚴格較小子集（本例 794 組） | 在已釘選候選庫中達到基數最小 |

`structural` 的數學理由不是演算法的「捷徑猜測」，而是命題 3.1 的獨立組合下界。兩種最小性核查相互對照，但**即使同時通過，仍不構成一般形式邏輯的最短證明定理**。

## 6. 成本測量及負面結果

相同的 $G=\mathbb Z/600\mathbb Z$，Python 標準函式庫，同一程序內重複 49 次，取中位數；不含啟動、I/O、可信來源釘選的建立，實驗數值見 `examples/benchmark_v16.json`。

| 路徑 | 算術／等價原子核查數量 | 本次中位毫秒 |
| --- | ---: | ---: |
| 每項目標直接核查九項 | 9 | 0.130107 |
| 選出五項，僅驗充分性 | 5 | 0.474176 |
| 五項加結構式最小性下界 | 5 | 0.500206 |
| 候選庫最小性全窮舉 | 12，另排除 794 組 | 10.965444 |

結果顯示：**證明前提數的減少，不必然代表 Python 驗證程序立即加速。** 本版的小型案例中，解析計畫、指紋核對、型別驗證與等價橋的固定成本，反而使「五項已充分」耗時高於直接核查九項。因而本輪可以宣稱「限定語言中的前提數降低」，不能宣稱普遍減少端到端延遲。基準僅對本環境、目前小型資料與實作成立。

## 7. 信任、來源與安全界線

- 每個前提先以凍結 v1.5 精確核心重算；不接收由產生者自行填入的 `PASS` 作為事實。
- 產生端與驗證端的**組合推理算法**彼此獨立；底層群算術與循環多項式仍共享凍結 v1.5 數學核心，不能冒稱有兩套完全獨立的算術實作。
- 計畫與定義各自具 domain-separated SHA-256；驗證需要**外部給定**的預期指紋。演示檔 `PINS_*_DEMO_ONLY.json` 不具現實來源身分認證。
- JSON 禁止重複鍵、非有限數值與浮點混入；算術主張要求 exact integer 型別，防止布林值混成整數證書。
- 未選入的前提，在 `sufficient` 與 `structural` 模式下不重新驗證，因此輸出明確標示它們為未檢查；只有 `minimum` 模式會全部重算。
- 舊版定義的來源版本變動會改變外部釘選及計畫指紋；沒有有效的新證書就不可沿用 PASS。
- 本研究的完整生成定義等價，不等於任何外部原始 CSV、JSON、PDF 或真實世界資料確實等於它。外部來源仍需使用 v1.1–v1.2 的獨立來源核查義務。
- 本版沒有額外使用或驗證 TCGCT 主倉最新非公開原生進位核心，也沒有將 TCGQT 多尺度視覺表示升格為數論定理。保留的 v1.5 對象與結論是此版的數學邊界。

## 8. 可重播指令及結果狀態

使用 Python 3.10+，不需第三方 Python 套件：

```bash
python -B -m unittest discover -s tests -q
python -B scripts/build_examples.py --check
python -B scripts/verify_minimal.py --plan examples/PLAN_DEMO_ONLY.json --pins examples/PINS_DEMO_ONLY.json --certificate examples/CERTIFICATE_DEMO_ONLY.json --allow-demo --mode structural
python -B scripts/verify_minimal.py --plan examples/PLAN_DEMO_ONLY.json --pins examples/PINS_DEMO_ONLY.json --certificate examples/CERTIFICATE_DEMO_ONLY.json --allow-demo --mode minimum
python -B scripts/benchmark_v16.py --check
python -B scripts/verify_release.py
```

`--mode sufficient` 只能輸出 `global_minimality=NOT_CHECKED`；`--mode structural` 證明限定推理語言的最小原子數；`--mode minimum` 直接驗證候選庫的窮舉最小性。示範檔必須指定 `--allow-demo`；實務部署不能把同資料夾裡的示範指紋當作可信外部授權。

本版新增 64 項測試（實際執行驗收以 `docs/VALIDATION_v1.6.md` 的最終紀錄為準），包括錯誤等價、僅總和相同、型別不符、假證書、JSON 重複鍵、未授權指紋、窮舉最小性、矩形目標前提缺失、大型群範例，以及產生端／驗證端對隨機選取前提子集的一致性測試。

## 9. 從 v1.5 到 v1.6 的真正意義

這一階段開始把「少做數學驗證」拆成三個互不相同的命題：第一，存在一組足以支持目標的較少數量前提；第二，確實能證明這組前提在指定語言下已經是最少；第三，這種證書減量對於真實驗證延遲是否有淨收益。

本版建立了前兩者在一個明確有限且受限的例子中的證據，第三者目前**沒有**。這種區分是未來將結構壓縮用於更一般調和分析、算術幾何或其他領域之前必須保留的核查契約。

**結語：數學驗證可以不必重走每一條已走過的路；但哪一條路得以省略，本身也需要一個不依賴省略之後才成立的理由。**