title: TCGCT × TCGQT：成本感知充分前提、結構式最優下界與跨版本驗證負擔
english_title: TCGCT–TCGQT v1.7: Cost-Aware Sufficient Premises and Structure-Gated Optimality Certificates
author: Neo.K / EveMissLab
research_collaboration: GPT-6
date: 2026-11-03
version: v1.7
status: FINITE RESEARCH PROTOTYPE / NOT A BSD PROOF / NO UNIVERSAL SPEEDUP
canonical_source: UTF-8 Markdown; inline math $...$ ; display math $$...$$
upstream: bit-identical v1.6 ZIP with 559 files, stored under upstream_v16/

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

摘要

此研究延續 v1.6 的「最小充分前提集」與 v1.5 的型別化跨表示橋接，進一步問：前提數最少，是否意味著實際的數學驗證工作也最少？ 我們把數學真值、證明充分性、前提驗證成本、命題轉移成本，以及已驗證基線的重用狀態，整理為有限且可獨立核查的問題。目標不是改變 BSD 猜想的真值，不是減少無條件的數學公理，也不是加速底層數值計算，而是針對明確的推理系統，選擇驗證負擔較低的充分證書。

在一個由三種模環表示、九項數論／有限調和命題及十二個候選原子構成的例子中，設定直接性質的冷核查成本為 $6$ 、跨表示等價橋的冷成本為 $17$ 、一次命題跨橋轉移為 $1$ 個模型工作單位。冷模式的成本最優方案不是基數最小的五項共享證書，而是九項直接證書，成本為 $54$ 。若三項根部直接證書與兩條等價橋已在同一程序中核查並保留，則暖模式的成本最優方案改成五項共享證書，後續成本為 $11$ 。這兩個最優解皆經獨立的 $2^{12}=4096$ 子集枚舉重新證實，並以各自適用條件嚴格限定的結構下界再次證實。

重要反向結果： 這些成本單位不是毫秒。Python 實測中，充分性檢查的端點並未一致因工作單位下降而縮短；再做一次一般最優性窮舉更可能遠貴於直接核查目標。結構式下界在其狹義適用域內，才明顯降低了最優性審計本身的負擔。

1. 接續來源與研究範圍

本版凍結承接的依賴包括：

v1.5 的完整有限群生成定義、跨表示精確等價與有型別命題白名單；
v1.6 的十二項原子候選、九項矩形目標與兩套獨立的基數最小性驗證；
v1.6 的 SHA-256 原始封裝，完整保留在 upstream_v16/，不更動原始代碼或舊結論。

目前只接受完整定義的有限群整數函數，推理規則限定為等價關係的對稱／傳遞，以及完全相同型別與參數的外延命題沿已驗證的完整函數等價橋轉移。本版不新增任何可以根據數值相似度、相同總和或視覺拓樸外觀自行推出函數等價的規則。

同樣地，此處的 TCGCT × TCGQT 是研究系譜及驗證接口名稱，沒有聲稱本版修改、驗證或重寫兩個獨立上游 GitHub 專案的完整數學核心。

2. 成本函數與可核查目標

設 $D$ 為有限數學定義集合， $A$ 為已明確列出的型別化前提候選， $T$ 為所要建立的目標命題集合。前提類型只有：

$P(i,c)$ ：定義位置 $i$ 上的命題 $c$ ，需要精確數學核查；
$E(i,j)$ ：兩份已定義函數在同一有限群上的完整外延等價，亦需精確核查。

給定被選入的候選集合 $S\subseteq A$ ，以及對每個目標 $g\in T$ 的轉移路徑 $\pi_g$ ，定義預估工作單位：

C_m(S,\pi)=\sum_{a\in S}c_m(a)+\sum_{g\in T}\sum_{e\in\pi_g}\tau(e).

其中 $m$ 為 cold 或 warm 模式， $c_m(a)$ 是釘選成本表中的正整數， $\tau(e)$ 為等價橋每被一項目標使用一次的非負整數轉移費。每個目標必須有一個直接真值前提及一條有型別的等價路徑；如果無此路徑，該 $S$ 不充分。費用模型特意保留「建立等價橋」與「利用等價橋轉移不同命題」的區別，避免把一次核查和無限次免費使用混同。

