--- title: "FELRA 計算正確性優先 M1：精確運算雙重重播、有限覆蓋證據綁定與命題隔離" english_title: "FELRA Computation-First M1: Dual Exact Replay, Finite Coverage Binding, and Claim Isolation" version: "v0.1" date: "2026-11-05" author: "Neo.K（研究目標及計算正確性優先設計）／GPT-6（工程規格、參考程式、測試與原稿）" affiliation: "EveMissLab／一言諾科技有限公司" status: "ENGINEERING RESEARCH DRAFT / ISOLATED REFERENCE / NOT MERGED INTO FELRA" canonical_source: "UTF-8 LF without BOM" canonical_math_delimiters: " $...$ and $$...$$ only" backend_status: "TCGCT P20 NOT CONNECTED; TCGQT P20 NOT CONNECTED; FELRA PPV NOT MODIFIED" external_peer_review: "NOT PEER REVIEWED" --- # FELRA 計算正確性優先 M1 ## 精確運算雙重重播、有限覆蓋證據綁定與命題隔離 **研究性參考實作，非正式 FELRA 發行版。** 本篇與完整程式碼、原始測試及重播資料在同一 ZIP 內交付。實驗的綠燈只證明在明示有限模型及測試中，程式對約定資料產生指定結果；不把它當成普適正確性的證明。 **作者：** Neo.K（研究目標及計算正確性優先設計）／GPT-6（工程規格、參考程式、測試與原稿） **機構：** EveMissLab／一言諾科技有限公司 **日期：** 2026-11-05 **版本：** v0.1 **原稿狀態：** ENGINEERING RESEARCH DRAFT / ISOLATED REFERENCE / NOT MERGED INTO FELRA ## 摘要 本輪承接 FELRA v1.15.2 既有的 PPV 研究證據狀態機、TCGCT／TCGQT 的精確運算與唯讀觀察分工，以及 RT-FBE-03 對 Radix Tower 第十二篇三階段八重交會的有限覆蓋證書。主要問題不是發明新的全域資訊定理，而是實現一道**計算資料優先**的安全邊界：人工或 AI 的研究命題即使仍為 OPEN、CONDITIONAL 或 REFUTED，已被獨立重算的計算產物仍能保存；同時，任何錯誤數值、中間狀態不一致、錯誤界域引用或不充分的來源證據，都不得升級為可發布的精確計算收據。 本包實作 `felra-cf-m1` 獨立 CLI、雙條計算重播、完整有限界域窮舉、實際 DAG 與八重交會證據的鏈結、三重內容摘要釘選和獨立收據重驗。為避免干擾正式驗證核心，`felra.ppv.kernel`、Lean 與 SMT 皆不在此原型的程式路徑內。真正 FELRA 整合僅提供經 Git blob 核對的增量 `pyproject.toml` 補丁，需本地端於隔離分支完成完整回歸後才能合併。 ## 1. 研究目的：計算可被驗證，命題仍允許研究 本輪保持三個不同的判定對象： - **計算執行證據**：給定固定型別的有限計算 DAG，全部節點輸入、中間值與輸出經精確有理數重新計算。此驗證不推論所有可能的數學歷程已被窮盡。 - **有限覆蓋證據**：給定明確語法、 $K$ 、 $N$ 與觀察窗，完整枚舉指定範圍的合法三元組，並核對每個交會的八個生成模板。此驗證不等於一般無界域的全稱命題已證。 - **研究命題證據**：交由 FELRA PPV、形式化後端或其他明確認可的機制決定。計算／覆蓋的綠燈不能被暗中轉成 `PPV VERIFIED`。 如果某位研究 AI 提出一條錯誤猜想，但恰好完成了一份正確的精確計算，應保存該計算證據，繼續修訂命題與適用域。若計算本身出錯，則必須拒絕使用該數值作為可信依據；不能用命題的說服力覆蓋算術錯誤。 ## 2. 接入架構與來源 ### 2.1 已核對的既有系統 - FELRA `main`：2026-11-05 讀取時，`pyproject.toml` 的版本為 1.15.2，Git blob 為 `3374ca464c3d28e417de90b12bf8c0af184f8bd9`；已有精確 PPV、對齊、信任衝突、Z3／Lean、來源重播。現有 PPV 不能因新計算閘門而變更結果語義。 - TCGCT P20：具原生精確來源冷啟動、DAG、來源修訂與重算的歷史研究接口；**本包沒有直接連接真實 TCGCT P20 runtime**。 - TCGQT P20：具獨立 BigInt 來源核查與唯讀觀察研究接口；**本包只測試模擬唯讀視圖，沒有接入真實 TCGQT P20 runtime**。 - RT-FBE-03：有限八重三元組的兩條獨立 oracle，以及數值與證書來源釘選的限制。研究包收錄該版冷凍 ZIP。 ### 2.2 本輪新增的閘門 ```text Math AI 提交的候選計算 DAG | +----------------+----------------+ | | Fraction 參考重播 (n,d) 整數對獨立重播 | | +---------------比對--------------+ | VERIFIED TRACE | 綁定實際三階段 m,u,z | PAPER XII 八重交會合法性與 K/N 視窗 | 完整集合兩個 oracle + 八模板見證 | Bundle / Job / Certificate 三份外部釘選 | 只發布範圍限定的收據 | FELRA PPV（完全獨立，未提升命題） ``` 完整的計算正確性不應靠「另一個 AI 覺得算對了」。本輪特地加入兩個不同的計算解釋器：第一個是前一版 `fractions.Fraction` 核心；第二個使用以整數分子／分母對組成的資料表示、獨立字面解析和獨立算子分派。兩者檢查每個中間節點，包括完整的分數和混合進位輸入。這種工程冗餘仍然共享 Python 整數算術和作業環境，因此不是數學上的雙獨立形式證明。 ## 3. 有界且可重播的形式定義 ### 3.1 計算圖與精確值 令有限的運算 DAG 為： $$ D=(V,E,\lambda), $$ 每個節點具有標記 $\lambda(v)$，其值位於有理數域： $$ q:V\to\mathbb Q. $$ 對任一合法運算節點 $v=\omega(u_1,\ldots,u_r)$，要求： $$ q(v)=\omega(q(u_1),\ldots,q(u_r)). $$ 原型限定有理數字面量、精確混合進位整數字面量、加減乘除、取負及有界整數冪；正規化與資源上限明示。未聲明的浮點精確性、不符合型別的布林數值、零分母、前向循環依賴和超出資源上限的計算都拒絕。注意：對 $0^0$ 的行為沿用原參考核心的整數冪運算慣例，不能自動輸出「所有數學語境都已判定」的無條件命題。 ### 3.2 有限覆蓋集合 指定語法 `radix-tower.paper12.eightfold-triples.v1` 及界域規格： $$ S=(K,N,W). $$ $W$ 必須為 `output_only` 或 `all_states`。精確合法的八重交會集合記為： $$ U_S\subseteq\mathbb Z_{>0}^{3}. $$ 此集合由 RT-FBE-03 原始四運算元／運算標籤 oracle 與整數門檻關係 oracle 分別重建，並比較全體集合；每個元素須能展示八種合法三階段歷程。只提供結果筆數、摘要、畫面格子或 AI 生成敘述皆不能證明集合窮盡。 ### 3.3 運算綁定 由來源圖中的實際節點索引選取： $$ B(D)=(q(m),q(u),q(z)). $$ 要把該圖聲明為八重交會中的一條歷程，必須同時滿足： $$ B(D)\in U_S, $$ 以及來源到 $m$ 為合法加法或乘法、 $m$ 到 $u$ 及 $u$ 到 $z$ 為合法算子／源操作數、每個操作數受 $K$ 約束、所有中間值為正整數，且**發布的圖輸出必須等於 $z$ 節點**。這最後一條不能省略：若驗證的是一條旁支，真正發布的值卻來自別的節點，即使兩者的計算都正確，也不能把前者的證書錯套到後者。 ### 3.4 三個獨立內容釘選 釘選分別指向： 1. `expected_bundle_sha256`：完整綁定請求，包含節點選擇、界域與命題參照； 2. `expected_job_sha256`：精確計算來源快照； 3. `expected_coverage_sha256`：有限覆蓋集合及其宣告語義。 三者以 UTF-8、排序欄位且無多餘空白的 canonical JSON 作摘要。此層只比較指定內容，**不**驗證作者身分、外部量測真實性、ACL、簽章、時間戳、防回滾或合法授權。展示用 `DEMO_PINS.json` 不得當成實際外部可信來源。 ## 4. 有限正例與負對照 ### 4.1 正例：K=40、N=1、只限制最終輸出 正例的真實 DAG 為： ```text 40 + 40 = 80 -> m 80 / 2 = 40 -> u 40 / 40 = 1 -> z ``` 第一段使用兩個在 K 內的來源運算元，後兩段也都符合 K 內的整數除法。完整三元組為 `(80,40,1)`，屬於指定的八重交會集合。使用原先的 `K40_N1_output.certificate.json`，覆蓋集合大小為 129，對應八模板證據數為 1,032。這些數據只對 Paper XII 的該版本語法及界域有效。 在三份外部內容摘要都匹配時，本輪可生成： ```text computation.status = EXACT_VERIFIED computation.oracle_agreement = TWO_EXACT_INTERPRETERS_AGREE binding.status = EIGHTFOLD_TRACE_VERIFIED coverage.status = EXACT_EXHAUSTIVE_VERIFIED coverage.membership = PRESENT release = APPROVED_EXACT_AND_SCOPED_MEMBERSHIP claim.status = NOT_EVALUATED_BY_GATEWAY ``` 若缺少摘要，仍可回報「本地重新算對」及「本地集合完整」兩項結果，但發布狀態必為 `HOLD`。不允許將由同一個提交者生成的摘要當成第三方來源可信性。 ### 4.2 必須拒絕的失敗模式 - 任何中間結果宣告錯誤，即使重新產生其內容摘要，也不能通過兩套精確運算。 - 真正發布的節點不是綁定的最終節點，即使旁支運算正確，也不允許錯誤套用。 - 來源值超出 K、運算標記錯誤、來源方向錯誤、同一節點重複引用成三階段，都必須停止。 - 覆蓋集合少一項或多一項，重新產生 JSON 摘要仍無法迴避雙 oracle 比較。 - 只更換 N、K 或 `output_only`／`all_states`，即使最後得到相同數值，也不能沿用原證書。 - TCGQT 型唯讀觀察建議的結果與精確圖不同，觀察器沒有權限覆寫算術正本。 - 來自計算圖、視圖、請求的 `formal_status: VERIFIED` 類注入欄位不能提升 PPV，也不能作為可讀出結果欄位。 - 收據被重寫、命題狀態被改成 VERIFIED，重播器從原材料重新計算後應發現不一致。 ### 4.3 有限範圍內的否定結論 若一條完整且精確的三階段運算產生了合法結果，但不構成指定八重交會的成員，在 `require_membership=false` 的查詢下，最多得到 `APPROVED_EXACT_WITH_SCOPED_ABSENCE`。它表示**在指定有限八重交會集合內不存在該三元組**，並不表示該數值不可計算、一般數學命題為假，或任何更廣泛的運算系統都不能生成它。 ## 5. 與 FELRA PPV 的關係 此原型刻意不呼叫 `felra.ppv.certifiers`，更不產生 `PROVES` 收據。FELRA v1.15.2 原先已區分 claim `VERIFIED`、`REFUTED`、`OPEN`、`TRUST_CONFLICT`、`BLOCKED` 等狀態，且具有域條件檢查與自然語言對齊責任。把算術結果強行變成 `PROVES`，會破壞原有證據權限模型。 因此可供未來 Math AI 使用的最小分工是： ```text compute_execution : VERIFIED / REJECTED / NOT_CHECKED finite_coverage : EXACT_EXHAUSTIVE_VERIFIED / REJECTED / NOT_CHECKED trace_binding : EIGHTFOLD_TRACE_VERIFIED / HOLD research_claim : NOT_EVALUATED_BY_GATEWAY ``` 真正的命題仍須經 FELRA PPV 的正式證據鏈處理。若一個人工或 AI 猜想是錯的，該猜想可以被駁斥，而已驗證的計算仍不被抹除。若來源數據錯誤，則引用這份錯誤資料的命題論證應被隔離與重新核驗。這正是**計算正確性優先，但不取消命題責任**。 ## 6. 現有接入成果與正式部署邊界 本輪交付： - `src/felra_cf_m1/reference_compute.py`：延續前一版精確 Fraction 計算圖核驗器； - `src/felra_cf_m1/independent_oracle.py`：獨立分子分母整數對重算及每一步比較； - `src/felra_fbc/`：延續 RT-FBE-03 兩路徑有限覆蓋核驗器； - `src/felra_cf_m1/gateway.py`：請求與實際精確 DAG、完整集合、原始來源三重摘要綁定； - `src/felra_cf_m1/cli.py`：`verify` 與 `replay` 指令； - `tests/`：既有計算核心與有限覆蓋測試，以及新的綁定攻擊、數域／進位交叉核查與重播測試； - `patches/`：以已讀取的正式 `pyproject.toml` 為基線，只增添 `felra-cf-m1` 外掛 CLI 及兩個輪包的增量補丁； - `handoff/`：Git、分支、差異審查與本地驗收契約。 這不是修改 FELRA 正式核心；也沒有實際呼叫 TCGCT P20 cold bootstrap 或 TCGQT P20 BigInt observer，更沒有在這個容器執行正式 FELRA 的 Lean／Z3 全套 drill。**各項未完成處必須明確保留在後續版本接入清單，不能從本包的測試綠燈推定已完成。** ## 7. 工程驗收與可反駁條件 基於本輪提交的程式與示例，需執行以下可重播流程： ```bash PYTHONPATH=src python -m unittest discover -s tests -v PYTHONPATH=src python -m felra_cf_m1 verify \ --bundle examples/positive.bundle.json \ --expected-bundle-sha256 BUNDLE_PIN \ --expected-job-sha256 JOB_PIN \ --expected-coverage-sha256 COVERAGE_PIN \ --output results/positive.replayed.json PYTHONPATH=src python -m felra_cf_m1 replay \ --bundle examples/positive.bundle.json \ --receipt results/positive.replayed.json \ --expected-bundle-sha256 BUNDLE_PIN \ --expected-job-sha256 JOB_PIN \ --expected-coverage-sha256 COVERAGE_PIN \ --output results/replay.json ``` 將上述占位 `*_PIN` 換成從授權外部來源取得的值；本包 `DEMO_PINS.json` 只供離線示範。`verify` 檢查計算、界域與綁定；`replay` 不信任舊收據，而從原始輸入重新生成一份完整收據再作比較。任一不一致均以 `HOLD` 或拒絕碼結束。 系統仍有不可避免的理論界限：有限模型全部通過不等於對任何數學域都不會犯算術錯誤；兩套 Python 解釋器也不等於外部形式證明。後續應在真正的 FELRA／TCGCT／TCGQT 三倉測試中引入來源授權與獨立實作差異，並以實際出錯案例持續擴大拒絕範圍。 ## 8. 下一階段 - **M2：** 實作 TCGCT P20 冷啟動來源的只讀 producer adapter，核對其真實來源修訂、DAG、逐步值和計算型別；不複製或覆寫 canonical TCGCT 核心。 - **M3：** 實作 TCGQT P20 獨立 observer adapter，將多尺度纖維／進位視圖與精確來源完全隔離。 - **M4：** 在 FELRA PPV 中為計算收據建立可引用、可失效的依賴關係，但不能由資料證據自動推出命題 VERIFIED。 - **M5：** 在本地 Windows / Python 3.10+ 完成 FELRA 既有所有回歸、Lean/Z3 認證、惡意測例、來源錯配與整體效能比較後，才決定是否釋出正式版本。 ## 參考原稿及工程來源 1. FELRA 專案：https://github.com/kakon77777-commits/FELRA ，`README.md`、`pyproject.toml`、`docs/PPV.md`、`docs/FORMAL_BACKENDS.md`、`AGENTS.md`，於 2026-11-05 讀取。 2. TCGCT 專案：https://github.com/kakon77777-commits/TCGCT ，`README_P20.md`、`docs/papers/TCGCT_TCGQT_Multiscale_Compute_Bridge_Contract_v0.1_DRAFT_2026-10-31.md`。 3. TCGQT 專案：https://github.com/kakon77777-commits/TCGQT ，`README_P20.md`。 4. RT-FBE-01～03 有限界域窮盡與覆蓋證書研究及 FELRA Compute-First 設計包，詳見本包唯讀上游快照。 5. SIO Paper 04、GRST-12、XPVB-03/04 和 GCTI-01～07 作為概念來源；本篇不將其未證普適猜想當作參考程式的正確性前提。 **End — FELRA Computation-First M1 v0.1, isolated reference implementation.**