← Archive
lm-005294 · 2026-11

TCGCT × TCGQT v0.6:有限交換群調和證書、跨程序核查與證明依賴圖

下載 MD 檔 ⬇
title
TCGCT × TCGQT v0.6:有限交換群調和證書、跨程序核查與證明依賴圖
english_title
Portable Proof-Carrying Harmonic Verification over Finite Abelian Groups
version
v0.6 / research draft
date
2026-11-02
author
Neo.K / EveMissLab
research_collaboration
GPT-6
status
EXACT_FINITE_SCOPE / EXECUTABLE_PROTOTYPE / NOT_BSD / NOT_FORMAL_PROOF_ASSISTANT
canonical_source
UTF-8 Markdown; canonical inline and display dollar delimiters

TCGCT × TCGQT v0.6:有限交換群調和證書、跨程序核查與證明依賴圖

作者: Neo.K / EveMissLab
機構: EveMissLab/一言諾科技有限公司
日期: 2026-11-02
版本: v0.6 / research draft
研究協作(原稿所載): GPT-6
原稿狀態: EXACT_FINITE_SCOPE / EXECUTABLE_PROTOTYPE / NOT_BSD / NOT_FORMAL_PROOF_ASSISTANT

摘要

本研究延續 v0.2 的精確纖維判定、v0.3 的有限交換群 Galois 軌道、v0.4 的有限向連續提升閘道及 v0.5 的同程序證明 DAG,將有限交換群的兩個子群纖維、四項正交分解和精確角色零判定接入同一個有型別證明依賴圖,並提供一種不信任外部 PASS、可在獨立程序重新核對的攜帶式數學見證。

此框架的關鍵不是宣稱傳統 BSD 猜想已有新解,而是研究:在不犧牲精確性、來源範圍與前提區分的情況下,能否避免跨程序重新生成部分昂貴的數學證書,改為核驗較簡潔的代數恆等式。以下定理均屬經典有限群/調和分析結果;本版的貢獻為可重播的證書合成、拒絕條件及工程化驗證對照。

1. 目標、來源與嚴格的非主張

工作鏈為:TCGCT 精確數學正本 → TCGQT 多尺度、子群與觀察鏡頭 → 調和分析零頻率與交互作用 → 帶來源、版本及獨立可核查見證的 DAG。這裡的「驗證更快」是減少合法重複核查工作,不是提高算術的指令吞吐量。

本稿不主張:已證明任意 BSD;精確有限群結論可直接提升至無限/連續群;表示進位不同會改變既有整數的質數性;雜湊等於來源認證;單一算例的時間比率對所有機器成立;Python 原型本身是形式化定理證明器。

保留的來源:v0.5(凍結)、v0.4、v0.3、v0.2,均在 upstream_v05/ 內。v0.6 將其運算圖的 schema 另升至 0.6,不覆寫前代官方原始碼。

2. 有限交換群的兩層纖維平均

定義有限交換群

G=∏i=1rZ/niZG=\prod_{i=1}^{r}\mathbb{Z}/n_i\mathbb{Z}

與子群 H1,H2≤GH_1,H_2\leq G,其中 f:G→Qf:G\to\mathbb{Q}。每個子群的纖維平均為

(PHf)(x)=1∣H∣∑h∈Hf(x+h).(P_Hf)(x)=\frac{1}{|H|}\sum_{h\in H}f(x+h).

由於群律交換,平移平均可重排成同一個 H1+H2H_1+H_2 子群的平均:

PH1PH2=PH2PH1=PH1+H2.P_{H_1}P_{H_2}=P_{H_2}P_{H_1}=P_{H_1+H_2}.

令 P1=PH1P_1=P_{H_1} 、 P2=PH2P_2=P_{H_2} 、 II 為恆等算子。則

f=f00+f01+f10+f11f=f_{00}+f_{01}+f_{10}+f_{11}

其中

f00=P1P2f,f01=(I−P1)P2f,f10=P1(I−P2)f,f11=(I−P1)(I−P2)f.\begin{aligned} f_{00}&=P_1P_2f,\\ f_{01}&=(I-P_1)P_2f,\\ f_{10}&=P_1(I-P_2)f,\\ f_{11}&=(I-P_1)(I-P_2)f. \end{aligned}