此成本不是物理計算複雜度下界，也不是任何系統的實際延遲。它是一個可反證的決策模型，其來源必須由使用者、可信管理者或獨立成本測量系統給定。輸入文件僅有自算的雜湊不能證明成本權重可信。

限定候選庫中的成本最優值定義為：

C_m^* = \min_{S\subseteq A}\ \min_{\pi\text{ 能證成 }T}\ C_m(S,\pi).

成本最優與基數最小不同，因為 $\arg\min |S|$ 一般不等於 $\arg\min C_m(S,\pi)$ 。對固定 $S$ ，各目標使用最低費用的合法等價路徑。本文產生端使用 Dijkstra 型路徑搜尋，驗證端則使用 Floyd–Warshall 路徑矩陣與獨立子集枚舉，不將產生端的最優宣告當成證據。

3. 冷驗證與暖驗證的信任差異

冷模式每次都重新核查被選的數學前提；成本表使用 cold 權重。暖模式只能使用由當前程序在當前來源與成本政策下實際核查過的前提，才能以 warm 權重建立後續決策。暖狀態是程序內短暫、不可由 JSON 直接反序列化的物件；新程序一律必須重新核查基線後才能產生暖狀態。

因此，暖模式的 $11$ 個單位不包含初始化已驗證基線的成本。這不是省略前提的首次驗證，而是針對同一個已驗證基線可能連續承擔多次驗證任務的攤銷模型。任何來源或成本表版本變動，都會使舊暖狀態無效；任何外部提供的 PASS 字樣、JSON 收據或 SHA-256，不能自動成為程序內的已核查狀態。

Python 程序本身不能對有相同執行權限的惡意程式碼提供硬體級不變狀態保證；要將其部署為外部服務，仍需程序隔離、正式權威金鑰、授權與防回滾機制。本版未宣稱提供那些能力。

4. 實例：三種模環表示、九項命題

沿用 v1.6，在 $G=\mathbb Z/600\mathbb Z$ 上定義六項週期向量：

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

將它分別寫成模 $6$ 、模 $30$ 、模 $60$ 的完整生成式，定義位置以 $A,B,D$ 區分；三者在共同週期上代表相同的整數函數。每個位置要求三類型別化命題：總和恰為 $800$ 、頻率 $1$ 的係數為零、頻率 $100$ 的係數非零。這九項目標並非九個互不相干的猜想，而是同一個已完整指定的函數在不同表示下的三類外延性質。

候選庫中有九個直接性質前提和三條等價橋 $E(A,B),E(A,D),E(B,D)$ ，合計十二項。v1.6 在此例已證得基數最小為五項。

4.1 成本政策

本版設定一個有意區分冷／暖驗證的示範成本模型：

費用類型	冷模式	已核查且允許重用的暖模式
每個直接性質原子	6	1
每條跨表示等價原子	17	1
每個目標每次使用一條等價橋	1	1

暖模式中，只有 $A$ 上的三個直接性質及 $E(A,B),E(A,D)$ 五項已完成基線核查；其餘未在暖基線中的候選仍依冷費用計算。因此，表中的 warm=1 並非宣稱所有候選都已免費暖化。

4.2 結果

冷模式直接驗證九項性質，各需 $6$ ，總費用 $54$ 。相比之下，先驗證 $A$ 的三項性質、兩條等價橋，再向 $B,D$ 轉移六項命題的五前提方案，冷費用為 $3\cdot6+2\cdot17+6\cdot1=58$ ，比九項直接方案貴。

暖模式則反轉：五項已核查基線各計一單位重用工作，向另外兩種表示轉移六項命題再計六單位，總費用 $5+6=11$ 。這裡的「重用成本」是政策估計，不宣稱每個已核查原子在真實系統恰好要花同樣的 CPU 時間。

判準	冷驗證	暖模式（先有核查基線）
最佳前提個數	9	5
預估工作單位	54	11
已驗證基線預先核查	不適用	5 項，成本另計
成本最優核查	4096 子集窮舉 PASS	4096 子集窮舉 PASS
特化結構下界	54	11

