GCPR–RWL–FELRA · PYTHON 優先驗證工作台
FELRA
形式演化邏輯—規則架構 Formal Evolving Logic-Rule Architecture
FELRA 先把理論與資料轉換成可重現的計算證據，再將穩定結果提升為形式規約與證明義務。每一次執行都留下雜湊、種子與環境版本，結果可以被重新驗證，而不只是被信任。v1.9 起，它也記錄一個論證實際上確立了什麼：每個命題的狀態都從可重驗的證書推導出來，從不由作者自己寫下。v1.15 起，當證明與反例互相矛盾，它會指出錯的是哪個來源，並驗證這個答案。
核心能力
從假說到證據包
宣告式的 project.yaml 描述參數空間、命題與分析；FELRA 執行後產生一份完整的 Evidence Bundle——CSV、JSON、Markdown、圖形與雜湊，全部可追溯。
01 · SPEC
宣告式規約
YAML 描述命題與分析，安全的 AST 數值表達式求值，不需要額外膠水程式碼。
02 · SEARCH
反例搜索
有限宣告網格、邊界檢查與隨機採樣，系統性尋找命題的反例，而非單點驗證。
03 · DATA
資料契約與品質
CSV／JSON／JSONL／gzip 型別化資料集，缺失、無效、重複列全部記錄為證據，附來源雜湊。
04 · STATS
統計推論
描述統計、假設檢定、Bootstrap 信賴區間、檢定力分析與穩健性分析（bootstrap／subsample）。
05 · SENS
敏感度與帕雷托
局部有限差分敏感度、殘差診斷、一至高維參數掃描、雙目標非支配前沿。
06 · MODEL
交叉驗證與效應量
洩漏感知的數值回歸交叉驗證、共享折模型比較、標準化效應量、多重比較校正。
07 · REGISTRY
實驗總帳
Append-only 的 JSONL 實驗登錄，felra registry 依專案／狀態檢視歷史執行。
08 · LOCK
預註冊
不可變的科學計畫鎖定，警告與嚴格兩種執行模式，計畫本身有穩定的 SHA-256 指紋。
09 · REPLAY
證據溯源與重播
JSON／DOT／SVG 證據溯源圖，結果雜湊 result_sha256，felra replay 獨立重新驗證，felra export 產出論文就緒的 Methods／Results／Limitations 包。
10 · SYMBOLIC
符號驗證
透過 SymPy 做代數恆等與導數的精確檢查，支援每變數宣告假設（positive、real、integer 等）——在整個宣告域上成立的證明，補足上面取樣式通道的不足。
11 · SOUNDNESS
數值健全性
溢位／NaN 偵測、精確導數條件數、float64 對任意精度的災難性抵銷偵測——跟符號驗證共用同一套解析器，套用在真實取樣點上。
12 · CROSS-METHOD
跨方法一致性
為同一物理量宣告兩種以上獨立公式或評估後端（numeric／symbolic／high_precision），逐點比對是否一致——精度拉再高也救不了公式本身的奇異點，只有換一個方法才行。
13 · FORMAL
外部形式化檢查器
透過封閉的轉接器集合呼叫 Lean、TLC 與 z3。每個判定都記下實際執行之程式本體與所讀義務的 SHA-256，並與 Python 證據並列報告——從不合併。Lean 公理稽核可檢查整個開發只依賴宣告的公理集合。
14 · EXACT
精確與任意精度數值
Decimal、Rational 與 mpmath 後端；加引號的字面值精確讀取（"0.1" 就是 1/10，不是 float64）；精度階梯回報 stable／unstable／exhausted；跨後端一致性檢查。
15 · CERTIFY
可重驗的證書
端點為精確有理數的區間包絡、精確恆等、不等式與外部形式化判定——每份都把雜湊寫進清單，並從自己記錄的資料重驗，而不是重跑發出它的那個分析。
16 · OBLIGATION
證明義務匯出
把命題轉成斷言其否定的 SMT-LIB2，並與鑑別孿生一起檢查——翻譯若塌縮成空定義域，只會被報為「未判定」，永遠不會被報為「已證明」。
v1.9 – v1.15 · 證明過程驗證 PPV
狀態只能推導，不能宣告
專案可以宣告命題、為它們提出的證據，以及把命題串起來的論證。FELRA 對每份證據執行具名的核驗器，再由一個小型核心從收據推導每個狀態：VERIFIED、REFUTED、BLOCKED、OPEN 或 TRUST_CONFLICT。專案檔裡寫下的狀態，載入時就會被拒絕。每條論證都是核心能檢查的某個方法的一次應用；還沒解決的部分以未決義務圖追蹤；形式化必須對齊原本被問的問題；矛盾會被追溯到它的來源。
CERTIFIERS
十種核驗器，各自說清能力邊界
多項式正規形、獨立撰寫的 SymPy 檢查、精確反例與見證、搭配鑑別孿生的 z3、對一個經 z3 證明涵蓋定義域的方框做窮舉搜尋、巢狀量詞的見證函數，以及 Lean 4。z3 給出的每個模型都先用精確算術重驗，才會被採信。
METHODS · v1.12
每條論證五項義務
方法庫有七種方法。每次應用都必須解除 O_pre、O_dir、O_bridge、O_cover、O_trust——由明確規則、由 z3 判定方法庫從命題建出的公式，或由核心判定。其他方法只記錄、永不接受；作者假設的義務會讓結論最多停在 CONDITIONAL。
GAP GRAPH · v1.13
還剩什麼，依類別列出
每次執行都展開成 AND／OR 未決義務圖，每個義務標上 GAP 類別 G0–G10。宣告的研究缺口只能透過它綁定的形式命題解除；把它展開成子缺口只是計畫，什麼也不會解除。
REASSESS · v1.13
會自我檢查的捷徑
felra ppv-reassess 只重算受變更影響的部分，然後檢查結果等於全量重算、每個改變的狀態都在受影響集合內。同一版本號下原地改寫命題，會被報為違規。
ALIGNMENT · v1.14
證的是對的問題嗎？
沒有機器能證明一句話等於一個公式。FELRA 讓形式化對齊讀者宣告的量詞、型別與定義域（由 z3 比對）、這句話已經判定的點（精確求值），以及獨立寫出的其他形式化（由 z3 逐點比對）。關鍵詞只當提示。
GOAL GATE
局部不等於全域
RUN_FINISHED、LOCAL_VERIFIED、ORIGINAL_GOAL_VERIFIED 分開報告，並指出每個被引用命題的作用域和目標差在哪。形式目標已驗證、卻沒對齊原句的，維持 GOAL_BRIDGE_OPEN。
TRUST_CONFLICT · v1.15
錯的是誰——並且驗證
同時被證明又被推翻的命題會被隔離，任何東西都不能建立在它上面。FELRA 從精確反例點指出被它否定的來源——基礎公理、證的其實是另一個陳述的證書、出錯的核驗器或求解器——再撤掉它重新評估。只有能消解矛盾的診斷才算 CONFIRMED。
PPV-VERIFY
只憑產物重驗
felra ppv-verify 重跑精確核驗器、重建每個 SMT 義務與 Lean 檔並逐位元比對、不靠求解器重驗求解器的模型，並重推每個狀態與每個診斷。它會明說有幾個判定建立在它沒有重跑的證明器上。
965353da a2b4371b b8120097 e89a5d98
felra ppv-verify — 40 項檢查全部通過：兩個診斷都從收據重新推導、FELRA 自己寫的 Lean 檔從命題重建、被引用的 Lean 檔對上 Lean 讀過的副本。有 2 個判定建立在 z3 的 unsat 上、2 個建立在 Lean 檢查過證明上——都對上了它們的檔案，但沒有重新推導。加上 --rerun-smt（把它們交回 z3 與 Lean 重跑）時，47 項全部通過。核心推導出的狀態與理由
- CONFLICT「沒有一個五次方等於四個依序排列的五次方之和」——由公理經 z3 認證的蘊含推出，卻被 27⁵ + 84⁵ + 110⁵ + 133⁵ = 144⁵ 推翻。診斷沿著蘊含往回追，發現公理在這一點不成立，指認它為
FOUNDATION_INCONSISTENT。撤掉它，命題成為 REFUTED——確認。 - BLOCKED建立在它上面的命題被隔離——不會透過一個矛盾中的前提變成 VERIFIED。
- CONFLICT對所有整數 a − b ≤ a——被 Lean 的
Nat.sub_le「證明」，又被 a = 0, b = −1 推翻。SPEC_MISMATCH：那個定理講的是 ℕ 不是 ℤ，而 b = −1 不是自然數。確認。 - NO VERDICT同一個命題、陳述由 FELRA 寫出的 Lean 證明，如它應該的那樣失敗：綁定的陳述不會偏離命題。
- VERIFIEDa − b + b = a，由綁定的 Lean 證明與多項式正規形各自證明。
f20f017e 82621afb 56343524 d603f0c2
felra ppv-verify — 63 項檢查全部通過，包括從命題重建的 10 個 SMT 義務，以及一個不靠 z3 重驗的 z3 反例模型。有 4 個判定建立在 z3 的 unsat 上，它能把它們對上義務檔，但無法重新推導。核心推導出的狀態
- VERIFIED四道整數「牆」之間的常數差，由正規形與 z3 證明；雙平方閘門的因式分解，由正規形與 SymPy 證明；兩條 Cayley 參數化恆等式，由 z3 證明。
- REFUTED「每個 p ≡ 3 (mod 4) 的質數至多整除一道牆」——精確見證 (u₁, v₁, u₂, v₂, p) = (3, 5, 2, 7, 3)，同一見證也推翻它的成對乘積版本。另一個落在定義域邊界上的「見證」被拒絕。
- REFUTED把 Cayley 點平方後仍當成同一點——由 t = 1/2 推翻，也由 z3 自己找到、經精確重驗的反例 t = −1 推翻。
- BLOCKED依賴被推翻引理的搜尋剪枝規則——被阻擋而非被推翻，也沒有連累那些恆等式。
- OPEN完美長方體本身。有界的 z3 搜尋沒有判定；一條論證用了未經檢查的方法，另一條不符合 implication 的契約。
LIVE REPRODUCIBILITY CHECK · 證據總帳
不是行銷數字——是在真實機器上重新跑出來的證據
以下紀錄取自 examples/reproducibility 範例專案，於 2026-07-20 以 FELRA v0.7.0 完整執行、獨立重播並匯出論文包。
x ** 2 >= 0）——在宣告的取樣預算內未發現反例。這是計算證據，不是數學證明。9e4817f6 af425cb0 77a9e3c7 0f12608b
felra replay artifacts/reproducibility — 重新計算的結果雜湊逐位元組相同。felra export 產出 18 個索引檔案：Methods、Results、Limitations、CITATION、圖表、報告與檔案雜湊。
快速開始
從安裝到第一份證據包
原始碼儲存庫目前為私有，以下步驟適用於有存取權的協作者。
01 · 安裝
$ python -m venv .venv $ .venv\Scripts\activate # Windows $ source .venv/bin/activate # Linux / macOS $ pip install -e ".[dev]"
02 · 建立並執行第一個專案
$ felra init my-theory $ felra run my-theory/project.yaml \ --output my-theory/artifacts/run
03 · 跑內建範例
$ felra run examples/data/project.yaml \ --output artifacts/data $ felra batch examples/repeated_batch/batch.yaml \ --output artifacts/repeated --workers 2
04 · 預註冊、重播與匯出（v0.7）
$ felra verify-preregistration project.yaml \ --record preregistration.json $ felra replay artifacts/run --output artifacts/replay $ felra export artifacts/run --output artifacts/paper
05 · 證明過程驗證（v1.9 起，需要 z3）
$ felra run examples/ppv_c3/project.yaml \ --output artifacts/ppv_c3 $ felra ppv-verify artifacts/ppv_c3
06 · 信任衝突與 Lean（v1.15 起，需要 z3 與 Lean 4）
$ felra run examples/ppv_conflict/project.yaml \ --output artifacts/ppv_conflict $ felra ppv-verify artifacts/ppv_conflict --rerun-smt
SCIENTIFIC BOUNDARIES · 驗證與統計邊界
FELRA 不會幫你誇大結論
這是一個學術驗證工作台，不是證明產生器。以下邊界寫在 AGENTS.md 裡，同樣的規則也管束任何在這個專案上工作的人或代理人。
FELRA 的 Python 結果是有限資料、有限精度、有限預算與特定統計假設下的計算證據，不等同於一般數學證明。
p 值不是「假設為真的機率」；拒絕虛無假設不自動建立因果關係。
未拒絕虛無假設，不代表兩者等價——「找不到反例」不會被改寫成「定理已證明」。
展示用的合成資料集必須維持標註為合成，不能被當成實證證據使用。
重播（replay）比對證明的是同一環境下的計算可重現，不是外部複現、科學有效性或普遍證明。
一次執行符合它宣告的預期，不等於證明了它的原始目標。已驗證的局部命題永遠不會把目標往上提升；報告把兩者分開陳述。
雜湊鏈只表示紀錄寫下後沒被改過，不表示紀錄的內容為真。z3 的 unsat 是求解器對「義務檔原文」的判定；FELRA 記下是哪個程式本體、哪份義務，但不重新推導它。
形式命題被驗證，不代表它就是原本被問的問題。原始目標綁了自然語言陳述時，只有形式化也對齊了那句話，目標才算驗證——而對齊是拿讀者明確宣告的承諾來檢查，不是證明「意義相同」。
不是 FELRA 寫出的 Lean 定理，和它被引用來支持的命題之間沒有綁定：Lean 檢查的是某個陳述。收據會記下是哪一個，並註明它沒有綁定。
版本弧
從 MVP 到證明過程驗證
v0.1–v1.0（2026 年 7 月）完成白皮書階段 2 路線圖的 V0–V8 證據通道。v1.1–v1.8（8 月）加入外部形式化檢查器、精確與任意精度數值、可重驗證書與證明義務匯出。v1.9–v1.11（10 月）加入證明過程驗證層；v1.12–v1.15 讓每條論證都成為可檢查方法的一次應用、以未決義務圖追蹤還剩什麼、讓形式化對齊被問的問題，並診斷矛盾。每一步都附一套演練，在程式碼裡植入缺陷、要求每個都被對應命名的測試抓到——22、17、10、9、18 個缺陷，全部抓到。
v1.15.0 – v1.15.2 2026-10-19 · 信任衝突的診斷
證明與反例互相矛盾時，核心隔離該命題、指出精確反例點否定的來源，並以撤掉它來確認。Lean 4 證書：由 FELRA 寫出陳述的（綁定）與引用現成定理的（不綁定）。1.15.1 起，felra replay 讀取執行目錄內被引用 Lean 檔的副本。1.15.2 起，兩個形式化只在相同的判定域上比較——判定域不同的兩個成立命題，不再被算作一致。345 項測試。
v1.14.0 2026-10-19 · 自然語言到形式命題
對齊紀錄讓形式化對上讀者宣告的讀法，以及這句話已經判定的點。完美長方體問題的一個形式化忘了「正」，就被退化長方體 (0, 3, 4) 真的證明了——並被拒絕當作原問題的答案。
v1.13.0 2026-10-19 · GAP 圖與 REASSESS
未決義務以帶 G0–G10 類別的 AND／OR 圖呈現；宣告的研究缺口只能透過綁定的命題解除；增量重算會拿全量重算檢查自己。
v1.12.0 2026-10-19 · 五項義務機器化
七種方法，每次應用都由 O_pre、O_dir、O_bridge、O_cover、O_trust 判定。巢狀量詞、公理與假設、釘住求解器程式本體的信任政策、窮舉搜尋。方法適用性案例 T1–T10 以真實數學跑完。
v1.11.0 2026-10-19 · 目標閘門會解釋自己
對每個被引向原始目標的已驗證命題，報告指出它的作用域差在哪——量詞、變數、型別、定義域、基礎。附 PPV 文件。255 項測試。
v1.10.0 2026-10-19 · PPV 一致性驗收
完美長方體參考專案（17 項宣告預期）；C01–C12 閘門與竄改測試，包括整條重建的帳本與摘要正確的偽造收據；22 個缺陷的演練，22/22。
v1.9.0 2026-10-19 · 證明過程驗證
命題版本、證據收據、推導每個狀態的核心、由核心建出並經 z3 認證的 implication 橋接、雜湊鏈帳本，以及 felra ppv-verify。
v1.8.0 2026-08-21 · 證明義務匯出
把命題轉成斷言其否定的 SMT-LIB2，並與鑑別孿生一起檢查，空定義域永遠不會被當成證明。
v1.2.0 – v1.7.0 2026-08-18 · 數值表示與證書
宣告式數值政策；精確 Decimal／Rational 與 mpmath 後端；精度階梯；從自身資料重驗的區間與數值證書；外部多精度資料接入。
v1.1.0 2026-08-18 · 外部形式化後端
透過封閉轉接器集合呼叫 Lean、TLC 與 z3，每個檢查器以程式本體的雜湊識別；Lean 公理稽核於 v1.3.1 加入。
v1.0.0 Cross-Method Consistency (V8) · 階段 2 完成
獨立方法一致性檢查（numeric／symbolic／high_precision 後端）補齊了完整的 V0–V8 驗證通道。新增 6 項回歸測試——累計 51/51。
v0.9.0 Numerical Soundness (V3)
溢位／NaN 偵測、精確導數條件數、float64 對任意精度的災難性抵銷偵測。新增 5 項回歸測試。
v0.8.0 Symbolic Verification (V2)
透過 SymPy 做代數恆等與導數的精確驗證，支援每變數假設宣告——在整個宣告域上補足取樣式通道。新增 7 項回歸測試。
v0.7.0 Preregistration, Provenance, Replay & Paper Export
不可變科學計畫預註冊、JSON／DOT／SVG 證據溯源圖、穩定 result_sha256、felra replay 與 felra export。33 項回歸測試。
v0.6.0 Effect Sizes, Cross-Validation & Registry
Bonferroni／Holm／Benjamini–Hochberg 多重比較校正、標準化效應量、洩漏感知交叉驗證、append-only 實驗登錄。
v0.5.0 Power, Robustness & Cache
JSON／JSONL／gzip 資料集、noncentral-t 與 Fisher-z 檢定力分析、bootstrap／subsample 穩健性分析、內容定址快取。
v0.4.0 Data, Statistics & Replication Pipeline
型別化外部 CSV 資料集、資料列命題、分組描述統計、假設檢定家族、百分位 Bootstrap 信賴區間、重複實驗與並行批次。
v0.3.0 Sensitivity, Residual & Pareto
局部敏感度、殘差分析、參數掃描、精確雙目標帕雷托前沿、felra batch。
v0.2.0 Executable Project Specs
可執行的 project.yaml、安全 AST 表達式求值、felra run 與專案級 Evidence Bundle、多種圖形輸出。
v0.1.0 Initial MVP
Python 優先研究工作台的最初版本。