title: 進位制塔樓有限界域研究 III：FELRA 有限精確運算覆蓋證書、雙重窮盡核查與計算正確性優先
english_title: Radix Tower Finite-Boundary Study III: FELRA Finite Exact Computation Coverage Certificates, Dual Exhaustion Audits, and Computation-First Verification
research_id: RT-FBE-03 / FELRA-FBC-01
version: v0.1
date: 2026-11-05
author: Neo.K（有限界域窮盡及計算正確性優先研究構想）／GPT-6（證書契約、條件性命題、有限演算法、反例與原稿）
affiliation: EveMissLab／一言諾科技有限公司
status: FINITE EXACT CERTIFICATE PROTOTYPE; INDEPENDENT DUAL ENUMERATION; NOT MERGED INTO FELRA; NOT LEAN VERIFIED
predecessors: RT-FBE-01 v0.1; RT-FBE-02 v0.1; Radix Tower Paper XII; FELRA computation-first design v0.1
source_archive_sha256: 72f844cde3df43913eb01b577dfd7ba5fcb4fc92cc6412ba22a890fc1e212059
canonical_source: UTF-8 / LF / no BOM; math delimiters only $...$ and $$...$$
peer_review: NOT PEER REVIEWED

進位制塔樓有限界域研究 III

FELRA 有限精確運算覆蓋證書、雙重窮盡核查與計算正確性優先

RT-FBE-03 / FELRA-FBC-01 · v0.1 · 2026-11-05

研究命題。 「每筆已列出的計算都算對」與「指定有限界域中的全部合法對象均已列出」是不同證明義務。若數學 AI 要優先保證計算正確性，FELRA 必須分別審計每個運算見證、完整窮盡的集合邊界、界域語義以及證據的來源釘選，而不能允許 COUNT_MATCH、HASH_MATCH 或某個觀察圖像直接升格為 EXHAUSTIVE_VERIFIED。

證據分類： [DEF] 工作定義；[PROP] 明確前提下的數學結果；[PROOF] 推導；[EXACT] 已執行的有限整數核查；[COUNTER] 精確反例；[ENGINEERING] 參考程式及接口；[LIMIT] 未建立的結論。

作者： Neo.K（有限界域窮盡及計算正確性優先研究構想）／GPT-6（證書契約、條件性命題、有限演算法、反例與原稿）
機構： EveMissLab／一言諾科技有限公司
日期： 2026-11-05
版本： v0.1
原稿狀態： FINITE EXACT CERTIFICATE PROTOTYPE; INDEPENDENT DUAL ENUMERATION; NOT MERGED INTO FELRA; NOT LEAN VERIFIED

摘要

前兩篇 RT-FBE 已在 Radix Tower 第十二篇的三階段八重操作交會語法內，建立 $K$ （原始運算元上限）與 $N$ （結果／中間態觀察上限）的雙軸濾過。第十二篇的 $(m,u,z)$ 是三個精確數值狀態，不是單一答案； $N$ 可僅裁切終點 $z$ ，也可同時裁切 $m,u,z$ 。在該語法內，固定 $K$ 後 $N\ge 2K$ 完整飽和；固定 $N$ 只裁切終點時， $K$ 無界增大不飽和；若 $N$ 裁切全部三個狀態，則 $K\ge\max(2,N)$ 時集合飽和。

本文將這些數學結果轉換為一個可交給 FELRA 的、來源範圍受限的有限運算覆蓋證書。證書提交完整且有序的精確三元組列表、來源語法版本、 $K,N$ 、界域類型、全集摘要與八重運算見證摘要。驗證器以兩套實作彼此獨立的標準整數流程重建全集：第一套直接枚舉原始運算元及各步操作標籤，第二套以質因數、整除及首次出現門檻重建；二者必須和提交集合逐元素一致。每個被接受三元組額外重播八種不同操作標籤的具體四運算元見證。