定理 A(正交與能量守恆)。 在實數內積 ⟨f,g⟩=∑x∈Gf(x)g(x)\langle f,g\rangle=\sum_{x\in G}f(x)g(x) 下, P1,P2P_1,P_2 是互相交換的自伴冪等算子。故以上四個部分兩兩正交,且

∑x∈Gf(x)2=∑a,b∈{0,1}∑x∈Gfab(x)2.\sum_{x\in G}f(x)^2=\sum_{a,b\in\{0,1\}}\sum_{x\in G}f_{ab}(x)^2.

證明概要。 平移 x↦x+hx\mapsto x+h 是有限集合的置換,故 PHP_H 自伴;子群平均兩次等於平均一次,故冪等。相互交換的兩個正交投影共同分解成四個互斥投影,其交叉內積為零。整數輸入時每個輸出值都屬有理數,無需浮點捨入。

本原型在 src/finite_abelian.py 計算有限群、生成子群、纖維平均與能量分解;src/portable_checker.py 則採獨立的索引與加法實作,從原始輸入重新計算並比較全部四項見證,不採用生產者的判定函式。

3. 子群消去、角色掩碼與軌道

對角色 χ∈G^\chi\in\widehat G,定義傅立葉係數為 f^(χ)=∑x∈Gf(x)χ(x)‾\widehat f(\chi)=\sum_{x\in G}f(x)\overline{\chi(x)}。子群平均的頻域作用為

