---
title: "FELRA 數學 AI 計算正確性優先改造：TCGCT × TCGQT × PPV 驗證總線"
english_title: "FELRA Math-AI Computation-First Architecture: Exact Arithmetic Gates, TCGCT/TCGQT Adapters, and PPV"
version: "v0.1 — implementation design and isolated reference prototype"
date: "2026-11-05"
author: "Neo.K（研究方向、FELRA 計算正確性優先與 TCGCT/TCGQT 整合意圖）／GPT-6（現況盤點、設計契約及隔離式原型）"
affiliation: "EveMissLab／一言諾科技有限公司"
status: "DESIGN / ISOLATED STANDARD-LIBRARY PROTOTYPE; NOT MERGED INTO FELRA; NOT LIVE TCGCT/TCGQT INTEGRATION; NOT A UNIVERSAL CORRECTNESS GUARANTEE"
source_format: "UTF-8, LF, no BOM"
math_delimiters: " $...$ and $$...$$ only"
---

# FELRA 數學 AI 計算正確性優先改造

**作者：** Neo.K（研究方向、FELRA 計算正確性優先與 TCGCT/TCGQT 整合意圖）／GPT-6（現況盤點、設計契約及隔離式原型）  
**機構：** EveMissLab／一言諾科技有限公司  
**日期：** 2026-11-05  
**版本：** v0.1 — implementation design and isolated reference prototype  
**原稿狀態：** DESIGN / ISOLATED STANDARD-LIBRARY PROTOTYPE; NOT MERGED INTO FELRA; NOT LIVE TCGCT/TCGQT INTEGRATION; NOT A UNIVERSAL CORRECTNESS GUARANTEE  

## 摘要

將數學 AI 的預設驗證入口從「直接請求 Lean／形式證明」改成「FELRA 先驗算計算，再將需要形式驗證的命題送到 PPV 與 Lean」。本設計**不把 Lean 刪除**：Lean 4 仍保有自身 kernel 之 proof acceptance 權威；FELRA 負責路由、算術和來源稽核、證明義務、狀態推導與公開閘門；TCGCT 提供原生精確數值和計算 DAG 的計算來源候選；TCGQT 提供獨立唯讀投影、多尺度觀察和一致性觀測。三者不得互相冒充。

研究者可保留、探索和修改錯誤或尚未完成的命題；但**未經計算驗證的數值結果不得標為可信，也不得被 AI 用作已確認計算前提**。計算過程的正確性和命題內容的真偽是兩條不同的驗證軸。

這是**計算正確性優先（computation-first）**，而非「計算正確性取代形式證明」；也不保證未支援問題能被算出、所有源資料都真實，或任何程式絕無 bug。需要保守拒絕與可重演證書。

## 1. 已核對的上游現況與版本定位

本次唯讀檢查 GitHub `kakon77777-commits/FELRA` 的 `main`：

- `pyproject.toml` 為 **1.15.2**（2026-10-19），其 `README.md` 開頭仍描述「目前版本 v1.11.0」，此為文件版本漂移；工程應以 package、changelog 與實際測試共同確認版本，不直接信 README 開頭。
- FELRA 現有安全 AST、Decimal／Rational、多精度、數值健全性、跨方法檢查、反例、資料重播、Lean／Z3／TLC 和 PPV。
- `felra.ppv.exact` 已拒絕二進位 float 偷渡、真假數值混用、零分母、超出預算的指數或質數輸入。
- `felra.ppv.kernel` 只由 receipt 推導 `VERIFIED`、`REFUTED`、`OPEN`、`TRUST_CONFLICT` 等命題狀態，不由模型自行宣告；已有 Lean bound/unbound、alignment、衝突診斷與獨立 `ppv-verify`。
- `AGENTS.md` 明定不得未經批准靜默改變 pass／proof／public API 的意義；非簡單版本需本地安全分支、全套測試、drill、校驗後提交。
- TCGCT P20 保留原生混合進位來源、DAG 及冷啟動來源釘選；TCGQT P20 有獨立 Node.js `BigInt`／SHA-256 來源觀察。現有 README 的 demo receipt 不等於來源認證。
- 2026-10-31 的 TCGCT–TCGQT AMOCF 橋接仍是**設計契約**；不得把 `E_L(F_L(G_L(x)))=F_B(x)` 的目標當成一般已完成的計算等價證明。

來源（唯讀核對）及內容指紋：