4.3 冷模式的短下界

命題 4.1（固定冷成本下界）。 在上列限定前提語言與冷費用中，證成全部九項目標至少需要 $54$ 個工作單位。

證明。 以選入的等價橋形成三個定義位置上的圖，將其分成 $c$ 個連通分量。考慮任一大小為 $s$ 的分量。對每一類命題，若選入 $t\ge1$ 個不同位置上的直接性質前提，需花費 $6t$ ；其餘 $s-t$ 個位置至少各有一次跨橋轉移，每次至少一單位，故每類命題至少費 $6t+(s-t)\ge s+5$ 。三類命題至少費 $3s+15$ 。連接該分量至少需要 $s-1$ 條已核查等價橋，費用至少 $17(s-1)$ 。合計每個分量至少為 $20s-2$ 。對三個位置求和：

C_{\mathrm{cold}}\ge\sum_{i=1}^{c}(20s_i-2)=60-2c\ge54,

因 $c\le3$ 。九項直接前提恰以 $54$ 單位完成全部目標，所以下界可達，證畢。

本引理的短證書不要求遍歷 $4096$ 個候選子集，但只適用於已核查的 3×3 矩形目標、候選格子、均勻冷成本與每跨橋一單位。若任何條件不同，實作不給此結構捷徑 PASS。

4.4 暖模式的短下界

命題 4.2（指定星狀已驗證基線下界）。 在暖狀態恰好為 $A$ 的三項直接前提與兩條等價橋 $E(A,B),E(A,D)$ 、其餘候選依冷費用計價的情況下，證成全部九項目標至少需 $11$ 個後續工作單位。

證明。 若選入的等價橋圖連通，三個定義位置至少需要兩條等價橋，費用各不低於一單位。對三類命題各三個目標，共九個目標；每個目標至少需要一個在該位置直接核查的性質原子，或一次跨橋轉移。每個直接原子費用至少一單位，每次轉移也至少一單位，且不同型別或位置的目標不能共用一次直接局部核查，故性質與轉移總費用至少九單位。加上兩條等價橋，得到至少十一單位。

若等價橋圖不連通，至少存在一個不含 $A$ 的分量，涵蓋該分量的三種命題型別各需要至少一個未預驗證的直接前提，各至少六單位，僅此已達十八單位，大於十一。因此總下界仍為十一。已暖化的五項星狀方案以 $3+2+6=11$ 單位達到此下界，證畢。

以上的第二種短證書也不是一般性組合最佳化的免費解。實作會先驗證目標矩形性、候選庫完整性、三種原子成本、轉移費率，以及暖狀態是否恰為指定星狀前提；任何假設改動，必須回到較一般的窮舉法或只報充分性。

5. 三種合法驗證模式

模式	核查內容	允許宣稱
`sufficient`	所選數學原子、型別化證書路徑、來源／成本釘選與實際費用加總	指定九項目標由該前提集合支撐；不宣稱成本最優
`structural`	`sufficient` 加上 3×3 目標與固定費用、暖態條件的結構下界	在特定費用模型下，所選方案達到可核查的全域下界
`optimal`	全候選數學原子、獨立 Floyd–Warshall 路徑成本、全部 $4096$ 個子集	在本候選庫、費用模型與規則語言中成本最優

不同模式不能合併成一個模糊的 PASS。尤其 sufficient 模式即使接受一份非最優但合法的五項冷證書，也會明確回報 cost_optimality=NOT_CHECKED。只有後兩種模式才可使用各自的適用範圍聲稱成本最優。

對抗反例： 當冷模式提交五項共享證書、誠實填報費用 $58$ 時，充分性驗證應當通過，但成本最優性驗證必須拒絕，因為九項直接證書只需 $54$ 。若有人把費用從 $58$ 改填為 $11$ ，即使重新計算其 JSON 自身雜湊，精確費用核查仍必須拒絕。

6. 來源、身份與可信基線