本輪原型新增 $67$ 項單元測試；將 $K=160$ 的 $40,212$ 筆精確出現門檻，與上一輪的 $50,880$ 個 $(K,N)$ 界域計數逐項核對；重新檢查使用者原始 Radix Tower 壓縮檔中 Paper XII 的 $20$ 筆 SHA-256 manifest，並確認 $K=40$ 的 $2,488$ 個精確三元組與原始 CSV 完全相同。另建立七個完整、自包含的證書示例，其中最大的一份包含 $40,212$ 個三元組及 $321,696$ 次模板見證核驗。

這不是新的通用數學證明助理、全數學語法的有限窮盡、真實 TCGCT／TCGQT 工程接線、全域資訊守恆律或 Lean 已證明定理。它是一個可獨立重跑的、範圍十分清楚的計算正確性與覆蓋完整性原型。

1. 原研究問題與三種不能混同的正確性

[DEF 1.1] 對同一研究結論，至少區分：

運算見證正確性（witness correctness）：給定具體數值、算子及輸入時，各中間值與輸出值精確符合已宣告算術規則。
有限集合完整性（finite coverage completeness）：不只所有已提交項都正確，還沒有漏掉指定語法及界域內任何合法對象。
命題有效性（claim validity）：某項全稱、存在、統計或自然語言命題，是否真的被上述證據支持，且前提、數域、邊界與推論方法無誤。

前兩項是本篇新增證書的責任；第三項仍歸 FELRA 既有 PPV、Lean、SMT 或其他已授權證明系統。FELRA 的 LOCAL_VERIFIED 不可自行提升為 ORIGINAL_GOAL_VERIFIED。命題可以保持 OPEN，而獨立的有限計算資產仍能保持 EXACT_EXHAUSTIVE_VERIFIED。

1.1 覆蓋不是觀察、不是來源真實性

一個 SHA-256 摘要只標示特定內容的位元組或指定 canonical JSON 快照。若提交集合漏了一筆，提交者重算摘要仍會得到有效雜湊。因此摘要一致不證明窮盡性。由同一文件自附的來源 hash 也不自動證明該文件確實由指定研究者或測量者提供；正式來源授權需外部釘選、簽章、可信通道及版本政策。

TCGCT 原生精確整數／有理數、TCGQT 多尺度唯讀觀察、SIO 跨表示等價，以及 GCTI 的可重用證據理念，在此只作接口角色說明；不預支尚未合併的實作。

2. 精確語法及界域

[DEF 2.1] 取整數 $K\ge2$ ，原始運算元集合為：

A_K=\{2,3,\ldots,K\}.

三階段計算形式：

m=a\ o_0\ b,\qquad u=m\ o_1\ c,\qquad z=u\ o_2\ d.

其中 $a,b,c,d\in A_K$ ，第一階段 $o_0\in\{A,M\}$ 表加法與乘法；第二、三階段 $o_1,o_2\in\{A,S,M,D\}$ 分別表示加法、正值減法、乘法、精確整除。全部精確中間態必為正整數；除法的結果與被除數也必為正整數，無餘數。不容許近似、截斷、浮點除法或暗中修改運算元範圍。

對指定三元組 $(m,u,z)$ ，若第一階段的兩個標籤都有合法來源，第二、三階段各有兩個不同標籤可生成相同的下個數值，則稱之為八重交會三元組。其八重是運算標籤模板數，而非原始四輸入歷程的重數或獨立數值個數。

[DEF 2.2] 令 $E_K$ 為固定 $K$ 的完整八重三元組集合。兩種視窗是：

E^{\mathrm{out}}_{K,N}=\{(m,u,z)\in E_K:z\le N\},

E^{\mathrm{all}}_{K,N}=\{(m,u,z)\in E_K:\max(m,u,z)\le N\}.

注意，前者允許中間值超出 $N$ 。對 $K=40,N=1$ ，前者有 $129$ 筆，後者是空集合；因此一個沒有 window 欄位的 EXHAUSTIVE 聲明不應被接受。

