- 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. 有限交換群的兩層纖維平均
定義有限交換群
與子群 ,其中 。每個子群的纖維平均為
由於群律交換,平移平均可重排成同一個 子群的平均:
令 、 、 為恆等算子。則
其中
定理 A(正交與能量守恆)。 在實數內積 下, 是互相交換的自伴冪等算子。故以上四個部分兩兩正交,且
證明概要。 平移 是有限集合的置換,故 自伴;子群平均兩次等於平均一次,故冪等。相互交換的兩個正交投影共同分解成四個互斥投影,其交叉內積為零。整數輸入時每個輸出值都屬有理數,無需浮點捨入。
本原型在 src/finite_abelian.py 計算有限群、生成子群、纖維平均與能量分解;src/portable_checker.py 則採獨立的索引與加法實作,從原始輸入重新計算並比較全部四項見證,不採用生產者的判定函式。
3. 子群消去、角色掩碼與軌道
對角色 ,定義傅立葉係數為 。子群平均的頻域作用為
因此四個部分的支持域由 、 的交集與補集完全決定。這個結構消失與輸入訊號的偶然相消不可混淆:前者不需要計算每個係數,後者仍需要代數見證。
設 ,選定原始 次單位根 。對角色索引 ,把頻譜計算整理成整係數多項式
若 為整數訊號,則
其中 是第 個循環多項式。第二個等價由原始 次單位根在 上的最小多項式性質得到。
定理 B(Galois 軌道)。 對 ,映射 對應 Galois 作用。頻譜零與非零性在這個軌道內一致;但是相同角色階數不保證屬於同一軌道。因此只能合法按軌道合併精確零判定,不能只按階數合併。
一個直接的反例在 :取 若 ,否則為零。角色 與 同為 2 階,但其 Fourier 係數分別為 與 。同階合併法會錯誤地宣稱兩者相同。
4. 攜帶式見證:讓新程序檢查,而不是信任
本版建立兩種攜帶式見證:
- 四分量 的全長精確有理數陣列。核查者由來源函數、群律與生成元獨立構造 ,逐格計算平均與重建,驗算正交與能量。每個分數都要求最簡正規字串,不可偷換為浮點近似。
- 每個 Galois 軌道的多項式除法證書 ,核查者重建 與 ,然後逐係數驗證
於是 當且僅當該角色在特徵零下的係數精確為零。新的驗證程序只需要逐項乘法與等式檢查,不需要重新執行原生產者的多項式長除。驗證器同時獨立重建 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 非循環群
訊號定義為
其中方括號是 0/1 指示值。60 格數值平方總和為 19;兩個子群由 與 各自生成,總和是整個群。
| 分量 | 精確平方能量 | 對應角色數 |
|---|---|---|
| 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 質數快照
的 CRT 編碼在 下有 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. 下一研究義務
- 將獨立核查進一步縮小到部分纖維/選定頻率,讓可攜見證不用攜帶全長四分量矩陣。
- 在來源變動後,構造受限增量見證,不只減少記憶體中的重算,也減少冷程序核查的重複子圖。
- 為連續分析尾項建立精確、可攜帶、可獨立核查的解析上界見證,避免把
bandlimited假設當成來源數據自行推斷。 - 固定外部 trust root、版本協議與多程序可驗收的供應鏈,避免把來源雜湊與來源簽名混淆。
- 若要觀察 BSD,只能把本框架當作驗證技術候選,必須另行證明任何從有限表象通往複解析、代數 regulator 或 -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 仍是開放事項。