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$ 上外延相同。此事實必須經精確數學核查，不能只因名稱、總和或統計指標一致就宣稱相等。

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

直接性質前提 $P(i,c)$ ：在定義 $D_i$ 上，型別化命題 $c$ 經凍結的精確算術／調和核心驗證。
定義等價前提 $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)$ 。

每個定義各需三項命題：

整數總和等於 $800$ 。
第 $1$ 頻率的傅立葉係數等於零。
第 $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 套件：

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 的真正意義

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

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

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

TCGCT × TCGQT：型別化最小充分前提集、結構式下界與調和命題證書

摘要