3. 第一個核心結論：八重模板的條件性分解

[PROP 3.1] 在 [DEF 2.1] 的語法及四個原始運算元可依階段自由選擇的前提下，一個三元組是八重交會，當且僅當第一階段可分別以 $A,M$ 到達 $m$ ，且後兩個轉移各可用兩種不同操作標籤到達其指定值。

[PROOF] 當右運算元 $d\ge2$ ，加法／乘法必使正值增加；正值減法／精確整除若合法，必使數值嚴格減少。因此對固定 $x,y$ ，後兩階段至多有兩種不同可用標籤：增加時可用 $A,M$ ，減少時可用 $S,D$ 。若三階段各有 $2,2,2$ 個標籤選擇，由於各階段右運算元沒有共享、互異或全域消耗限制，任選第一階段某來源、再依序任選第二與第三階段見證，所得完整四輸入歷程仍合法，合計八個不同標籤字。反之若全部八個標籤字可實現，每階段在固定精確中間態下必有前述對應標籤見證。證畢。

界線。 若後續引入共用運算元、非純函數副作用、跨步資源限制、其他算子或不同數域，該分解不得直接沿用。

4. 第二個核心結論：雙獨立全集構造

4.1 Oracle A：直接原始運算元枚舉

Oracle A 首先對每個 $(a,b)\in A_K^2$ 直接計算 $a+b$ 與 $a\cdot b$ ，為每個 $m$ 記錄可實現的來源標籤。再對每個合法 $m$ ，遍歷 $d\in A_K$ 及 $A,S,M,D$ 四種操作產生所有合法的 $u$ ；以同一方式取得所有後繼 $z$ 。對三階段各有二標籤的數值三元組，依選定的 $N$ 視窗過濾，取無重複集合。

由 [PROP 3.1]，這種逐步分解式枚舉等價於四個原始運算元及全部操作模板的完整窮舉。在較小 $K=2,\ldots,8$ ，本輪另有真正的四重原始運算元巢狀窮舉作第三種負對照。

4.2 Oracle B：首次出現門檻

沿 RT-FBE-02，對 $m$ 同時有加法與乘法來源所需的最小運算元上限，定義：

\kappa_0(m)=\max\left(\left\lceil\frac{m}{2}\right\rceil,\min_{d\mid m,\;2\le d\le\sqrt m}\frac{m}{d}\right)

（僅在 $m\ge4$ 為合數時有定義）。對 $x\ne y$ ，令 $l=\min(x,y)$ 、 $h=\max(x,y)$ ，若 $l\mid h$ 且 $h-l\ge2$ ，定義：

\kappa_1(x,y)=\max\left(\frac hl,h-l\right).

其餘情況未定義。精確三元組首次出現的最小界限為：

\kappa(m,u,z)=\max\left(\kappa_0(m),\kappa_1(m,u),\kappa_1(u,z)\right)

（若任一項未定義，整體未定義）。本輪 Oracle B 依整除關係與界限直接構造符合 $\kappa\le K$ 的三元組，再用指定視窗過濾；它不調用 Oracle A 的原始運算元枚舉資料。

4.3 兩個集合必須逐項相等

[PROP 4.1] 設提交集合為 $S$ 。在指定的有限語法與界域內，若兩個演算法的數學定義均符合前述推導，且實際驗證得到：

S=E^{A}_{K,N}=E^{B}_{K,N},

則 $S$ 恰為該有限語法下的完整八重三元組集合。若 additionally 每個成員的八個實際操作模板都能在精確算術內重播，則 $S$ 亦有完整的指定見證覆蓋。