1. FELRA `pyproject.toml` blob `3374ca464c3d28e417de90b12bf8c0af184f8bd9`：https://github.com/kakon77777-commits/FELRA/blob/main/pyproject.toml
2. FELRA `CHANGELOG.md` blob `a25520aa9832372f91e5e6d7b942dbb59d429652`：https://github.com/kakon77777-commits/FELRA/blob/main/CHANGELOG.md
3. FELRA `docs/PPV.md` blob `a0e6c5dd2205639561bbe32aa86470d0d3825775`：https://github.com/kakon77777-commits/FELRA/blob/main/docs/PPV.md
4. FELRA `AGENTS.md` blob `c1629916ee672c48a7982e022a7107a54a0fc08e`：https://github.com/kakon77777-commits/FELRA/blob/main/AGENTS.md
5. TCGCT `README_P20.md` blob `8d5ec0c95654608ba60425fab501d7e1c187036f`：https://github.com/kakon77777-commits/TCGCT/blob/main/README_P20.md
6. TCGQT `README_P20.md` blob `f901727071602e66ced5ce449608833da17e0c54`：https://github.com/kakon77777-commits/TCGQT/blob/main/README_P20.md
7. 橋接契約 blob `5d5302343f429e11cacd03811ed081552dc1f1c5`：https://github.com/kakon77777-commits/TCGCT/blob/main/docs/papers/TCGCT_TCGQT_Multiscale_Compute_Bridge_Contract_v0.1_DRAFT_2026-10-31.md

這些是檔案 blob 指紋，不是整棵 repository commit pin，也不是第三方作者身份證明。正式整合前需記錄各倉的完整 commit、工具鏈和外部權限。

## 2. 產品目標與不可妥協的分離

### 2.1 計算軸（Computation Verdict）

當任務涉及已支援且具有可執行精確語義的運算，要求：

- 明示原始輸入、型別、定義域、算子與前置條件；
- 每個可檢查中間節點具有精確輸出與依賴；
- 使用至少一個不共享核心錯誤來源的驗證路徑重播或核對；
- 後端版本、來源快照、依賴證據與轉碼完整保留；
- 不通過時硬阻擋可信數值發布；結果為 `UNVERIFIED`、`BLOCKED` 或 `UNSUPPORTED`，而不是猜出近似值冒充精確。

對浮點、連續、無窮運算，必須另給已驗證的誤差界、數值語義與適用範圍；否則不能標作 `EXACT`。硬體執行環境、RAM、Token 或超時是可拒絕的前提，絕非正確性豁免。

### 2.2 命題軸（Claim Verdict）

允許 AI 提交 `DRAFT`、`OPEN`、`REFUTED`、`CONDITIONAL` 或明確修正的命題；FELRA PPV 的正式狀態仍由現有 kernel 推導。**不存在「我已算對 100 個點，所以命題已被證明」**的自動提升。

示例：在標準主持人協議下計算三門問題換門勝率 $2/3$ 可以通過運算證據；「所有三門問題條件下換門永遠有 $2/3$ 勝率」仍可能 `REFUTED`。計算 receipt 不因命題失敗而失效，但一旦修正了計算的生成規則或機率測度，就必須重新判定 receipt 適用性。

### 2.3 雙軸公開原則

| 計算軸 | 命題軸 | AI 可做什麼 |
|---|---|---|
| EXACT_VERIFIED | OPEN | 顯示已核驗數值、命題待證，不暗示定理成立 |
| EXACT_VERIFIED | REFUTED | 保留數值作反例或修正素材；不得發布原命題成立 |
| EXACT_VERIFIED | VERIFIED | 可以分別標示「算術核對」與「形式證明」，並保留兩份證書 |
| BOUNDED_VERIFIED | OPEN | 僅發布有界誤差、精度與條件，禁止標為精確等式 |
| MISMATCH / INVALID / UNSUPPORTED | 任意 | 阻擋可信計算數值；不以 Lean 成功掩蓋算術錯誤 |
| EXACT_VERIFIED，但來源／視圖有衝突 | 任意 | 隔離發布，直到釐清版本、來源或觀察結果 |

這個矩陣只定義新的**計算軸**與對外發布策略，**不改 FELRA v1.15.2 的既有 PPV status 語義**。

## 3. 建議的目標架構（不是現有運作狀態）

```text
OCME 知識／數學 AI 研究提案
          |
          v
FELRA Intake（將計算任務與命題主張分離）
          |
          +--> CalculationArtifact --+--> TCGCT native exact adapter
          |                          +--> FELRA exact / independent oracle
          |                          +--> arithmetic DAG replayer
          |                          +--> receipt + source / type / budget audit
          |                                    |
          |                                    v
          |                               Compute Gate
          |                                    |
          |                   +----------------+-----------------+
          |                   |                                  |
          |              EXACT / BOUNDED                  REJECTED / OPEN
          |                   |                                  |
          |                   +--> TCGQT read-only view           +--> AI replan
          |                             |
          |                        display gate
          |
          +--> ClaimArtifact --> FELRA PPV --> SMT / Lean 4 / optional other checks
                              |                       |
                              +--> scope + methods + evidence
                                          |
                                          v
                                  Independent Publication Gate
```

