← Archive
lm-005433 · 2026-11

FELRA 計算正確性優先 M1：精確運算雙重重播、有限覆蓋證據綁定與命題隔離

zh-Hant · md Raw source ↗ Metadata ↗
下載 MD 檔 ⬇
📎 附件 · Companion files — 隨文交付的程式 / 證明 / 資料，可獨立下載重驗
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，全部節點輸入、中間值與輸出經精確有理數重新計算。此驗證不推論所有可能的數學歷程已被窮盡。
  • 有限覆蓋證據：給定明確語法、 KK 、 NN 與觀察窗，完整枚舉指定範圍的合法三元組，並核對每個交會的八個生成模板。此驗證不等於一般無界域的全稱命題已證。
  • 研究命題證據：交由 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 本輪新增的閘門

             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,λ),D=(V,E,\lambda),

每個節點具有標記 λ(v)\lambda(v)，其值位於有理數域：

q:V→Q.q:V\to\mathbb Q.

對任一合法運算節點 v=ω(u1,…,ur)v=\omega(u_1,\ldots,u_r)，要求：

q(v)=ω(q(u1),…,q(ur)).q(v)=\omega(q(u_1),\ldots,q(u_r)).

原型限定有理數字面量、精確混合進位整數字面量、加減乘除、取負及有界整數冪；正規化與資源上限明示。未聲明的浮點精確性、不符合型別的布林數值、零分母、前向循環依賴和超出資源上限的計算都拒絕。注意：對 000^0 的行為沿用原參考核心的整數冪運算慣例，不能自動輸出「所有數學語境都已判定」的無條件命題。

3.2 有限覆蓋集合

指定語法 radix-tower.paper12.eightfold-triples.v1 及界域規格：

S=(K,N,W).S=(K,N,W).

WW 必須為 output_only 或 all_states。精確合法的八重交會集合記為：

US⊆Z>03.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)=(q(m),q(u),q(z)).

要把該圖聲明為八重交會中的一條歷程，必須同時滿足：

B(D)∈US,B(D)\in U_S,

以及來源到 mm 為合法加法或乘法、 mm 到 uu 及 uu 到 zz 為合法算子／源操作數、每個操作數受 KK 約束、所有中間值為正整數，且發布的圖輸出必須等於 zz 節點。這最後一條不能省略：若驗證的是一條旁支，真正發布的值卻來自別的節點，即使兩者的計算都正確，也不能把前者的證書錯套到後者。

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 為：

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 的該版本語法及界域有效。

在三份外部內容摘要都匹配時，本輪可生成：

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 使用的最小分工是：

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. 工程驗收與可反駁條件

基於本輪提交的程式與示例，需執行以下可重播流程：

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.