[PROOF] Oracle A 由 [PROP 3.1] 對全部合法來源與後繼進行窮盡，因此得到所宣告語法的全部八重三元組。Oracle B 由 RT-FBE-02 已證的必要充分首次出現判準對同一集合提供不同構造；兩者與 $S$ 逐元素相同，故 $S$ 既沒有漏項，也沒有超出指定語法的假項。八模板具體見證的精確重播確保提交者沒有把單純相同數值誤報為八種合法模板。證畢。

[LIMIT] 以上為關於指定數學模型與演算法的條件性論證，不是經 Lean／Coq 機器驗證的 Python 程式正確性證明。兩種方法也可能共享錯誤的語法理解，因此需保存原始研究語法、獨立代碼路徑與負例。

5. 證書格式與信任分層

[ENGINEERING] 每份提交證書包含五個固定頂層鍵：

schema：固定版本 felra.finite-coverage.v0.1。
grammar：固定八重交會語法 ID；不得用這份證書證明其他數學語法。
scope：K,N,window,input_operand_min,input_operand_max,positive_intermediates,exact_integer_division。
submitted_set：排序且無重複的完整三元組、計數、集合摘要、八模板重播次數及八模板見證串摘要。
provenance：原始檔位元組摘要及非權威來源說明，不能自稱作者簽章。

強制拒絕的情形包括：只有計數或雜湊沒有全集、集合缺項、集合超出界域、整數被替換為布林或浮點、錯誤 K/N、視窗偷換、語法偷換、缺少八模板見證、來源釘選不同、未知 JSON 欄位或在提交證書中自行聲明 VERIFIED。驗證器狀態只從提交內容重新推導。

5.1 兩種不同的驗證結果

機器收據保留：

mathematical_status = EXACT_EXHAUSTIVE_VERIFIED：這份完整集合在目前獨立有限演算法下得到正確核對；不對應其他語法或其他界域。
publication_status = HOLD_MISSING_EXTERNAL_PIN 或 APPROVED_PINNED_FINITE_COVERAGE：表示此內容是否與呼叫者另外提供的 canonical SHA-256 摘要吻合。即使吻合，source_authenticity 仍是 NOT_ESTABLISHED；釘選只是一個外部完整性承諾，並未在本原型內驗證其授權來源。

必要區分： APPROVED_PINNED_FINITE_COVERAGE 不等於 ORIGINAL_GOAL_VERIFIED，不表示這份原稿是由某個第三方認證，也不代表推理超出有限界域。

5.2 對 FELRA PPV 的銜接

本輪實作的 felra_fbc.bridge.evaluate_request 會重新驗證完整證書，再檢查請求的語法與整個界域完全一致，才回覆 PRESENT 或 ABSENT。輸出的 claim_status 與 formal_proof_status 永遠維持 NOT_EVALUATED，不得暗中提升為 PPV 的 PROVES 或 VERIFIED。

若將來真的接入 FELRA v1.15.2，建議把此收據當成獨立的 FINITE_COMPUTE_COVERAGE 證據型別；PPV 只能通過明示的、能檢查 O_pre/O_dir/O_bridge/O_cover/O_trust 的方法規則引用它，不允許 coverage_status 直接成為全稱命題證明。

6. 對 TCGCT 與 TCGQT 的具體接口

6.1 TCGCT：精確計算正本與依賴來源

當實際接線時，TCGCT 可以提供精確有型別輸入、逐步算術、版本鎖定的來源 DAG 與數值重算；FELRA 驗證器仍需獨立核對其運算輸出。本包目前採用 Python 原生任意精度整數作精確參考核心，尚未呼叫正式 TCGCT P20。 若未來導入混合進位表示，轉碼前後必須證明或獨立核對保值，不能把位值符號的字面相同當成底層數值相同。

6.2 TCGQT：唯讀觀察與跨進位投影

本包 observe_read_only 對每個精確三元組取指定進位制的整數數量級層，計算投影格子數、同格不同精確狀態的配對數及最大格子佔據。全部只是 TCGQT 風格的參考觀察，未連接 TCGQT 官方執行器。