- **TCGCT** 是原生混合進位／精確算術及來源 DAG 的候選 producer，不是唯一不可質疑的 oracle。
- **FELRA compute gate** 把 TCGCT 產物及 Python Fraction、現有 `felra.ppv.exact` 或其他真正獨立的實作交叉檢查。避免「TCGCT 自己算、TCGCT 自己宣告對」；高保證需求允許多實作一致及形式證書。
- **TCGQT** 只觀察、給出形狀／尺度／相位／進位鏡頭和算法建議；若視圖顯示出與精確核對不一致的數值，回報視圖衝突，不改 canonical 值。
- **PPV／Lean** 處理的是命題與推理可靠性，不能被一個 `calc=PASS` 偷升為 `VERIFIED`。

## 4. 最小型別契約

### CalculationArtifact

```text
id, source_id, source_revision, input_types, precision_policy,
operation_dag, canonical_intermediates, exact_or_bounded_outputs,
algorithm_id, engine_version, valid_domain, provenance_refs,
independent_check_receipts, observation_refs, publish_gate
```

`canonical_intermediates` 每一項至少包含 node id、op、typed args、typed result、exactness grade、依賴與來源版本；來源若會變，應記錄快照 pin 和失效閉包。儲存 Hash 不等於資料真實性、授權或 signed attestation。

### ClaimArtifact

```text
claim_ref, revision, natural_language_statement, formal_spec,
quantifiers, domain, assumptions, original_goal, linked_calculations,
PPV_receipts, PPV_derived_status, scope_alignment
```

CalculationArtifact 只提供一條可引用的數學證據邊；ClaimArtifact 的真偽仍由 PPV methods、scope/alignment 與 proof obligations 判定。

### 出錯時拒絕的最低集合

`EXACT_MISMATCH`、`DIV_BY_ZERO`、`TYPE_MISMATCH`、`ROUNDING_UNCERTIFIED`、`UNSUPPORTED_OPERATOR`、`DEPENDENCY_CYCLE`、`SOURCE_REVISION_MISMATCH`、`STALE_VIEW`、`MISSING_PROVENANCE`、`BUDGET_EXHAUSTED`、`VERIFIER_DISAGREEMENT`、`CLAIM_SCOPE_OPEN`。不同錯誤不能被壓成同一個成功布林值。

## 5. 對現有 FELRA 的最小侵入改動

建議新增平行模組，不先重構 `felra.ppv.kernel`：

```text
src/felra/computation/
    model.py               # Calculator IR、型別、source revision
    exact_gate.py          # 獨立逐節點驗算、失敗即拒絕
    source.py              # source pins / revision / invalidation
    receipts.py            # arithmetic certificate schema + canonical digest
    adapters/
        tcgct.py           # P20 輸出轉入 CalculationArtifact，固定版本
        tcgqt.py           # P20/AMOCF observation，唯讀權限
    policy.py              # 嚴格可發布門檻
    replay.py              # 不依賴主執行器的證據重播

src/felra/cli.py           # 預計新增 compute-verify / compute-replay 子命令
src/felra/runner.py        # 可選 computation: 管線；不改既有命題與 PPV 預設語義
schema/                   # compute-job, compute-receipt JSON Schema
examples/computation_first/
tests/test_computation_*.py
scripts/drill_compute_first.py
```

**重要：** 上面只是整合檔案計畫。此包附帶的 `poc/compute_gate.py` 是**完全隔離式參考驗證器**，沒有寫進 FELRA 倉庫，也沒有呼叫真正的 TCGCT 或 TCGQT。正式版本需重用 FELRA 既有 exact machinery，減少重複規則；先建立與現有 `ppv-verify` 平行的 `compute-replay`，再研究可核驗的橋接 receipt。

## 6. TCGCT × TCGQT 接入次序

**M0｜凍結來源與非侵入規格。** 記錄 FELRA 1.15.2 的實際 commit、TCGCT P20、TCGQT P20 / AMOCF 版本及 golden vectors；建立專用 branch，不動 main。

**M1｜計算閘門。** 對純整數、有理數、有限 DAG 先完成 independent replay，拒絕不一致與未證精度。可用 POC 的錯誤案例作紅隊基準。

**M2｜TCGCT 精確接入。** 實際讀取 TCGCT 原生 mixed-radix raw terms、來源 cold bundle、依賴圖與 output；對全部中間節點做 independent Fraction / BigInt 或其他已核查方法。不得用單一來源自簽 hash 假裝驗證。