成本政策使用與 v1.6 計畫不同的 domain-separated SHA-256，兩者各自以外部預期釘選核對。成本表不能未經授權自行漂移。
所有型別、數學定義與精確性判定由完整保留的 v1.6→v1.5 核心重算，未提交或未驗證候選不會因產生器宣稱便成為真值。
產生端先檢查候選前提，再搜尋最低成本選擇；驗證端不呼叫產生端的路徑／最小化函式，獨立重算充分性、費用與有限域內的最優性。
在 sufficient 模式中，未選入的候選數學前提不需要全部重算，因此不得聲稱它們的真值都已重新檢查。
暖狀態在單一程序內由精確數學核查產生，不能從外部 warm=true、字串 PASS 或儲存的 JSON 直接恢復；冷程序對暖模式需先付出建立基線的成本。
DEMO_ONLY 釘選必須明示啟用；同封裝的示範釘選不構成真實金鑰授權、來源作者身份或現實資料真實性。
若有不完整資料、不同來源版本、型別不符、非法轉移路徑、偽造工作單位或缺少外部釘選，必須拒絕；不能為了達到預期的成本數字而降低驗證條件。

7. 計算、成本模型與實測的區分

examples/benchmark_v17.json 記錄 Python 單程序的中位耗時；其中暖模式的主核查不包含初始化基線費用，該費用另行量測。資料皆使用示範 600 點對象，沒有經過外部服務、網路延遲或硬體隔離。此處只報告本次有資料支持的方向：

冷成本模型選擇九項直接證書（54 單位），暖成本模型選擇五項共享證書（11 單位），均經數學核查。
小型 Python 核查實測不保證暖方案比冷方案短，因為計畫解析、型別轉移、來源釘選與已驗證狀態管理仍有固定開銷。
每次要求最優性窮舉，須負擔額外 $4096$ 子集審計；狹義結構下界可以在相同結論強度下以較少的核查工作代替它。
成本表是受限任務下的選擇指標；預估與實測不同並不是可以刪去誤差的理由，而是需要更新成本模型版本、在新版本重新驗證的證據。

未來要宣稱大規模驗證加速，還必須把實際來源成本、冷啟動、成本表建立與維護、記憶體、外部信任，以及重驗風險全部納入端到端測試。不能只比較短證書的 JSON bytes 或數學原子數量。

8. 可重播實作與驗證契約

Python 3.10+，精確數學核心使用標準函式庫。封裝為單一 ZIP，舊版 v1.6 原始 559 個檔案以位元組相同的方式保留，並另有 SHA-256 清單可核對。

python -B -m unittest discover -s tests -q
python -B scripts/build_examples.py --check
python -B scripts/benchmark_v17.py --check
python -B scripts/verify_cost.py --plan examples/plan.json --cost-policy examples/cost_policy.json --pins examples/external_pins_DEMO_ONLY.json --certificate examples/cost_certificate_cold.json --allow-demo --mode cold --check optimal
python -B scripts/verify_cost.py --plan examples/plan.json --cost-policy examples/cost_policy.json --pins examples/external_pins_DEMO_ONLY.json --certificate examples/cost_certificate_warm_DEMO_ONLY.json --allow-demo --mode warm --warm-ids a_sum,a_zero,a_nonzero,eq_ab,eq_ad --check optimal
python -B scripts/verify_release.py --full-tests

最後一個 verify_release.py 為唯讀驗收，不修改雜湊清單或重新產生數學證書。若重新整理範例或效能數字，必須明示更新檔案及生成新清單，不把舊版簽名視為自動繼承。

9. 本輪主張登記與界線

已由本版實作與測試支持： 有限候選庫中的成本相依充分性驗證、型別化跨域前提核查、冷／暖基線下不同成本最優方案、完整有限子集最優性審計，以及固定費率下可取代窮舉的結構式成本下界。

未由本版驗證： 對無限制數學命題的最短證明；通用調和分析證書壓縮率；真實第三方資料的來源身份；人類／AI 推理所需 Token 的普遍降低；不同硬體的端到端加速；BSD 猜想或任何其高秩缺口的解決。

結語：最少的前提不是最少的工作；唯有把前提、來源、轉移與驗證條件一起算進來，省下的證據才能不靠未付出的證據來成立。

TCGCT × TCGQT：成本感知充分前提、結構式最優下界與跨版本驗證負擔

摘要