在 $K=40,N=40$ 、只限制輸出的同一批 $2339$ 個精確三元組上：

進位基底	數量級格子	同格不同精確三元組的無序配對數
2	106	64,882
8	11	1,135,345
10	8	957,808
16	8	654,836

這裡的格子數並不單調決定碰撞配對數。這些投影不得反過來改寫 submitted_set.triples 或讓觀察器聲稱原始計算已經獲證。所有視圖皆記錄 READ_ONLY_OBSERVER 並保持 authoritative_math=false。

7. 精確負對照與界域飽和

[COUNTER 7.1] 對任意 $K\ge3$ ，三元組 $(2K,K,1)$ 是合法八重交會，且首次於界域 $K$ 出現。它在 output_only 且 $N=1$ 的集合裡；但在 all_states 且 $N=1$ 的集合裡不存在。故結果視窗不等於中間態視窗，也不能從某一個有限 $K$ 的終點窮盡推論固定 $N=1$ 下所有無界 $K$ 的源歷程已窮盡。

[PROP 7.2] 在本篇已固定的語法中，每筆八重三元組的三個精確數值皆不超過 $2K$ ，故 $N\ge 2K$ 時兩種視窗都取得固定 $K$ 的全集。對 all_states 視窗，若固定 $N$ 且 $K\ge\max(2,N)$ ，集合在後續放大 $K$ 時不再增加。但 output_only 的固定 $N$ 則沒有這種 $K$ -方向飽和。

重要例外： 這些飽和性是 Paper XII 語法的結果；對任意深度、任意算子、負整數、實數、浮點或量子過程不得複用。

8. 本輪實際運行與原始研究核對

以下為執行程式後保存於 results/ 的精確結果，不是尚未執行的性能預估：

證書界域	視窗	完整精確三元組數	八模板重播次數
K=40, N=1	僅終點	129	1,032
K=40, N=40	僅終點	2,339	18,712
K=40, N=40	全部三狀態	2,074	16,592
K=40, N=80	僅終點（固定 K 已飽和）	2,488	19,904
K=80, N=40	僅終點	5,305	42,440
K=160, N=40	僅終點	12,008	96,064
K=160, N=320	全部三狀態（固定 K 已飽和）	40,212	321,696

完整原稿核對：原始 Radix Tower 壓縮檔的 SHA-256 為 72f844cde3df43913eb01b577dfd7ba5fcb4fc92cc6412ba22a890fc1e212059；原 Paper XII 的 $20$ 筆檔案 manifest 全部一致；其 $K=40$ 、 $N=80$ 集合的 $2,488$ 個三元組與本輪重算全集完全相同。上一輪 $40,212$ 筆最小門檻 CSV 與 $50,880$ 個二維矩陣計數亦已逐筆重算比對。

軟體驗收：69/69 新增測試通過，包含標籤式窮盡、門檻式窮盡、 $K=2\ldots8$ 原始四輸入小域完全窮盡、假證書拒絕、非法操作型別、跨界域冒用及唯讀觀察不可污染數學正本。完整 bundle validation 包含外部原稿核對與 ZIP 重開核驗；相關重播命令詳見 README。

統計與速度聲明： 本輪沒有做與正式 TCGCT P20、TCGQT 官方程式或其他證明助理的公平速度基準，因此不聲稱一般運算加速。兩套獨立全集演算法會帶來額外計算成本；其直接收益是界域完整性稽核，而不是已證實的算力節省。

9. 可重播命令與 canonical source 政策

在本壓縮包根目錄下執行（不需聯網，僅 Python 標準函式庫）：

PYTHONPATH=src python -m unittest discover -s tests -v
PYTHONPATH=src python -m felra_fbc issue --k 40 --n 40 --window output_only --output /tmp/k40.json
PYTHONPATH=src python -m felra_fbc verify --certificate /tmp/k40.json --output /tmp/k40.receipt.json
PYTHONPATH=src python -m felra_fbc observe --certificate /tmp/k40.json --bases 2,8,10,16 --output /tmp/k40.view.json