**M3｜TCGQT 只讀接入。** 接收 TCGCT 已驗證 source revision，根據同一值生成多進位／相位／多尺度圖；將圖的 source links 與數值 display 對回精確 value，若不一致拒絕可見數值。

**M4｜與 PPV 銜接。** 為已驗證 arithmetic event 發行新的 typed receipt，和 PPV claim_ref、domain、assumption links 相連；Lean 4 仍只為需要的形式證明義務啟動，明示未完成與不適用。不得把 compute receipt 直接列作 `lean_proof`。

**M5｜數學 AI 發布與回歸。** AI 提案產生 typed computations → FELRA 驗證 → 失敗時重新計算或拒絕 → 成功才進入解釋／推理。所有 PR 必須跑原有 `pytest`、`ruff`、`compileall`、PPV drill 與新算術 drill；實測效能需將來源讀取、轉碼、oracle、快取及輸出成本全部計入。

## 7. 必測反例與正例

1. 精確字串 `0.1 + 0.2 = 3/10`，不因 Float64 表示問題失敗；若要求 binary64 bit-exact 則需另行指定其語義。
2. 中間節點寫錯，縱使後面寫出「正確最終答案」，整條歷程不得標為完全核對。
3. 除以零、零的負次方、浮點或 bool 混入 exact 欄位，必須拒絕。
4. 運算 DAG 有循環、缺依賴或重複 ID，必須拒絕。
5. TCGCT mixed radix 數位 `(0,1)`、基底 `(2,3)`（低位至高位）代表 2；若 claimed value 寫成 3，拒絕。
6. TCGQT 的觀察數值不吻合 canonical value，保留計算檢查事實，但阻擋錯誤視圖發布。
7. job payload 的 source pin 改變、來源 revision 過期、偽造命題 `status`、偽造 `receipt`，均不得變更驗證權限。
8. 計算完全正確，但命題仍 `OPEN`／`REFUTED`；不允許 status 混淆。
9. Lean 未安裝、Lean 失敗、對不同 sort 的真定理引用錯誤，不能讓不符的命題變 `VERIFIED`。
10. 多種進位編碼／不同 TCGQT 鏡頭不應修改計算基礎值；傳輸等價需逐案建立。
11. 有界浮點／區間只能在誤差界與舍入前提經驗證後輸出 `BOUNDED_VERIFIED`，不冒稱完全精確。
12. TCGCT／TCGQT 來源都可能各自正確而兩者版本不相容，這時暫停發布、重新解決來源對照。

## 8. 可交付物與本輪驗證範圍

本包附有 `poc/compute_gate.py`、`tests/test_compute_gate.py`、示例 jobs、型別契約和本地交接計畫。PoC 範圍：**有限、拓撲已排序的有理數計算 DAG；add/sub/mul/div/neg/pow_int、mixed-radix literal、逐節點宣告值比對、SHA-256 快照一致性、只讀視圖衝突的發布閘門。**

- reference arithmetic 由 Python stdlib `fractions.Fraction` 執行；尚**未**接真正的 FELRA/TCGCT/TCGQT runtime。
- 此 PoC 沒有數學「命題證明」能力、不驗證任何資料的物理真實性、沒有作者簽章／ACL／anti-rollback、沒有通用無限過程或跨系統證書。
- PoC 的 `EXACT_VERIFIED` 只指**在這個有界語法及給定快照內**運算輸出與獨立精確重播一致；`APPROVED_EXACT_FOR_PINNED_SNAPSHOT` 還要求提供匹配的外部 payload pin，**仍不是來源身份認證**。
- 不支援的算子、精度、無界過程、非決定性模型或需解析證明的任務回傳未支援或交給其他真正有資格的驗證器。

**若要把「AI 不太能算錯」變成可驗證工程要求，正確承諾應是：AI 可以提出不完整數學主張；但沒有足夠計算證據的數值，不能通過可信輸出閘門。**

## 9. 下一版正式整合的交付成功條件

M1 驗收是「在 FELRA 真正倉庫環境，原有所有 PPV 算例及 drill 不回退，已支援運算在全程重播核查後才發布」。M2/M3 驗收是「TCGCT P20 和 TCGQT P20 真實檔案與版本 receipt 可核對、其觀察不可覆寫 canonical 值」。M4 驗收是「PPV 狀態只從 kernel 導出，計算 receipt 只能作為已定義的 evidence，而不得直接代表 theorem proof」。所有工程改動必須先通過 repo 版控與本地整合驗收，不能根據此規格假稱已上線。

**結語：讓命題可以被修正，讓計算必須先接受查核；把算對的運算留作資產，把尚未證明的主張留作問題。**