PHf^(χ)={f^(χ),χ(h)=1 對所有 h∈H,0,其他.\widehat{P_Hf}(\chi)=\begin{cases} \widehat f(\chi),&\chi(h)=1\ \text{對所有}\ h\in H,\\ 0,&\text{其他}. \end{cases}

因此四個部分的支持域由 H1⊥H_1^\perp 、 H2⊥H_2^\perp 的交集與補集完全決定。這個結構消失與輸入訊號的偶然相消不可混淆:前者不需要計算每個係數,後者仍需要代數見證。

設 L=lcm⁡(n1,…,nr)L=\operatorname{lcm}(n_1,\ldots,n_r),選定原始 LL 次單位根 ζL\zeta_L。對角色索引 k=(k1,…,kr)k=(k_1,\ldots,k_r),把頻譜計算整理成整係數多項式

Ak(X)=∑x∈Gf(x)Xe(k,x),e(k,x)≡−L∑ikixini(modL).A_k(X)=\sum_{x\in G}f(x)X^{e(k,x)}, \qquad e(k,x)\equiv-L\sum_i\frac{k_ix_i}{n_i}\pmod L.

若 ff 為整數訊號,則

f^(k)=Ak(ζL),f^(k)=0  ⟺  ΦL(X)∣Ak(X).\widehat f(k)=A_k(\zeta_L),\qquad \widehat f(k)=0\iff\Phi_L(X)\mid A_k(X).

其中 ΦL\Phi_L 是第 LL 個循環多項式。第二個等價由原始 LL 次單位根在 Q\mathbb Q 上的最小多項式性質得到。

定理 B(Galois 軌道)。 對 u∈(Z/LZ)×u\in(\mathbb Z/L\mathbb Z)^\times,映射 k↦ukk\mapsto uk 對應 Galois 作用。頻譜零與非零性在這個軌道內一致;但是相同角色階數不保證屬於同一軌道。因此只能合法按軌道合併精確零判定,不能只按階數合併。

一個直接的反例在 G=Z/6×Z/10G=\mathbb Z/6\times\mathbb Z/10:取 f(x,y)=1f(x,y)=1 若 x=0x=0,否則為零。角色 (3,0)(3,0) 與 (0,5)(0,5) 同為 2 階,但其 Fourier 係數分別為 1010 與 00。同階合併法會錯誤地宣稱兩者相同。

4. 攜帶式見證:讓新程序檢查,而不是信任

本版建立兩種攜帶式見證:

  1. 四分量 f00,f01,f10,f11f_{00},f_{01},f_{10},f_{11} 的全長精確有理數陣列。核查者由來源函數、群律與生成元獨立構造 H1,H2H_1,H_2,逐格計算平均與重建,驗算正交與能量。每個分數都要求最簡正規字串,不可偷換為浮點近似。
  2. 每個 Galois 軌道的多項式除法證書 Qk,RkQ_k,R_k,核查者重建 AkA_k 與 ΦL\Phi_L,然後逐係數驗證
Ak(X)=ΦL(X)Qk(X)+Rk(X),deg⁡Rk<deg⁡ΦL.A_k(X)=\Phi_L(X)Q_k(X)+R_k(X),\qquad\deg R_k<\deg\Phi_L.

於是 Rk=0R_k=0 當且僅當該角色在特徵零下的係數精確為零。新的驗證程序只需要逐項乘法與等式檢查,不需要重新執行原生產者的多項式長除。驗證器同時獨立重建 Galois 軌道、角色遮罩與來源訊號;不能依賴傳入的 PASS 字串。

這個證書不是密碼學簽章;來源驗收必須由包外提供 expected claim-graph SHA-256。將同一 ZIP 裡面寫的雜湊作為自己驗證自己的權威,是本版明確禁止的信任擴張。若來源身分、數學來源的真實性、驗證器程式碼供應鏈或外部證明系統出現問題,這個包不能自行補足。

設計上的差別:驗證一份可重用數學證書不等於「完全不用算」,而是只做足以確認結果的檢查工作。新 verifier 仍須檢查原始輸入、結構、型別、全部生成子群及每個必需的多項式恆等式。

5. 同一張 DAG 的結合、失效與重用

v0.6 允許下列型別節點與 v0.5 舊節點共存:

  • source/abelian_integer_signal:完整有界訊號、模數維度、來源 ID 和 revision。
  • proof/abelian_four:兩組生成元、四分量精確分解。
  • proof/abelian_orbits:子群遮罩與 Galois 軌道精確角色驗證。
  • proof/all_of:與舊有有限群、分段線性連續證書共同組成合取;任何未完成、否證或無法驗證的前提均不得暗中升格。

依賴圖的來源雜湊包含型別、算子、參數和上游節點的雜湊。只有在同一程序已實際驗證過且來源不變時,才重用無需再驗的記憶體快取。外部冷啟動時走另一條入口:僅對攜帶式 Abelian 見證使用獨立 portable_checker.py 重驗;其餘舊類型仍要重新核查,不會自動把記憶體快取升格成跨程序可信快取。

在本版示範的 15 節點合取目標中,初次核查 15 個、相同快照重複核查 0 個。只修改 Abelian 訊號一格且明示 revision 後,核查 4 個、重用 11 個。只修改舊有理折線時,舊路線的結論可能轉為 UNRESOLVED,不可因新 Abelian 路線 PASS 就把合取提升。

6. 實驗與實際數值

6.1 非循環群 Z/6×Z/10\mathbb Z/6\times\mathbb Z/10

訊號定義為

f(a,b)=[a=0]+[b=0]+[(a,b)=(1,3)],f(a,b)=[a=0]+[b=0]+[(a,b)=(1,3)],

其中方括號是 0/1 指示值。60 格數值平方總和為 19;兩個子群由 (1,0)(1,0) 與 (0,1)(0,1) 各自生成,總和是整個群。

分量 精確平方能量 對應角色數
common 289/60 1
h1_only 107/20 9
h2_only 97/12 5
interaction 3/4 45
合計 19 60

原型將 60 個角色分為 16 個 Galois 軌道;角色的階數只分成 8 類。每個軌道的多項式商/餘式在全新核查程式中逐係數驗證。本例 16 個軌道均非零,與第 3 節的只依一個座標之反例不同,避免誤把「某些結構分量被消去」說成原訊號的所有角色都為零。

6.2 210 點 CRT 質數快照

G=Z/2×Z/3×Z/5×Z/7G=\mathbb Z/2\times\mathbb Z/3\times\mathbb Z/5\times\mathbb Z/7 的 CRT 編碼在 0≤n<2100\le n<210 下有 46 個質數,平方能量為 46。此實驗獨立量測子群平均、四分量重建及 16 個 Galois 軌道。這是有限快照,不是質數分布無限定理;CRT 坐標是數論與表示的已知變換。

6.3 Cold process 對照基準

examples/benchmark_v06.json 保存每條路徑在全新 Python 子程序重複 7 次的實測原始數值。每輪比較「由來源重新產生整個證書」與「獨立核查來源加既有商/餘式見證」。測得:

案例 生產者內部時間中位數 核查者內部時間中位數 生產者/核查者
非循環 60 點 34.9268 ms 9.8780 ms 3.5358
CRT 210 點 50.6570 ms 22.9850 ms 2.2039

限制: 單一容器的一次性有限樣本,無信賴區間,且兩條路徑不是同一演算法;核查路徑還需要收到事先產生的證書。加入 Python 啟動與 I/O 後,60 點兩路徑分別為約 792.0 與 762.2 ms,210 點則為約 793.7 與 806.4 ms,並未展示穩健的端到端加速。上表是特定工作負載的實際驗證成本實驗,不得解讀成普適速度優勢或證明複雜度結果。冷驗證做了數學核對,而不是略過核對。

7. 故障注入與驗證邊界

測試包含:竄改來源版本、來源內容、子群生成元、四分量任一分數、商式、餘式、軌道的省略或重排、臆造 PASS、來源數值改動而外部釘選未改、重新計算另一個包內雜湊試圖取代外部釘選、超過有界模數與群大小、試圖把非法群座標寫進算子等。

這些必須被拒絕,而非視為通過。另一個反例是有限群上相同角色階數不同零性;測試以完全獨立的初等訊號驗證這件事。有限域模一個質數算得 0 的情況仍然不被自動提升成特徵零下零值。

已知程式限制:Python 的數學實作本身未經 Lean/Coq 形式化;每個新組合群的群階至多 240,最多四個循環因子,每個分量數值限制在 256-bit,沒有任意精度解析函數、p-adic、無窮群或受信任作者簽章。無法驗證時拒絕,不以猜測填補。

8. 下一研究義務

  1. 將獨立核查進一步縮小到部分纖維/選定頻率,讓可攜見證不用攜帶全長四分量矩陣。
  2. 在來源變動後,構造受限增量見證,不只減少記憶體中的重算,也減少冷程序核查的重複子圖。
  3. 為連續分析尾項建立精確、可攜帶、可獨立核查的解析上界見證,避免把 bandlimited 假設當成來源數據自行推斷。
  4. 固定外部 trust root、版本協議與多程序可驗收的供應鏈,避免把來源雜湊與來源簽名混淆。
  5. 若要觀察 BSD,只能把本框架當作驗證技術候選,必須另行證明任何從有限表象通往複解析、代數 regulator 或 pp -adic 特徵零命題的橋接。

9. 重播方式

從本交付根目錄:

python -B scripts/build_examples.py --check
python -B -m unittest discover -s tests -v
python -B scripts/verify_release.py

兩個真正不同程序使用的命令:

python -B scripts/portable_cli.py produce --graph examples/graph_v06.json --target abelian_orbits --out packet.json
python -B scripts/portable_cli.py verify --packet packet.json --expected-pin YOUR_TRUSTED_EXTERNAL_CLAIM_DIGEST

examples/experiment_v06.json 所附的 pin 僅供展示格式,不是可信外部錨點;使用者必須從獨立、可信的路徑取得 expected digest。數學 source、證書及證據完整,不代表來源作者身份已認證。


研究結論: 在受限的有限交換群整數訊號上,精確纖維四分解與 Galois 軌道零判定可以組成同一張證明 DAG;跨程序可由獨立重算的結構前提 + 多項式商餘式驗證重建結論,而非相信外部傳來的 PASS。特定實驗中內部驗證工作量下降,但端到端性能、一般化解析橋接與 BSD 仍是開放事項。