Windows PowerShell 可先設定 PYTHONPATH 為 src，再使用同一批 python -m ... 命令。外部來源若提供 canonical certificate SHA-256，再將 --expected-cert-sha256 加至驗證命令；不要把計算程式自行產生的摘要冒稱為獨立可信來源。

完整上游數據核對需要提供使用者原始 Radix_Tower.zip 與上一版 RT-FBE-02 的資料夾；如未提供，證書自身仍可有限重播，但不能宣稱重新核對了使用者的上游來源檔案。

所有正式研究內容以 UTF-8、LF、無 BOM 保存；LaTeX 一律使用 $...$ 與 $$...$$。壓縮包內含單一 canonical Markdown 原稿、程式、JSON 證書、回歸樣本、完整性摘要及本地接入說明。

10. 研究成果與不可逾越的界線

本篇已完成的是對 Paper XII 有限三階段八重交會語法的精確覆蓋證書系統：它能在已限定的 $K,N$ 及視窗政策下重算完整三元組集合，拒絕缺項或冒用界域，並把這些有限計算成果交給數學 AI 使用，而不自動宣稱某個研究命題成立。

尚未建立的是全數學運算語法的覆蓋證書、一般長度的任意運算 DAG 之窮盡、無限界域的一般定理、FELRA PPV 實際合併、TCGCT P20 及 TCGQT 官方工具的執行對接、來源授權機制或形式證明助理驗證。它們不得被本輪的 PASS 標籤偷換。

本篇結語：

計算正確性是一筆可以保存的證據；界域完整性是另一筆必須獨立建立的證據。只有兩者的作用域都明確，數學 AI 才有資格把「已經算對」轉化為「在這個有限世界裡，已經算全」。

參考來源

EveMissLab 上游研究與實作（本輪實際核對或引用其指定內容）

Neo.K / GPT-6，《進位制塔樓有限界域研究 I》，v0.1，2026-11-05；完整壓縮包 Radix_Tower_Finite_Boundary_Exhaustion_v0.1_2026-11-05.zip。
Neo.K / GPT-6，《進位制塔樓有限界域研究 II》，v0.1，2026-11-05；RT_FBE_02_Two_Axis_Exhaustion_Birth_Thresholds_and_Window_Semantics_v0.1.md。
Neo.K / EveMissLab，《進位制塔樓與全域運算關係幾何》第十二篇，使用者提供的 Radix_Tower.zip 原始附件及 SHA-256 manifest。
FELRA，《形式演化邏輯—規則架構》，目前 GitHub main 的 pyproject.toml 標記 v1.15.2；https://github.com/kakon77777-commits/FELRA，docs/PPV.md、docs/FORMAL_BACKENDS.md、AGENTS.md。
TCGCT 精確運算及 P20 來源冷啟動：https://github.com/kakon77777-commits/TCGCT。
TCGQT 獨立 BigInt／唯讀觀察：https://github.com/kakon77777-commits/TCGQT。
《TCGCT × TCGQT 多尺度觀察計算橋接與核心不變量契約》，2026-10-31，TCGCT docs/papers/。
《FELRA 計算正確性優先架構 v0.1》，2026-11-05；本輪上一階段獨立原型。

既有數學與計算機科學背景（非原創歸屬）

有限集合枚舉、整數因數分解、正整數除法、必要充分條件、字母表標記歷程、獨立 oracle 交叉測試、內容定址摘要與 fail-closed 證書檢查均屬成熟方法；本文的研究性成果在於將其按 Paper XII 的完整精確語法與 FELRA/TCGCT/TCGQT 分工組成可核查的界域證據接口。

End of RT-FBE-03 / FELRA-FBC-01 v0.1.

進位制塔樓有限界域研究 III：FELRA 有限精確運算覆蓋證書、雙重窮盡核查與計算正確性優先