---
title: "ARKE-05｜跨表示研究同一性：定理、演算法、方法與證據的結構比較"
english_title: "ARKE-05 | Cross-Representation Research Identity: Structural Comparison of Theorems, Algorithms, Methods, and Evidence"
series: "ARKE Research — AI 原生自主科研完備與知識演化論"
series_english: "AI-Native Research Completion and Knowledge Evolution"
series_id: "ARKE"
paper_id: "ARKE-05"
series_part: "第二部：AI 自主查核與雙向知識檢驗"
sequence: 5
series_total: 12
author: "Neo.K with GPT（AI 協作）"
institution: "EveMissLab／一言諾科技有限公司"
version: "v0.1"
date: "2026-10-28"
timezone: "Asia/Taipei"
language: "zh-TW"
status: "FORMAL_RESEARCH_MANUSCRIPT_V0.1; THEORY_AND_METHOD_PROPOSAL; EMPIRICAL_VALIDATION_NOT_RUN"
document_type: "跨表示研究同一性理論／有型別研究比較／見證與反例契約／可否證實證設計"
canonical_source_encoding: "UTF-8"
canonical_math_delimiters: "inline= $...$ ; display=$$...$$"
source_verification_cutoff: "2026-10-28"
repository_policy: "ARKE 軟體工程獨立於十二篇研究；本文不宣稱演算法已整合至 GitHub、EveTrain 或數學 AI"
license: "作者權利保留；正式授權條款尚未決定"
---
# ARKE-05｜跨表示研究同一性：定理、演算法、方法與證據的結構比較
## Cross-Representation Research Identity: Structural Comparison of Theorems, Algorithms, Methods, and Evidence
**系列：** ARKE Research，第 05／12 篇
**作者：** Neo.K with GPT（AI 協作）
**機構：** EveMissLab／一言諾科技有限公司
**日期：** 2026 年 10 月 28 日（Asia/Taipei）
**研究狀態：** 正式理論與方法論原稿 v0.1；本篇 H1–H8 尚未執行，不以概念例子代替實證。
**承接：** ARKE-01（受約束研究完備）、ARKE-02（合法知識可達性）、ARKE-03（來源定址與研究依賴）、ARKE-04（先例發現與新穎性查核）。
**後續：** ARKE-06（多元研究驗證）、ARKE-07（雙向知識修正）、ARKE-08 至 ARKE-12（歸屬、演算法、演化與跨域實證）。
**版本：** v0.1
---
# 摘要
AI 自主研究的先例搜尋不能止於找到標題相似的論文。兩份研究可能以不同語言、符號、公理化、計算模型、資料表示或證明技術，陳述實質相同的結論；也可能使用幾乎相同的詞語，卻因量詞、成立域、隱含假設、成功機率或物理詮釋不同，而構成不可互換的研究成果。若 AI 將「文本相似」誤認為「研究同一」，可能抹去先例與獨立貢獻；若把「形式證明通過」誤認為「全部研究內容同一且正確」，則可能進一步誤判歷史成果、計算複雜度與實證支持。
本文提出 **ARKE 跨表示研究同一性契約**（Cross-Representation Research Identity Contract, **CRRIC**），作為 ARKE-04 先例候選檢索之後、ARKE-06 各類有效性驗證之前的研究比較層。其主要工作不是宣稱存在一個可以自動判定所有數學定理、程式與科學理論是否等價的萬用算法，而是提供**有型別、具作用域、帶見證、可反駁、可追溯且允許未知**的比較程序。
本篇區分：作品身分、文字／表示相同、命題等價、單向蘊涵、方法承接、演算法外延行為、計算成本、證明有效性、證據支持以及歷史優先權。本文進一步提出共同語義契約、跨語言／跨形式系統翻譯見證、命題雙向蘊涵義務、演算法操作契約、證明與方法的獨立比較、實驗結果的操作化比對、歷史版本反向追蹤及衝突保留程序。
由此可把「兩份論文是否一樣」改寫為：**兩個被精確定位的研究主張，在什麼共享假設、什麼語義轉譯、什麼適用域與何種可檢驗證據下，成立哪一種關係？** 本文提出十項可由定義、反例或有限構造支持的條件命題，並規劃八組可否證實驗，以測試相對於純文本向量相似度、單一形式化後判等及只憑引用圖查找的比較收益。所有相關實證均維持 `NOT_RUN`。
**關鍵詞：** ARKE、跨表示研究同一性、研究主張、語義保持、命題蘊涵、定理對齊、演算法外延等價、操作等價、方法先例、證據關係、學術新穎性、形式化驗證、反例、研究可追溯性。
---
# 0. 研究定位、主張分型與方法邊界
## 0.1 要解決的問題
對於兩項研究候選 $a$ 、 $b$，一個具備自主科研能力的 AI 應能回答：
1. 兩者是否指向同一作品、同一版本或同一來源片段？
2. 如果作品不同，兩者是否對**相同任務或現象**提出可比較主張？
3. 使用不同語言或符號時，是否存在可靠的語義保持轉譯？
4. 在指定假設和成立域下，主張是等價、單向蘊涵、局部重疊、矛盾，還是不可比較？
5. 即使結論相同，證明路徑、演算法、算力成本或實驗證據是否不同？
6. 存在較早的相同主張時，其證明是否已完成，或只是一項未驗證的歷史嘗試？
7. 如果目前無法判定，應保存什麼未知、缺口與後續查核義務？
8. 比較結論如何接回可回訪原文、歷史版本與研究依賴證據？
本篇主張：上述問題是**多層關係辨識**，不能被壓縮成「語義向量相似度超過閾值就合併兩篇論文」。
## 0.2 主張類型標記
本文採用下列區分，避免將研究建議寫成已證實的普遍定理：
| 標記 | 含義 | 可用的支持方式 |
|---|---|---|
| `D` | 定義或研究物件 | 明確指明型別、上下文與比較條件 |
| `N` | 規範或設計原則 | 陳述適用理由、取捨與限制 |
| `P` | 條件命題、邏輯事實或反例推論 | 在列明前提下進行論證 |
| `H` | 尚待驗證的經驗假說 | 預註冊對照、保留集、測量與失敗準則 |
| `B` | 不可推出的結論及方法邊界 | 反例、不可判定性或證據不足 |
`P` 不等於本文已執行 Lean／Coq／Isabelle／SMT 的機器證明；除非明確提供可重播機器產物，否則只聲稱本文的文字論證。`H` 的預期方向不能被當成已測結果。
## 0.3 三項不取代
本文**不取代**既有的：
- 自動定理證明、形式邏輯與 proof assistant；
- 程式語義等價／翻譯驗證（translation validation）；
- 學術搜尋、書目引用索引、研究資料管理與 provenance 標準。
跨 proof assistant 的概念對齊已有具體研究，例如 Gauthier 與 Kaliszyk 比較六種形式證明庫內的相近概念與同構候選 [R1]；程式最佳化後的語義保持檢查已有 Necula 的 translation validation 工作 [R2]；物理理論的經驗、定義與範疇等價亦有成熟的哲學與形式研究 [R3][R4]。本文的新候選貢獻，是將相關思想放在**AI 自主學術先例查核**所需的統一、受限制且可稽核的研究流程內，而不是主張這些既有方法由 ARKE 首創。
---
# 1. 為何「找到相似論文」不是完成研究同一性查核
## 1.1 相同字詞可對應不同研究命題
假設兩篇論文均寫出「在多項式時間內完成」。第一篇所稱的多項式時間可能依輸入長度 $n$ 衡量，第二篇則可能把預計算資料、外部 oracle 或資料編碼成本排除在外。即使自然語言表面相同，兩者也未必指涉相同的可計算性主張。
同樣地，實驗報告中的「有效」可能表示統計顯著、臨床重要、工程可部署或在特定資料分布下有效。未記錄操作定義時，文字等同不保證研究等同。
## 1.2 不同表示亦可承載相同主張
一項圖論性質，可以用自然語言、集合論表示、型別理論、TPTP 形式化語句或圖像化結構敘述。在有適當翻譯及語義橋接時，這些形式可能對應同一研究內容。
但僅看到符號相似、或翻譯模型生成看似通順的文字，不能直接斷定其語義保持。必須檢查邏輯基礎、定義和暗中帶入的前提。
## 1.3 同一結論不等於同一研究貢獻
兩個研究者可能獨立證明同一命題：
- 早期工作有正確而較長的證明；
- 後期工作有較短或更容易形式化的證明；
- 或早期只提出猜想，後期首次給出有效證明。
在這些情況下，「結果的先例」、「方法的先例」與「成功證成的先例」不應被混為一個欄位。ARKE-04 已區分四種先例，本篇負責提供更嚴格的**關係見證**，而非替歷史研究者直接分配學術權威。
## 1.4 比對的基本單位是具體主張，而非作品整體
一篇論文可能同時提出定理 A、推論 B、數值實驗 C 及方法 D。即使定理 A 與另一論文完全相同，也不能直接推論兩篇作品全部等價。
研究比較的最小單位應是 ARKE-03 的 **L4 研究主張**，並透過 L0–L3 定位原作品、版本、載體與片段；L5 紀錄該比較的證據及歷程。作品級關係可以由多筆經查核的主張級關係彙整，但不能反向取代它們。
---
# 2. 與 ARKE-01 至 ARKE-04 的嚴格接口
## 2.1 研究完備契約不作任何新穎性捷徑
ARKE-01 定義受約束研究完備為：
$$
\mathrm{RC}_{\Gamma}(r,\pi)=1
\iff
\mathrm{Freeze}(r,\pi)
\land \mathrm{ScopeMatch}(r,\Gamma,\pi)
\land \bigwedge_{o\in\mathcal O_{\mathrm{hard}}}
[\sigma(o,\pi)=\mathrm{PASS}].
$$
ARKE-05 **不重定義**這個完成契約；它只為其中「前置先例比較／研究同一性查核」義務提供有型別輸出。即使跨表示比較通過，也不能單獨宣稱研究在所有意義上正確、全域首次或具備發表資格。
## 2.2 來源可達性與同一性是不同的前提
沿用 ARKE-02：已知某篇論文的存在，不代表有權取得其全文；可取得全文也不代表已理解其主張。在只讀到題名或摘要的情況下，系統可以提出 `COMPARISON_CANDIDATE`，但不得聲稱完成深層定理等價性驗證。
## 2.3 使用 ARKE-03 的 Research Trace Anchor
ARKE-03 定義研究錨點：
$$
A=\langle w,v,m,\ell,\sigma,h,t,\rho,\pi\rangle.
$$
本篇直接沿用 $w$ （作品）、 $v$ （版本）、 $m$ （載體）、 $\ell$ （定位）、 $\sigma$ （片段選擇器）、 $h$ （完整性指紋）、 $t$ （時間）、 $\rho$ （權利）、 $\pi$ （歷程），不建立一套互相競爭的學術識別體系。
一筆跨表示關係必須能返回支撐其判定的**兩側來源錨點**及實際比較工件。來源被撤回或修訂時，舊關係可保留歷史狀態，但其目前可用性須重新查核。
## 2.4 接受 ARKE-04 的暫定關係，不偷換證據層級
ARKE-04 已提出初步關係：`related`、`same_claim`、`stronger`、`weaker`、`method`、`attempt`、`counter`、`unknown`。本文把它們展開成具備**方向、前提、見證與不確定性**的查核狀態。
例如 `same_claim` 原可作為檢索後的候選；本篇若沒有形式證明、可信的有限窮舉、可重播反例或足以支持領域特定結論的證據，仍必須保留 `PENDING_EQUIVALENCE`，而不是把候選關係升級為全域同一。
## 2.5 本篇與 ARKE-06 的分工
ARKE-05 主要回答：**兩個主張之間可證成哪一種關係？**
ARKE-06 將進一步回答：**該主張自身在指定領域、證據與驗證方法下是否成立？**
兩者可互相提供線索，但不可互相取代。即使 $a$ 與 $b$ 在某套假設下等價，也可能兩者都不符合外部現實；即使 $a$ 已被驗證，也不代表其與 $b$ 的關係已被核對。
---
# 3. D1：研究比較對象與不可混同的身分軸
## 3.1 四種研究內容軸
令單項研究主張物件 $c$ 為：
$$
C(c)=\langle I_c,S_c,M_c,P_c,E_c,H_c\rangle.
$$
其中：
- $I_c$：沿用 RTA 的來源身分與片段定位；
- $S_c$：研究所主張的命題、任務、模型及適用域；
- $M_c$：方法或演算法的實際構造；
- $P_c$：證明、推導或論證工件；
- $E_c$：可檢查的經驗、計算或形式化證據；
- $H_c$：研究歷程、版本與時間資訊。
這六個欄位並非要求每個領域都具備完全相同的資料型態；某些論文沒有程式碼，某些實驗沒有形式證明。在缺少對應內容時應填 `NOT_APPLICABLE` 或 `UNKNOWN`，而不是捏造假資料。
## 3.2 同一性不能只有一個值
對兩項研究 $a,b$，本篇提出比較向量：
$$
\mathcal J(a,b\mid\Lambda)
=\langle J_I,J_S,J_M,J_P,J_E,J_H,U\rangle.
$$
其中 $\Lambda$ 是第 4 節的比較契約， $U$ 為未知與未完成義務。各維度的結果為**型別化關係及證據狀態**，不是預設可相加的六維分數。
重要區分如下：
| 比較維度 | 問題 | 即使為真，也不能推出 |
|---|---|---|
| $J_I$ 來源同一 | 是否同作品、版本、檔案、片段？ | 命題正確、證明有效 |
| $J_S$ 主張關係 | 是否具有相同的數學／科學內容？ | 使用相同方法或有相同證據 |
| $J_M$ 方法關係 | 是否使用相同的計算構造與研究策略？ | 結論等價或計算成本相同 |
| $J_P$ 證明關係 | 是否為相同／可轉換的論證？ | 原始學術首次性 |
| $J_E$ 證據關係 | 是否測量同一效應、共享或複現證據？ | 因果機制相同 |
| $J_H$ 歷史關係 | 是否早於、承接或獨立於另一項工作？ | 技術抄襲、正確性或學術應有權利 |
同一份研究可同時滿足「主張相同」「方法不同」「證明獨立」「證據互補」。資料模型不得強迫只選一種。
## 3.3 「同一」的範圍須被限定
一個詞可能在不同研究社群中有不同意義，例如 `equivalent` 可表示：
1. 位元組或文字內容完全相同；
2. 允許重命名、重排或記號改寫後相同；
3. 在明確公理／定義下邏輯上等價；
4. 對所有指定輸入產生相同行為；
5. 在某個實驗域中產生相近觀測；
6. 在相同研究問題上達到類似實用效果。
六者不形成毫無例外的同一強弱排序。第 5、6 類尤其容易受容許誤差、資料分布與外部有效性影響；第 4 類可能要求無法一般判定的程式語義性質。
---
# 4. D2：共同比較契約（Comparison Contract）
## 4.1 比較之前先固定「比較什麼」
定義：
$$
\Lambda=\langle
\mathcal T,\mathcal D,\Gamma,\mathcal L,\tau,
\mathcal O,\mathcal R,\delta,\mathcal V,\mathcal P
\rangle.
$$
- $\mathcal T$：原始任務、研究對象及預期輸出語義；
- $\mathcal D$：輸入／現象的共同成立域，包含排除條件；
- $\Gamma$：可接受的公理、定義、背景假設與前提；
- $\mathcal L$：邏輯基礎、語義解釋與公式所在語言；
- $\tau$：跨表示、跨語言、跨模型的翻譯及其驗證見證；
- $\mathcal O$：必須保留的可觀測量、輸出和成功判準；
- $\mathcal R$：資源度量、計算機型、預計算與外部資訊規則；
- $\delta$：明定的數值容差、統計門檻或近似關係，若不適用則為空；
- $\mathcal V$：可使用的驗證方法、信任邊界與證據層級；
- $\mathcal P$：來源取用、授權、保存與重新使用限制。
**D2（Contract-Scoped Comparison）。** 只有在 $\Lambda$ 的必要欄位已明確、兩邊研究物件有足夠內容支持比較時，才可以輸出超越「候選相關」的關係裁決。
若其中關鍵欄位未知，系統不得因語言模型偏好某個解釋而偷偷補上。它可以嘗試檢索補件，也可以保留多個合理的比較契約，但不可把不同契約的結論當作同一關係。
## 4.2 非平凡性與一致性義務
如果欲在某個背景理論 $\Gamma$ 下推導 $a\leftrightarrow b$，必須注意：在經典邏輯中，若 $\Gamma$ 不一致，任何公式都可能由爆炸原理導出。故本篇要求至少另附：
$$
\mathrm{Consistent}(\Gamma)
\quad\text{或}\quad
\mathrm{ModelWitness}(\Gamma).
$$
這裡 `Consistent` 的來源與證明方法也必須被檢查；如未能建立，應標記 `BACKGROUND_CONSISTENCY_UNRESOLVED`。存在一個可信模型可作為指定語義下的非空性／可滿足性見證，但並不直接解決所有基礎邏輯體系的元數學問題。
若兩篇論文的前提不同，不能簡單把 $\Gamma_a\cup\Gamma_b$ 當作共同背景，除非這個聯集的合法性與語義影響已有查核。尤其在實驗研究中，將兩項互不相容的資料生成假設取聯集，可能導致虛假的比較。
## 4.3 成本契約不能從比較中消失
在理論計算機科學中，兩個演算法即使計算同一函數，也可能存在完全不同的時間、空間、查詢、能源與預先知識需求。沿用 UCPNP／UNPNP 的研究提醒：
$$
\mathrm{SameOutput}(A,B)
\not\Rightarrow
\mathrm{SameCost}(A,B).
$$
因此對「更快」或「更容易」的比較，必須指定成本是每次查詢、初始化加查詢、攤銷成本，還是整個跨時間系統的總成本。不可將預計算／資料庫／oracle 的成本無聲排除。
## 4.4 單位、尺度與物理詮釋契約
在物理或實驗科學中，表面相同的式子若單位、規範、儀器校準或有效尺度不同，可能不能互換。特別應檢查：
- 測量的同一物理量是否具有可追溯單位對應；
- 坐標、規範及正規化是否改變可觀測結論；
- 模型的近似階數與有效域是否一致；
- 統計估計量是否指向同一母體參數；
- 觀測一致是否僅止於某個有限實驗條件。
本篇不預設「觀測等價」就是「理論本體同一」。物理理論等價的多個概念在既有研究中已被分開討論 [R3][R4]。
---
# 5. D3：由弱線索到強關係的型別化比較階梯
## 5.1 不等價的八種比較層
建議至少保留：
| 型別 | 最低支持 | 仍然缺少什麼 |
|---|---|---|
| `BIBLIOGRAPHIC_MATCH` | 可信身分與版本資料 | 具體主張與證據 |
| `TEXTUAL_OR_STRUCTURAL_SIMILARITY` | 可回訪片段及相似特徵 | 語義保持與等價證明 |
| `TRANSLATION_CANDIDATE` | 明確轉譯候選與詞彙映射 | 翻譯正確性的見證 |
| `DEFINITIONAL_EQUIVALENCE` | 在固定形式系統內可檢查的定義相等 | 外部詮釋與跨體系同一 |
| `LOGICAL_EQUIVALENCE` | 兩個方向的有效推導及背景約束 | 歷史首次、方法與實驗有效性 |
| `ONE_WAY_ENTAILMENT` | 經認證的單向推導 | 反向成立或嚴格強弱 |
| `BEHAVIORAL_EQUIVALENCE` | 操作語義下的功能或可觀測等價見證 | 相同複雜度、相同程式構造 |
| `EMPIRICAL_COMPATIBILITY` | 指定實驗設計、容差與不確定度下的相容性 | 完整理論等價或因果同一 |
此表只是不同關係的類型列舉，不表示每一行都能在線性序列中自然晉升到下一行。例如兩個實驗模型的觀測相容性，不必然具有一個可被同一 proof assistant 解析的定理語句。
## 5.2 加入可反駁的負面關係
為避免「只有等價／未知」，還必須支援：
- `NOT_EQUIVALENT_WITH_WITNESS`：已有符合共同語義契約的有效區分見證；
- `CONTRADICTS_UNDER`：在共同假設及可比較域內存在邏輯或觀測衝突；
- `INCOMPARABLE_UNDER`：缺乏必要的共同任務、翻譯或統一語義；
- `OVERLAP_WITHIN_SCOPE`：在具體、非空的子域已建立共同關係，但全域關係未確定；
- `PARTIALLY_OVERLAPS_WITH_SEPARATION`：已建立非空交集且有合格見證表明兩者在其他子域有實質差異；
- `UNKNOWN`：資料、模型或驗證能力不足，保留未決。
`OVERLAP_WITHIN_SCOPE` 不應被自動改標為 `PARTIALLY_OVERLAPS_WITH_SEPARATION`：**目前只知道某個交集，並不代表已證明交集以外必定有差異。**
## 5.3 每種關係都要伴隨可檢查義務
以型別化裁決物件表示：
$$
J_{\Lambda}(a,b)
=\langle k,d,w,e,s,u,\pi\rangle,
$$
其中 $k$ 為關係型別、 $d$ 為方向、 $w$ 為見證或反例工件、 $e$ 為來源與核驗證據、 $s$ 為作用域、 $u$ 為剩餘未知、 $\pi$ 為研究歷程。
**N1（No Witness, No Upgrade）。** 只有相似度、模型口頭推論或檢索排序的關係，原則上維持 `CANDIDATE`；要升格為可檢查的邏輯等價或嚴格不等價，必須提供該類型允許的見證、驗證方法與信任前提。
但「一定要形式證明」不是本篇規範。對所有有限情況均已窮舉的結果、在指定實驗條件下有充分測量證據的觀測比較、或可重播的程式測試反例，都可在**各自宣稱範圍**內構成適當見證。
---
# 6. D4：跨語言、跨符號與跨表示的翻譯見證
## 6.1 翻譯不是字詞替換
假設主張 $a$ 使用語言 $L_a$，主張 $b$ 使用 $L_b$。要在共同語義域比較，至少需要明確描述映射：
$$
\tau_a:L_a\rightarrow L_*,
\qquad
\tau_b:L_b\rightarrow L_*.
$$
其中 $L_*$ 為受約束的共同比較語言或中介表示；不預設所有科學研究都適合完全轉成一階邏輯。翻譯工件須列明：變數與型別、量詞域、記號定義、單位、作用域及省略條件。
## 6.2 語義保持義務
對於一個受限、可比較的片段，可提出如下證明義務：
$$
\forall M\in\mathcal M_a,
\quad
M\models\varphi
\iff
F(M)\models\tau_a(\varphi).
$$
此處 $F$ 為經明確定義的模型或語義解釋映射。這是**候選語義保持契約的理想形式**，不是所有跨語言模型都已經存在此等價證明。若只能支持其中一個方向，必須標明 `ONE_WAY_TRANSLATION`；若只能在有限測例上核對，標為 `TESTED_TRANSLATION`。
## 6.3 避免量詞、否定及域的翻譯漂移
例一：
$$
\forall x\in D,\;P(x)
$$
不等於：
$$
\exists x\in D,\;P(x).
$$
例二：
$$
\forall x\in D,\;\neg P(x)
$$
不等於：
$$
\neg\forall x\in D,\;P(x).
$$
例三：在一般情況下，「對所有有限圖成立」不得未經額外證明直接改成「對所有圖成立」。
這些錯誤可能發生在翻譯、OCR、PDF 文字提取、公式圖像解析及模型自動摘要。它們不是排版瑕疵，而是研究主張身分的變化。
## 6.4 多模態不是文字化之後就自動等價
圖形、實驗影像、譜圖與示意圖可承載文字未完整描述的資訊。若研究比較依賴圖中某個曲線、區域或時間片段，應保存原始載體版本、定位區域及解析方式，並承認從圖像到文字的投影可能有資訊損失。
本篇允許：原圖與 OCR 文字並存、文字與數學式並存、程式碼與流程圖並存。它們的關係可以被驗證，但**任何單一投影都不自動取代原始研究表示**。
---
# 7. D5：數學定理的命題關係與雙向見證
## 7.1 比對共同命題，而非先比證明長度
設 $\varphi_a$ 、 $\varphi_b$ 分別是兩項研究的命題內容。若有經查核的共同比較背景與翻譯，可提出等價義務：
$$
\Gamma_*\vdash
\forall x\in D_*,\;
\left(\tau_a(\varphi_a)(x)
\leftrightarrow
\tau_b(\varphi_b)(x)\right).
$$
這裡的 $\Gamma_*$ 必須列出採用的公理、定義與所有必要前提； $D_*$ 是**明確指明的共同研究域**。若主張不是帶自由變數的述詞，可依其語法改寫為閉合命題的雙向蘊涵。此式並不是一個可以將任意自然語言直接丟入求解器的萬能公式。
嚴格的關係宣稱應包含兩個方向：
$$
\Gamma_*\vdash
\tau_a(\varphi_a)\Rightarrow\tau_b(\varphi_b),
$$
$$
\Gamma_*\vdash
\tau_b(\varphi_b)\Rightarrow\tau_a(\varphi_a).
$$
且兩邊的量詞、型別、定義域與翻譯見證必須相符。單獨用模型說「我認為是同一定理」，不能填補這兩個義務。
## 7.2 形式系統的信任邊界
Lean 的內核能檢查指定形式理論中的證明項，但官方文件也明確區分**內核接受證明**與**形式命題是否忠實表達研究者想說的非形式命題**，並提醒檢查所依賴的公理 [R5][R6]。
因此 ARKE 在形式查核通過時，至少仍記錄：
- 使用的形式語言、proof assistant、版本及引入的理論庫；
- 形式命題本身及其與原文的對應錨點；
- 公理依賴（例如是否有未完成 `sorry` 或自訂公理）；
- 翻譯／形式化過程及其歧義；
- 比較只涵蓋整篇研究的哪一個結論、哪個參數域。
**N2。** 一個形式定理被核驗，不等於其自然語言解讀與歷史新穎性都已被核驗。這不是貶低形式證明，而是將它放回正確的認識論作用域。
## 7.3 單向蘊涵與嚴格強弱
若：
$$
\Gamma_*\vdash\varphi_a\Rightarrow\varphi_b,
$$
則可以在共享語義域與假設下記錄 `a_entails_b`，但不能僅因未找到反向證明便宣布 $a$ **嚴格強於** $b$。
嚴格區分還需有合格反向失敗見證，例如某個滿足背景假設的模型 $M$：
$$
M\models\Gamma_*\land\varphi_b\land\neg\varphi_a.
$$
若有如此模型，才能排除該背景下的 $\varphi_b\Rightarrow\varphi_a$。若判定器只報 `unknown` 或超時，應保留反向未決。
簡單例子：在實數域內， $x>2$ 蘊涵 $x>1$ ；取 $x=3/2$ 可見反向不成立。但若文獻 A 只聲稱「在 $x\ge3$ 的條件下 $x>2$ 」，文獻 B 的前提也改變，則需要重新核對各自條件，不能只比較裸公式。
## 7.4 成立域與端點條件
研究 A 在 $D_a$ 成立、研究 B 在 $D_b$ 成立，即使文字結論相同，未必是全域等價。首先定義：
$$
D_*=D_a\cap D_b.
$$
可以先在非空共同域上比較，並把各自特有的區域分開追蹤。對調和分析、偏微分方程、數論、概率及複雜度理論而言，開區間／閉區間、端點、量詞順序、參數是否固定及常數是否均勻，都可能構成真正的研究差異。
當 $D_*$ 為空時，**以共同域為前提的等價主張不能獲得有內容的支持**。應回到是否存在合法、非平凡的域映射，而不是利用空域上的真空真值生成「相同成果」。
## 7.5 可決定片段與一般開放片段
在明確有限、封閉且可列舉的語義域中，系統可能透過完整窮舉比較所有情況；對某些可判定邏輯片段，可藉 SMT、決策程序或特定形式檢查器產生有效見證。SMT-LIB 為此類可互操作的求解問題提供標準語言，但求解器所支持的理論、決策能力與回傳狀態仍需依使用情境核對 [R7]。
對任意高階數學、包含無窮結構或涉及未解決命題的比較，不可假設存在總能終止且正確給出等價／不等價的算法。**可決定片段的成功不得泛化為全域判等能力。**
---
# 8. D6：演算法的輸出等價、操作等價與複雜度差異
## 8.1 演算法比較先固定任務語義
一項演算法候選至少需明確列出：
$$
\mathfrak A=
\langle X,Y,F,M,C,\epsilon,R,E\rangle.
$$
其中：
- $X$：合法輸入及其編碼；
- $Y$：預期輸出與輸出編碼；
- $F$：被計算的函數或關係；
- $M$：抽象計算模型（例如隨機存取機、圖靈機、平行、量子、oracle 等）；
- $C$：時間、空間、查詢及其他資源的計量規則；
- $\epsilon$：確定性、隨機錯誤、近似或容忍度條件；
- $R$：允許的先備資料、預計算、外部資訊與權利限制；
- $E$：可重播的實作、定理、測試或證明工件。
若 A 解的是 SAT 判定、B 解的是 #SAT 精確計數，兩者具有明確的**任務歸約關係**，但輸出型別並不相同。尤其不得因為「計數不為零可判定可滿足」，就宣稱兩套演算法在所有計量與功能意義上完全一致。
## 8.2 外延等價與實作等價
若 $f_a,f_b$ 為同一輸入集合上的**全函數**，外延等價可定義為：
$$
\forall x\in X,\quad f_a(x)=f_b(x).
$$
若為部分函數，還須要求定義域／終止性一致，且在共同已定義輸入上輸出相同；若為有狀態、互動式、概率式或併發系統，則須指定 trace、觀測及容許的抽象關係。
兩個程式實現相同數學函數，卻可能是完全不同的演算法，並非同一段程式碼，也未必具有相同的時間或能源特徵。更不能只憑相同測試集通過就認定外延等價。
## 8.3 隨機化與確定性不能靜默合併
即使兩種方法對同一任務輸出相同，若其中一種只以特定成功機率成立，則研究主張須記錄：
$$
\Pr[A(x)=F(x)]\ge1-\epsilon(n),
$$
以及該概率對哪些隨機來源、輸入分布、重複試驗或最壞輸入成立。對永遠正確但運行時間隨機的 Las Vegas 型算法，則不應套用相同的輸出錯誤語義。
把「隨機化」「零錯誤」「確定性」「近似」全部抹除，只留「次指數」三個字，會遺失研究成果的關鍵差異。
## 8.4 上界、下界與證明範圍的非對稱
若 A 被證明時間上界為 $O(n^2)$，B 被證明時間上界為 $O(n^3)$，**不能直接推出** B 的真實最壞時間一定比 A 慢：上界可能不緊。若要主張嚴格資源分離，需比較適當的下界、上界、統一成本模型、參數與演算法本身。
對複雜度主張，至少列出：
- 輸入大小究竟是變數數量、公式位元長度還是資料庫總大小；
- 參數是否固定，以及隱藏常數可能依哪些參數變化；
- 上界是否在全部輸入還是某些密度／分布條件下成立；
- 空間與資料初始化成本是否納入；
- 是否有有效的機器模型及實際構造；
- 形式化證明與自然語言論文的上界是否完全一致。
## 8.5 預計算與外部知識不可免費
假設演算法 A 線上查詢只需常數時間，但建立索引需要大量計算；B 不需預計算、單次查詢較慢。這可能是兩種不同的計算成本配置。若比較的是在線延遲，可合理得出 A 在某條件下較快；若比較完整成本，則須將索引建立與維護納入。
這不是對傳統複雜度理論的重新定義，而是要求 AI 清楚區分**抽象複雜度命題**與**真實系統成本命題**，避免發表時混用。
## 8.6 一般程式等價性的不可判定邊界
對任意圖靈完備程式，不能要求 ARKE 永遠自動決定它們是否計算相同部分函數。這與停機問題及非平凡程式語義性質的不可判定性有關；Rice 定理提供一般性的限制背景 [R8]。
較精確地說，若存在一個對任意兩個程式皆終止且正確判斷其部分可計算函數是否完全相等的程序，固定其中一個為特定常數函數後，便可用它判定非平凡語義性質，與相應不可判定結果衝突。因此本研究不能將「AI 會推理」等同「所有演算法都可以總判等」。
實際可行的策略是保留：可證明片段、受限語言的決策程序、可生成反例的測試、獨立形式驗證，以及 `UNKNOWN` 的停止狀態。
---
# 9. D7：證明路徑與方法同一性是獨立的研究對象
## 9.1 結論相同不表示證明相同
兩個有效證明 $p_a,p_b$ 可以證成同一命題 $\varphi$，但使用不同引理、不同分解、不同計算概念或不同公理化。其學術貢獻可能是：
- 降低外部假設或移除不必要的引理；
- 提供較短、更易理解或更可形式化的推導；
- 以新工具揭示此前未被注意的結構；
- 將局部結論推廣至更大但明確的成立域；
- 建立可重播的替代證明及錯誤定位機制。
因此 $J_S$ （主張等價）不能自動推出 $J_P$ （證明同一）或 $J_M$ （方法同一）。
## 9.2 方法比較的最低特徵
方法比較不應只分類為「代數方法」「分析方法」「深度學習方法」等粗類別。候選方法物件至少記錄：
1. 核心構造與實際使用的數學物件；
2. 必需的轉換、歸約、分解與中介引理；
3. 條件和不可去除的假設；
4. 主要證明責任與失敗情形；
5. 可回訪的關鍵步驟、程式碼或實驗協議；
6. 對舊方法的承接、替換或真正新增的部件。
一個 AI 可以先提出「方法結構相似」的候選，但如果無法指出對應的關鍵步驟，就只能保留為**結構類比**，不得宣稱同一方法、源自前人或抄襲。
## 9.3 Proof plan、proof term 與論證解說不同
在形式證明系統中，proof term 可以被檢查；但兩份 proof term 的位元組不同，不代表它們沒有共同邏輯結構。反過來，同一自然語言證明草圖可以由不同形式化完成，也可能根本不具足夠推導細節。
ARKE 建議保留三個層次：
- `PROOF_TERM_RELATION`：形式物件的可驗證關係；
- `PROOF_DEPENDENCY_RELATION`：必要引理、假設、技術步驟的對應；
- `EXPLANATORY_RELATION`：人類或 AI 可理解的推理脈絡與解釋。
三者不相互取代。TPTP 的定理證明問題庫與證明系統生態已提供可使用的既有語言和基準 [R9]；ARKE 應重用可用規格，而不是建立只在自己框架內有效的新型 proof language。
## 9.4 「證明有效」與「證明正是原作者那一個」分離
即使一份形式化重建證明了某個命題，也不能因此自動宣稱完整復現舊論文原證明的思路；可能僅是另一條獨立證明。同樣，新的解說雖與舊文相似，仍不能由此推出模型直接讀取或抄用了該來源。
本篇只在證據允許時建立 `USES_METHOD_FROM`、`SHARES_LEMMA`、`INDEPENDENT_RECONSTRUCTION_CLAIMED` 或 `UNRESOLVED_LINEAGE`；是否具有法律意義上的侵權、欺詐或不當引用，並非語義相似算法可以單獨裁定。
---
# 10. D8：經驗研究與物理理論的非同一性邊界
## 10.1 觀測相容不等於理論等價
若模型 A 與模型 B 在某批資料上產生近似相同的預測，最多可支持相應**觀測域與容差**下的相容性。在域外、不同干預或不同模型詮釋下，兩者可能給出相異結果。
可提出受限制的判定：
$$
\forall x\in D_{obs},\quad
d\bigl(O_A(x),O_B(x)\bigr)\le\delta,
$$
其中 $d$ 是事先選擇的距離或誤差尺度， $\delta$ 是對應任務合理的門檻。對真實有限資料而言，通常不能直接取得左式的全稱證據；必須把它替換成可觀測樣本估計及對樣本外推所需的假設。
因此 **`EMPIRICALLY_COMPATIBLE_ON_DATASET`** 與 **`THEORETICALLY_EQUIVALENT`** 必須分開標記。
## 10.2 同一數值不等於同一實驗證據
兩項實驗即使報告相同的均值或估計值，也可能使用不同儀器、母體、取樣、校準或資料清理。研究證據之間至少應比較：
- 測量對象及操作定義；
- 採樣框架、資料集版本與缺失機制；
- 儀器、校準、單位與觀測誤差；
- 統計估計量、區間估計與不確定度；
- 干預、對照及可能的混雜；
- 複現、重分析及資料重用關係。
相同實驗數值不是互為複製或獨立複現的證據；尤其資料集共享時，兩份報告可能不是獨立的經驗支持。
## 10.3 相同現象、不同因果主張
兩份研究都報告變數 $X$ 與 $Y$ 有相關性，但只有一篇提出 $X$ 導致 $Y$。兩者的觀測主張可能部分相符，因果主張卻不同。AI 不應從圖表相關係數直接把前一項提升為後一項的先例。
可用以下型別分開：`MEASUREMENT_COMPATIBLE`、`STATISTICAL_ESTIMAND_MATCH`、`CAUSAL_CLAIM_MATCH`。後兩項若缺乏共同識別假設與研究設計，必須保持未決。
## 10.4 不以 Lean 作為所有領域的唯一驗證器
形式邏輯、統計重分析、物理數值模擬、實驗重播、反例、資料完整性檢查及專家領域的測量協議，對不同主張有不同的驗證功能。ARKE-06 將制定多元驗證義務；本篇只確保**比較關係所依賴的證據種類被正確標記**。
---
# 11. D9：比較見證、證據閘道與結論狀態
## 11.1 四種不可替代的見證來源
本文要求每個非平凡的比較結論，標明支持它的見證種類：
| 見證 | 示例 | 支持的最大範圍 |
|---|---|---|
| `FORMAL_DERIVATION` | 在可信形式背景下的雙向蘊涵證明 | 指定形式命題與背景 |
| `FINITE_EXHAUSTIVE` | 對確知完整的有限輸入空間逐一驗算 | 指定有限宇宙及解析器 |
| `COUNTERMODEL_OR_TRACE` | 有效反模型、反例輸入或可觀測 trace | 對受限同一主張的否證 |
| `EMPIRICAL_EVIDENCE` | 凍結資料、測試協議、可信統計推論與可重播工件 | 指定樣本、假設與測量域 |
此外，`SEMANTIC_ALIGNMENT`（翻譯檢查）與 `SOURCE_ANCHOR`（可回訪原文）是多數比較的必要配套，但不能獨自取代上述數學／實證見證。
## 11.2 不確定性不能用單一信心分數抹除
令比較義務集合為：
$$
\mathcal O_J=\{o_1,\ldots,o_k\}.
$$
每項義務回傳：
$$
\sigma(o_i)\in
\{\mathrm{PASS},\mathrm{FAIL},\mathrm{UNKNOWN},
\mathrm{BLOCKED},\mathrm{NOT\_RUN}\}.
$$
義務未通過時仍可有局部成果，但不能將整個比較裁決標記為已完成。`BLOCKED` 表示受權利、工具或來源狀態限制，與數學上已證明不成立的 `FAIL` 不同；`NOT_RUN` 表示尚未執行，不得假稱測試結果。
## 11.3 比較結論的審核層級
| 層級 | 意義 | 可公開宣稱 |
|---|---|---|
| `CANDIDATE` | 模型或檢索器提出疑似關係 | 「可能相關／疑似等價」 |
| `SUPPORTED_WITH_SCOPE` | 有受限、可回訪的支持證據 | 「在已查核範圍內有此關係」 |
| `CHECKED_RELATION` | 指定判定器或受約束程序已檢查核心見證 | 「此比較義務在該契約下通過」 |
| `REFUTED_UNDER` | 有有效反例或反模型 | 「該全稱等價主張在此條件下不成立」 |
| `INCONCLUSIVE` | 高風險缺口或證據相互衝突 | 「目前不能確認」 |
| `SUPERSEDED` | 新來源或版本使原結論需重評 | 「前版為歷史紀錄，非當前裁決」 |
`CHECKED_RELATION` 是有**明確限制**的研究程序判定，不是「所有數學家皆接受」「所有知識已覆蓋」或「全球學術首次性已確認」。
## 11.4 證據來源與推導來源分離
對每一項比較，保留兩條鏈：
- **來源存在鏈：** 兩篇研究的原稿、版本、時間、片段與合法取得條件；
- **比較有效性鏈：** 使用何種轉譯、驗證程序、證明或反例取得何種關係。
這沿用 ARKE-04 的雙重證據分離。任何模型輸出的「因為我看到相似句子，所以兩者等價」，若缺乏可回訪原文和合理的語義分析，不可同時充當兩條鏈的完成證據。
## 11.5 雙向比較應保留方向
`a_entails_b` 與 `b_entails_a` 必須保留為有向關係；`a_uses_method_from_b` 更不能因方法相似就倒轉。研究歷史中的引用、先後時間和方法承接也有方向性。
對兩個方向都通過的邏輯蘊涵，若滿足共同比較契約及翻譯義務，可以額外建立等價候選及其見證；不能刪除原來的兩項方向性證據。
---
# 12. P1–P10：跨表示研究同一性的條件命題
下列命題主要是對一般錯誤推論的反例或對既定契約的結構結果，不宣稱它們是超越既有邏輯學、程式語義學的新大定理。
## 12.1 P1：字串相同不保證跨語境命題相同
**命題 P1。** 若比較語境或語義解釋沒有固定，兩個相同自然語言字串不必然代表相同研究命題。
**論證。** 例如兩份文件均寫「效率提高 10%」，其中一份指時間降低、另一份指每秒輸出增加；兩份文件的操作定義不同。即使字串相同，測量對象與真值條件可不同。故無比較語境時，文字相同不足以推出命題同一。證畢。
**界線。** 若字串是同一正式語言中的完整閉合公式，且語義環境、定義與公理完全固定，則可取得更強的關係；P1 不否認該情況。
## 12.2 P2：同一命題可以有不同證明方法
**命題 P2。** 命題等價不蘊涵證明路徑或方法相同。
**論證。** 同一有限恆等式可由展開代數式求得，也可由組合計數解釋取得；兩者可共享結論，卻具不同中間步驟與論證資源。故由主張同一不能推出方法同一。證畢。
## 12.3 P3：單向蘊涵不能推出雙向等價
**命題 P3。** 給定共同且相容的語義背景， $a\Rightarrow b$ 單獨不能推出 $a\leftrightarrow b$。
**論證。** 在實數上令 $a$ 為 $x>2$ 、 $b$ 為 $x>1$。則 $a\Rightarrow b$，但 $x=3/2$ 滿足 $b$ 而不滿足 $a$。證畢。
**工程含義。** 檢索器若找到較弱的歷史結論，不能直接宣稱新研究「完全被前人證明」；同樣也不能僅憑強弱推斷誰先發現某項方法。
## 12.4 P4：有限測試相同不能推出所有輸入等價
**命題 P4。** 若輸入集合 $X$ 存在不在測試集 $T$ 內的點，則 $f|_T=g|_T$ 一般不能推出 $f=g$ 於全部 $X$。
**論證。** 任取 $x_0\in X\setminus T$。令 $f(x)=0$ 對所有輸入成立；令 $g(x)=0$ 對 $x\neq x_0$ 成立，而 $g(x_0)=1$。二者在 $T$ 上完全相同，卻於 $x_0$ 不同。證畢。
**界線。** 如果 $T=X$ 且確實完整、窮舉程序正確，這個反例不適用。
## 12.5 P5：形式關係通過不能推出歷史首次性
**命題 P5。** 即使獲得有效的 $\varphi_a\leftrightarrow\varphi_b$ 證明，也不能僅據此裁定哪一方最早提出、最早證成或直接承接另一方。
**論證。** 證明項處理的是兩個形式命題的關係；歷史優先權須靠出版版本、時間與來源存在鏈決定。可以構造兩個發表先後相反、但命題關係完全一致的歷史情境。等價推導無法區分這兩個歷史情境。證畢。
## 12.6 P6：方法相似不能推出結果等價
**命題 P6。** 兩項研究採用相同的一般方法類別，不充分保證其輸出或主張相同。
**論證。** 相同的最小平方法可以在不同目標變數、樣本及模型條件下估計不同的量；相同的歸納法也可以證明完全不同的數學定理。方法分類相同不蘊涵結論的真值條件相同。證畢。
## 12.7 P7：不一致的背景可產生無意義的形式「等價」
**命題 P7。** 若採用帶有爆炸原理的邏輯且背景 $\Gamma$ 不一致，僅由 $\Gamma\vdash\varphi\leftrightarrow\psi$ 無法作出有內容的跨研究同一性結論。
**論證。** 在該邏輯下，不一致背景可證任意命題，故亦可證兩個任意命題間的雙向蘊涵。若沒有一致性或非空模型的保障，這種推導無法區分真正有意義的關係。證畢。
**界線。** 這是針對採用爆炸原理的系統；不同的非古典邏輯需另行規範。
## 12.8 P8：修訂來源可改變當前比較狀態，但不刪除舊證據
**命題 P8。** 若新版本修改了被比較主張的內容或前提，既有 `CHECKED_RELATION` 不保證仍對新版本成立。
**論證。** 設版本 $v_1$ 述及 $\varphi$，版本 $v_2$ 改為 $\varphi'$。若先前見證只建立 $\varphi\leftrightarrow\psi$，而未建立 $\varphi'\leftrightarrow\psi$，則原見證不能自動證成新關係。保留舊版本及證據，並將新比較列為待查。證畢。
## 12.9 P9：等價的傳遞性需要相容上下文及翻譯
**命題 P9。** 若同一一致背景與相同語義域下有 $a\leftrightarrow b$ 、 $b\leftrightarrow c$，且用於 $b$ 的解釋相同，則有 $a\leftrightarrow c$。
**論證。** 將兩個雙向蘊涵的各個方向合成，即得 $a\Rightarrow c$ 與 $c\Rightarrow a$。證畢。
**界線。** 若第一個關係使用 $\Lambda_1$，第二個使用不相容的 $\Lambda_2$，或中介主張 $b$ 的定義被偷換，則不得利用本命題直接宣稱傳遞。候選相似、觀測相容、引用承接等非等價關係也不自動符合傳遞律。
## 12.10 P10：一個合法反例足以否定指定域的全稱等價
**命題 P10。** 若宣稱對所有 $x\in D$ 均有 $f(x)=g(x)$，且找到 $x_0\in D$ 滿足 $f(x_0)\neq g(x_0)$，則此全稱等價為假。
**論證。** 由全稱量詞的反例規則直接得出。證畢。
**界線。** 反例的輸入合法性、程式執行重播、浮點容差與外部資料版本仍須核查；錯誤解析的測例不能當作有效反證。且反例只否定該指定域上的全稱等價，不必否定其他子域的局部相容。
---
# 13. 真實公開案例：ETH 研究先例應如何作跨表示比對
## 13.1 案例性質與資料邊界
以下使用可回訪的公開研究紀錄示範 **CRRIC 應檢查哪些欄位**，不是對 ETH 反證本身作數學正確性判定，也不宣稱已完成兩篇論文的完整技術等價審查。
已知可定位的公開紀錄包括：
- Giorgio Camerani 在 2021 年 2 月公開 *The #ETH is False, #k-SAT is in Sub-Exponential Time*，其摘要主張使用**隨機化**演算法在 $2^{o(n)}$ 時間內精確計算固定寬度 # $k$ -SAT 的滿足指派數量，並據此聲稱推翻 #ETH／ETH 等假說 [R10]。
- OpenAI 在 2026 年 10 月公開 *The Exponential Time Hypothesis is False*，其論文與公開形式化範圍文檔主張一項**確定性**固定寬度 CNF 精確計數演算法，並有相應 Lean 形式化材料 [R11][R12]。
截至本文查核日，上述資料足以確認**歷史上存在相近的公開研究主張**；不足以僅憑摘要、題名和形式化範圍就確認兩篇演算法同構、兩個證明相同或 2021 年的主張已被獨立證實。
## 13.2 正確的比較入口
兩項研究首先在目標層存在交集：固定寬度 CNF、精確滿足指派計數、次指數時間主張。這支持 `RELATED_TARGET`，但尚不足以支持 `SAME_ALGORITHM`。
比較表如下：
| 項目 | 2021 Camerani（公開摘要所述） | 2026 OpenAI（公開資料所述） | CRRIC 裁決 |
|---|---|---|---|
| 研究目標 | # $k$ -SAT 精確計數 | 固定寬度 $k$ -CNF 精確計數 | `TARGET_OVERLAP_CANDIDATE` |
| 演算法隨機性 | 隨機化主張 | 確定性主張 | `DISTINCT_PROPERTY_REPORTED` |
| 時間形式 | $2^{o(n)}$ 主張 | 次指數上界，含更細參數條件 | 須核對輸入表示、量詞與上界 |
| 形式化狀態 | 此處未確認可用的獨立完整證明 | 公開 Lean 範圍文件 | 不可推論兩者同等有效 |
| 方法結構 | 需閱讀原文與細部推導 | 需閱讀原文與細部推導 | `METHOD_COMPARISON_NOT_RUN` |
| 學術首次性 | 具有較早公開主張的時間紀錄 | 具有較後公開主張的時間紀錄 | 只能裁定存在早期主張，不直接裁定首次證成 |
這裡的 `DISTINCT_PROPERTY_REPORTED` 只說文件對演算法性質採取不同描述；不代表數學上已經證明某種隨機算法不可能去隨機化，也不能推出另一演算法絕對不同。
## 13.3 同一作品內：論文上界與形式化上界也應比較
OpenAI 公開的 Lean 範圍文件將已形式化的時間界與論文中的較尖銳上界分開列出 [R12]。因此，即使來自同一研究作品，也不能把「某個上界經形式化檢查」偷換成「該論文所聲稱的一切最強上界都已形式化」。
例如，範圍文件描述的一項形式化結果具有大致形態：
$$
(L+1)^{O_k(1)}
2^{O_k\left(n(\log\log n)^2/\sqrt{\log n}\right)},
$$
而論文還提出在其他記帳方式或條件下更強的上界。兩者可以同時屬於次指數時間，卻不能因此宣稱**字面界限相同、推導義務相同或完全可互換**。分析必須保留 $L$ 、 $n$ 、 $m$ 、固定 $k$ 、輸入編碼與隱藏常數的角色。
本篇不自行驗證上述複雜度界限的證明，僅將其作為「**研究表述的形式化範圍需要和自然語言結論逐項對齊**」的公開示例。
## 13.4 較早主張與新證明可能同時有價值
即使某個舊研究主張了相同的宏觀結論，也存在至少四個不同情形：
1. 舊研究已有效證明同一主張，新研究提供替代證明或新算法；
2. 舊研究提出相同結論，但證明尚有缺口，新研究提供新的有效證成；
3. 舊研究只涵蓋較窄域，新研究拓展域或強化成本界限；
4. 新舊研究其實具有不同任務或假設，表面相同但不能視為同一結果。
CRRIC 應保留多個可能分支，透過證據逐步排除，不由知名度、模型名稱或出版先後直接決定。
## 13.5 本案例不容許的推論
本篇不宣稱：
- 2021 年論文已經正確推翻 ETH；
- 2026 年論文必然抄襲或重新包裝 2021 年算法；
- Lean 形式化已驗證對任意自然語言敘述的全部含義；
- 由於研究主題相似，所以 2026 年的演算法沒有新增數學貢獻；
- 單憑公開時間即可裁決全部學術歸屬。
**本案例的唯一確定用途**，是展示 AI 若能自行完成基本先例搜尋，就應在宣稱學術突破前，主動將這類較早主張納入可追溯比較，而不是讓「沒有想到查」成為研究完備的默認狀態。
---
# 14. 三個跨領域合成案例（非真實驗收）
## 14.1 案例 A：同一數學式，成立域卻不同
研究 A 宣稱對所有實數 $x$：
$$
x^2\ge0.
$$
研究 B 僅宣稱對整數 $x$：
$$
x^2\ge0.
$$
在標準實數與整數的相容詮釋下，A 的宣稱涵蓋 B 的全部輸入，但 B 的聲明本身沒有涵蓋所有實數。此例說明：**同一公式字串不代表同一量詞域，強弱關係必須指明翻譯與域映射。**
若 B 的證明完全不同，它仍可能提供新方法；若 B 的全文包含額外結論，也不能因這個片段受 A 涵蓋就把整篇 B 判定沒有新意。
## 14.2 案例 B：排序輸出相同，演算法規格不同
研究 A 與 B 都以升序排序。當輸入鍵值皆不相同時，兩者輸出可能完全一致；但若排序的輸入包含重複鍵，且規格要求保留原先次序，穩定排序與非穩定排序可能產生不同輸出序列。
此例至少需要記錄：
- 元素是否具有可觀察的附加資料；
- 相同鍵是否允許；
- 穩定性是否屬於輸出契約；
- 比較的是整個序列還是僅按鍵排序後的投影；
- 時間、空間與 in-place 條件是否納入。
若只測沒有重複鍵的輸入，兩者可能被錯判為外延完全等價；此類反例適合作為 ARKE-05 的保留測試題。
## 14.3 案例 C：物理模型在觀測資料中等效，因果機制不同
設合成研究 A、B 在一段有限觀測時間內對某訊號有近似相同的預測。但當研究者施加不同控制參數或跨出先前尺度，兩者預測分離。
在未取得干預資料之前，可以記錄 `EMPIRICAL_COMPATIBILITY_ON_DATASET`；在新實驗提供合格區分見證後，可以在更廣比較域建立 `NOT_EQUIVALENT_WITH_WITNESS`。先前局部吻合的歷史紀錄仍保留，不應因新結果而消失。
這個例子對應 ARKE-07 的雙向知識修正：新證據可以縮小舊理論有效域，並要求下游引用重新評估，但**不必然消滅舊理論在原有效域的實用價值**。
---
# 15. M1：AI 自主研究同一性查核流程（方法論規格）
## 15.1 從 ARKE-04 候選清單進入
入口應是「已凍結研究候選及可回訪先例」，而不是任由模型讀完後直接覆寫研究原稿。建議流程如下：
**M0 — Freeze。** 鎖定新研究版本、研究主張與輸出、生成歷程與檔案摘要；承接 ARKE-04 的盲研究隔離。
**M1 — Retrieve。** 由合法資料來源取得可查核的先例片段及其 RTA；不足全文的只建立受限候選。
**M2 — Type。** 分離作品身分、結果命題、演算法、方法、證明、實驗與歷史關係；一篇論文可建立多個主張。
**M3 — Align。** 搜尋詞彙、符號、定義、任務與語義映射；保留對應版本、翻譯信心及證據缺口。
**M4 — Compare。** 在 $\Lambda$ 中比較量詞、假設、成立域、方法、輸入編碼、成本與可觀測量。
**M5 — Witness。** 嘗試取得指定關係所需的雙向推導、有限窮舉、反模型、程式反例、重播或統計支持；未完成則保留未知。
**M6 — Audit。** 查來源、驗證器狀態、依賴公理、版本、合法使用、是否有不一致的中介轉譯；任何不足都限制可主張範圍。
**M7 — Record。** 將正向、反向、局部與未知關係寫入帶有證據的歷史紀錄；不可改寫原始研究或刪去失敗先例。
**M8 — Return。** 輸出限定作用域的差異報告與 ARKE-04 新穎性向量更新，交由 ARKE-06 繼續對結果有效性進行獨立核驗。
## 15.2 最小流程表示
```text
compare_research(candidate_a, prior_b, contract):
assert candidate_a.frozen and prior_b.source_identified
anchors = resolve_legally_permitted_claim_anchors(a, b)
if anchors.incomplete:
return CANDIDATE_WITH_GAPS
typed = split_by_claim_method_proof_evidence_history(a, b)
bridge = propose_translation_and_common_contract(typed, contract)
if bridge.invalid or bridge.unresolved:
return INCONCLUSIVE_WITH_TRANSLATION_OBLIGATIONS
relations = []
for dimension in typed.dimensions:
obligations = derive_relation_specific_obligations(dimension, bridge)
findings = run_allowed_checkers_or_record_not_run(obligations)
relations.append(classify_scoped_relation(findings, anchors, bridge))
audit = verify_provenance_rights_models_axioms_and_version(relations)
return emit_relation_bundle(relations, audit, unresolved=all_open_obligations)
```
此偽代碼是**研究方法契約**，不是已實作程式。`run_allowed_checkers` 必須根據獨立工程系統的授權、資源與執行隔離政策執行，不因研究文件存在便獲得任意檔案讀取或計算權。
## 15.3 允許 AI 自主完成基本工作，但不能假造確定性
AI 可自行選擇工具、產生查詢、對齊文本、執行允許的程式、生成反例候選、調用現有形式驗證器、記錄差異並提出後續查核；這符合本系列的 AI-first 立場。
但如果比較對象是一般不可判定的程式語義問題、尚無可用形式化、權利不允許取得內容，或實驗資料不足，輸出 `INCONCLUSIVE` 是合法而必要的研究結果。**自主性不等於一定有答案；它包括自行知道何時尚不能下定論。**
## 15.4 限制錯誤合併的傳播範圍
當兩篇研究被錯併，後續可能同時錯誤處理引用、新穎性、版本及理論依賴。故 CRRIC 的輸出在沒有合格見證前，應以候選邊連結，不允許自動合併研究主張的 canonical identity。
若已確認某個特定主張等價，也不自動把整份作品或全部證據合併。系統只可在指定作用域建立可追溯同一關係，保留兩側版本與原始出處。
---
# 16. D10：可機器讀取的跨表示關係語義物件
本節僅提供**概念 JSON 範例**，供獨立 ARKE GitHub 工程在未來制定正式 Schema；不是已通過相容性測試的 API，也不暗示此物件能直接授權執行任何模型、程式或外部搜尋。
```json
{
"schema": "arke/crric-relation-concept-v0.1",
"comparison_id": "CMP-SYNTH-001",
"comparison_status": "EXAMPLE_NOT_EXECUTED",
"subject_a": {
"claim_id": "A-C01",
"work_id": "A-W01",
"version_id": "v1",
"rta_ref": "RTA-A-001",
"source_sha256": null
},
"subject_b": {
"claim_id": "B-C01",
"work_id": "B-W01",
"version_id": "v2",
"rta_ref": "RTA-B-001",
"source_sha256": null
},
"contract": {
"task_identity": "synthetic-comparison-only",
"shared_domain": "finite natural numbers n >= 1",
"assumptions": ["standard-arithmetic"],
"logic": "unresolved-formalization",
"input_encoding": "not-applicable",
"cost_model": "not-applicable",
"tolerance": null,
"rights_policy": "metadata_and_permitted_fragments_only"
},
"translation": {
"status": "PROPOSED_NOT_VERIFIED",
"mapping_ref": null,
"preservation_witness": null
},
"relation": {
"dimension": "claim",
"type": "PENDING_EQUIVALENCE",
"direction": "bidirectional_candidate",
"scope": "contract.shared_domain",
"evidence_level": "CANDIDATE",
"proof_a_to_b": "NOT_RUN",
"proof_b_to_a": "NOT_RUN",
"counterexample": null
},
"history": {
"prior_claim_found": "UNKNOWN",
"prior_validated_result_found": "UNKNOWN",
"method_lineage": "UNRESOLVED"
},
"verification": {
"source_anchors_checked": false,
"background_consistency_checked": false,
"checker_version": null,
"replay_artifact": null,
"unresolved": [
"formal-mapping",
"two-way-entailment",
"source-content-access"
]
},
"authority": {
"training_authorized": false,
"method_execution_authorized": false,
"scientific_validity_certified": false,
"global_novelty_certified": false,
"rsi_verified": false
}
}
```
## 16.1 最小必填義務與欄位依賴
- 若 `relation.type = LOGICAL_EQUIVALENCE`，原則上須有相同契約下的兩向證明或其他同等強度可重播證據。
- 若 `relation.type = NOT_EQUIVALENT_WITH_WITNESS`，須有符合共同域的區分見證與檢查記錄。
- 若 `translation.status = PROPOSED_NOT_VERIFIED`，不得把經翻譯得到的等價結果提升為無保留的跨語言／跨形式系統裁決。
- 若 `source_sha256 = null`，只能表示未有可核對來源指紋，不能當作已驗證完整性。
- 若來源版本改變，應新增新比較事件並連結舊事件，不應直接改寫舊 `comparison_id` 的歷史語義。
- 若 `authority` 中出現權限聲明，其權威來自外部正式授權系統，不得由論文研究物件自行賦權；本範例全部為 `false`。
## 16.2 不預設唯一資料庫或唯一圖原語
比較結果可保存為關聯式資料表、文件、事件流、有型別圖、超邊、內容定址工件或其他合適結構。ARKE-03 的 RTA 和研究依賴關係可以是跨系統互操作層，**不是要求所有數學表示、圖片或模型推理一律轉為一般知識圖譜**。
對已驗證等價的多種表示，系統可以建立等價關係；若語義上下文不同，仍保留不同節點與關係作用域。對不同原稿的作者、作品與版本識別，不因研究命題相同就抹除各自的來源身分。
## 16.3 最低歷程與完整性保證
應保留事件 ID、事件序號、不可變比較輸入摘要、來源錨點版本、查核程序版次、結果狀態、所用模型／演算法版本、必要成本及檢查時間；跨事件改動須明確以新事件或新版本表示。
雜湊鏈與不可變儲存可以幫助檢出部分事後改動，但不是數位簽章或無條件的防惡意保證。研究身分、歷史優先權及證據真實性應按不同威脅模型另行檢查；這點與 EveTrain RAI Registry 的既有界線一致。
---
# 17. 比較品質的可觀測指標
## 17.1 錯誤合併率（False Merge Rate）
令 $G_{neq}$ 為保留測試集中**已具合格區分見證**的研究配對， $P_{merge}$ 為系統錯誤宣稱全域同一的配對。若 $|G_{neq}|>0$：
$$
\mathrm{FMR}=
\frac{|G_{neq}\cap P_{merge}|}{|G_{neq}|}.
$$
此指標衡量在已知不等價案例上的錯誤同一宣稱；不得把所有缺乏既知關係的配對都當成 `not equivalent` 的金標。
## 17.2 有證據等價召回（Witnessed Equivalence Recall）
令 $G_{eq}$ 為在指定作用域內有合格等價見證的保留配對， $P_{eq}$ 為系統依規範給出等價裁決的配對：
$$
\mathrm{WER}=
\frac{|G_{eq}\cap P_{eq}|}{|G_{eq}|},
\qquad |G_{eq}|>0.
$$
這個分母是**經標註／核驗的 benchmark 集合**，不能視為全世界所有實質等價先例。對於尚無完整可決證據的案例，應另列未決，不得用不完整金標硬性計分。
## 17.3 作用域與假設錯誤率
對預先標註的域敏感題，計算：
$$
\mathrm{ScopeError}
=
\frac{\#\text{違反已知域或量詞條件的裁決}}
{\#\text{已評估的域敏感裁決}}.
$$
只在分母非零、標註定義一致時輸出。若系統在 domain-mismatch 案例中正確保留未知或局部關係，不應將其誤算為「一定要給全域結論才算成功」。
## 17.4 過度保守與逃避判斷率
若系統對全部案例都回答 `UNKNOWN`，FMR 可能是零，但系統並未完成實際比較。故必須同時量測：
- 已具有合格見證的案例中被無必要地保留為未知的比例；
- 正確提供有型別局部關係而非全域裁決的比例；
- 在固定成本預算下完成最低比較義務的比率；
- 對 `UNKNOWN`、`BLOCKED`、`NOT_RUN` 的分類正確性。
本研究不設任意固定的「未知率必須低於某數」作為普遍門檻；應按任務風險和證據可取得性評價。
## 17.5 證據可重播率
對輸出 `CHECKED_RELATION` 的案例，測量外部獨立執行者在合法權限下，能否使用保存的版本、輸入、驗證器與見證重新取得相同**受約束裁決**。重播率低時，需區分工具版本漂移、來源斷鏈、法定取用限制及證據內容本身的錯誤。
## 17.6 真實資源成本與代價轉移
比較總成本至少拆成：
$$
\mathbf C=
(C_{search},C_{read},C_{align},C_{verify},
C_{store},C_{update}).
$$
實際記錄以時間、token、能源、儲存、授權費及其他單位分開保存，不假定能在無共同權重時直接求出客觀唯一總分。若索引建立昂貴但每次比對便宜，應報告單次、批次與長期攤銷視角，不能只挑對自己有利的成本口徑。
## 17.7 研究增量保存率
在已知兩份研究共享某個結論、但各自方法或證據不同的案例中，量測系統是否仍保留：
- 先前主張的來源與其成立狀態；
- 新研究的具體方法或證明增量；
- 各版本的獨立證據及時間；
- 關係的未知與未完成部分。
若某系統能較快合併文件，卻錯誤刪除了新證明或舊失敗路徑，其結果不得被視為知識演化品質更高。
---
# 18. H1–H8：可否證的實證研究方案（全部 NOT_RUN）
## 18.1 共同實驗原則
以下為**研究設計**，不是執行報告。正式實驗應先決定：資料來源及權利、預註冊樣本與分析方法、盲測切分、比較契約生成策略、各類真值／見證的最低接受標準、成本預算、錯誤風險與停止條件。
至少設定三種可比較方案：
- **B0：** 文字／向量檢索加語言模型直接判斷相同與否；
- **B1：** 檢索後使用標準化公式、程式或單一驗證器，但沒有完整多維度關係契約；
- **T：** 本篇 CRRIC 型別、契約、翻譯見證、證據與未決機制。
若 T 使用更多 token、時間、資料庫或驗證工具，必須在分析中保留資源差異，另設等預算比較。不可讓 T 看到 B0、B1 沒有資格取得的測試答案，卻宣稱改善全由新方法造成。
正式金標不可只靠研究模型自己評自己。可以使用獨立形式檢查、既有具見證的 benchmark、保留反模型及合法的跨系統重播；難例可納入多方獨立判定，但**人類專家不是 AI 自主查核工作流的預設必經環節**。
## 18.2 H1：跨語言與跨符號對齊降低等價先例漏檢
**假說。** 相較 B0，在同一資料、時間與預算條件下，使用受約束翻譯及量詞／成立域檢查的 T，能提高已具等價見證之跨語言定理配對的召回率，且不增加錯誤合併率。
**資料。** 已存在可形式核驗的同一命題不同語言／表示對、同名異義對、翻譯否定漂移對；按定理家族切分，避免同一模板近似拷貝同時出現在訓練和測試。
**主要指標。** WER、FMR、錯譯率、來源定位成功率、每例驗證成本。
**失敗條件。** WER 改善不明顯，或改善伴隨高於預註冊容忍幅度的 FMR；也可能因翻譯成本過高而不具成本效益。
## 18.3 H2：顯式量詞與成立域減少錯誤的「嚴格強弱」判定
**假說。** 相較 B0/B1，T 對不同端點、有限／無窮域、隱含常數或量詞順序的研究案例，能降低將 `ONE_WAY_ENTAILMENT` 誤標為 `LOGICAL_EQUIVALENCE` 的比例。
**資料。** 經形式構造的成對定理、空域陷阱、不一致背景陷阱及具有有效區分反模型的案例。
**主要指標。** 量詞誤判率、嚴格強弱方向錯誤、`UNKNOWN` 適當保留率。
**失敗條件。** 系統仍以文字相似度替代域查核，或因過度保守而錯失大量本可有效確認的關係。
## 18.4 H3：將方法、主張與證明分離能保留新增研究貢獻
**假說。** 相較只比對結論的 B1，T 更能保留「舊定理＋新證明」「舊方法＋新成立域」「早期錯誤證明＋後期有效證明」的不同學術貢獻類型。
**資料。** 具有多證明、修訂版或獨立方法的數學／演算法文獻，使用公開可合法核對的來源與先例時間。
**主要指標。** 方法增量保存率、過度合併率、歷史倒灌率、引用關係型別準確率。
**失敗條件。** T 仍把「同一結論」當成整篇論文無新意，或改善完全依賴額外人工標記而無法由 AI 基本流程重播。
## 18.5 H4：反例導向查核降低程式功能等價誤判
**假說。** 在具有非穩定排序、邊界溢位、空輸入、未終止分支等故障注入的有限程序庫中，T 結合反例搜尋與操作契約，比單純相同測試集比較更能發現不等價。
**資料。** 合法、封閉的程式與輸入生成規格；對可完整窮舉的片段，建立精確金標；對一般程式只要求找到合法反例而不宣稱全域可決。
**主要指標。** FMR、有效反例發現率、錯誤報告率、CPU 與記憶體成本。
**失敗條件。** T 大量產生假反例，或對經驗性非等價結論的信任聲明超出證據範圍。
## 18.6 H5：形式化範圍核對減少「證明檢查通過＝全文全主張通過」
**假說。** 將來源命題、形式化命題、已使用公理及結果上界逐項對齊的 T，比只讀取工具 `PASS` 狀態的 B1，更少作出超出 proof artifact 範圍的研究有效性聲稱。
**資料。** 包含 `sorry` 依賴、額外假設、形式化較弱版本與原文端點缺口的合成與公開案例。
**主要指標。** 過度驗證宣稱率、未查公理率、形式化範圍錯配率、正確保留可用結論率。
**失敗條件。** T 仍以工具成功執行代替來源語義查核，或把局部缺口誤判為整篇研究必然無效。
## 18.7 H6：跨領域契約降低觀測相容與因果同一混淆
**假說。** 在物理與其他經驗研究案例中，明確檢查測量操作定義、干預條件與證據版本，能降低將局部觀測相容提升為理論／因果等價的錯誤。
**資料。** 合成可控模擬、公開可重播的資料研究、相同結果不同生成機制的保留集。
**主要指標。** 因果同一誤判、測量域錯配率、反例辨識率、證據可重播率。
**失敗條件。** 多元契約無法操作化，或資料量不足時系統仍輸出確定因果裁決。
## 18.8 H7：有型別比較的錯誤成本是否小於工程新增成本
**假說。** 在長期持續更新的學術索引上，T 的初始對齊成本可能增加，但能透過可重用見證、版本增量及避免錯誤合併，降低後續重查或學術修復成本。
**資料。** 按時間順序重播的論文版本更新、撤回、修訂及新增先例；禁止使用未來版本倒灌。
**主要指標。** 單次／攤銷成本、重複檢查率、錯誤修復成本、知識關係有效時間、版本遷移的失敗率。
**失敗條件。** 新增的保存與核查成本遠高於實際降低的錯誤處理成本，或收益僅在合成有利資料下出現。
## 18.9 H8：將 CRRIC 接入 AI 自主研究流程可降低基本學術缺漏
**假說。** 在凍結研究候選之後，使用 ARKE-04 檢索加 ARKE-05 比較的 AI 自主查核流程，比只靠模型自行撰寫參考文獻更能辨認先前相同主張與新研究的實際增量。
**資料。** 跨數學、理論計算機科學、工程與物理的保留研究候選；包含知名與低曝光來源、有真實可核查先例及無法確認的未知案例。
**主要指標。** 錯誤首次性宣稱率、關係準確率、證據可回訪率、過度保守率、可用結論輸出率與完整成本。
**失敗條件。** AI 依然經常把先前主張誤判為已正確證明、將無法取得全文的論文視為不存在，或需依賴未預先配置的人類補救才能完成原本已自動化的基本步驟。
## 18.10 所有假說的共同執行狀態
| 項目 | 本稿狀態 |
|---|---|
| H1–H8 實驗執行 | `NOT_RUN` |
| 跨語言／跨證明器真實比較 | `NOT_RUN` |
| 通用演算法外延等價引擎 | `NOT_IMPLEMENTED` |
| AI 自動生成形式見證的效能 | `NOT_MEASURED` |
| 系統級成本與準確度比較 | `NOT_MEASURED` |
| ARKE 專用獨立 GitHub 工程整合 | `NOT_VERIFIED` |
| EveTrain RAI／RSI 能力提升 | `NOT_DEMONSTRATED` |
上述 `NOT_RUN` 不表示「結果為零」「假說已遭反駁」，也不允許以已有理論論證代替將來實驗。
---
# 19. 主要失敗模式與最低防護
## 19.1 同名異義與異名同義
**錯誤：** 相同術語當作同一模型，或不同名稱就排除真正相同的命題。
**防護：** 比較詞彙定義、量詞域和操作語義；保留原始稱呼、別名、來源片段及有條件的翻譯見證。
## 19.2 量詞與端點漂移
**錯誤：** 把「部分」「幾乎處處」「存在」改成「所有」，或將開區間偷換成閉區間。
**防護：** 型別化量詞、條件與域；對不一致背景、空域及端點設專門反例。
## 19.3 只靠文字或向量相似度合併研究
**錯誤：** 高相似度直接寫入 canonical same-claim ID。
**防護：** 相似度只產生候選；等價、蘊涵及不等價關係必須要求對應的證據與範圍。
## 19.4 只依賴有限測試下的相同輸出
**錯誤：** 程式通過 100 個測例便被稱為對所有輸入等價。
**防護：** 區分 `TESTED_ON_FINITE_SET`、`EXHAUSTIVELY_CHECKED_FINITE_DOMAIN`、`FORMALLY_CHECKED` 與 `UNKNOWN_GENERAL_CASE`。
## 19.5 形式系統通過即宣稱全文研究正確
**錯誤：** 忽略形式化語句與自然語言命題的差異、未檢查公理、較弱上界或部分完成。
**防護：** 保存來源對應、依賴公理與可重播範圍。Lean 官方驗證文件已提供明確的信任邊界及公理追蹤方式 [R5][R6]。
## 19.6 以新穎性推導正確性，或反向推導
**錯誤：** 找不到先例便認為新成果真，或某個推導有效便宣稱全球首次。
**防護：** 沿用 ARKE-04 的先例存在鏈與研究有效性鏈；不將兩者合併成單一 `verified` 欄位。
## 19.7 版本錯併與修訂倒灌
**錯誤：** 新版加入的定理被歸回舊版本；被撤回的主張仍被當作現行支持。
**防護：** 作品、版本、載體、片段、主張分層定位；新增關係事件而不刪除歷史。
## 19.8 對無法取得全文的先例作強判決
**錯誤：** 只有題名或摘要，卻宣稱已證明兩套演算法完全一致或完全不同。
**防護：** 允許 `SOURCE_ACCESS_LIMITED`；提出可能的比較方向，但所有未取得的證明步驟保留為未知。
## 19.9 OCR、圖片與跨模態資訊遺失
**錯誤：** 數學公式上標、下標、否定符號、坐標、圖像局部區域經轉寫後改變命題。
**防護：** 保留原始載體與片段選擇器，針對關鍵數學符號做反向核對；無法解析時不升格比較裁決。W3C Web Annotation 提供既有的 selector／state 模型，適當情境可直接重用 [R14]。
## 19.10 指令注入與檢索來源偽裝權威
**錯誤：** 外部論文、網頁、README 或 PDF 中夾帶要求 Agent 授權執行、洩漏私有資料或修改研究證據的指令。
**防護：** 研究內容是**不可信資料輸入**，不是工作流控制指令；來源權限、工具執行與知識判斷須隔離。外部引用文本不得自行授予 GPU、網路、祕密或檔案修改權。
## 19.11 權利、倫理與訓練資料邊界
**錯誤：** 視可索引為可重製，或視可讀為可任意訓練及散布。
**防護：** 延續 ARKE-02 的權利分層：metadata、定位、片段讀取、保存、再散布、模型訓練分別檢查；對不允許保存的內容以合法地址及低洩漏關係資訊替代。
## 19.12 輸出「不知道」被誤當失敗
**錯誤：** 系統為追求表面完成率而捏造證明、反例或先例。
**防護：** `UNKNOWN`、`NOT_RUN`、`BLOCKED` 與 `FAIL` 分離；評估指標同時衡量錯誤斷言與不必要的逃避判斷。
## 19.13 歷史歸屬與作者責任被相似演算法替代
**錯誤：** 兩個演算法使用相同技術就自動推論後來研究者抄襲，或者早期稿件存在就否定後來有效證明。
**防護：** 時間、來源、實質方法承接、訓練／閱讀可見性與學術歸屬應各自記錄。語義同一性分析不能獨自裁決人類意圖、法律責任或知識貢獻的全部面向。
---
# 20. 與既有標準及研究的差異化定位
## 20.1 現有工作已解決了哪些部分
已存在的技術和研究至少包括：
- **形式證明與一致性查核：** Lean 等 proof assistants 及其 proof checking、已知公理追蹤 [R5][R6]；
- **受限邏輯求解：** SMT-LIB 及對應求解器生態 [R7]；
- **跨形式庫概念對齊：** Gauthier–Kaliszyk 對不同 proof assistant 的概念比對 [R1]；
- **程式翻譯驗證：** Necula 的編譯語義保持檢查方法 [R2]；
- **理論同一性研究：** Weatherall 對物理理論各種等價概念的區分 [R3][R4]；
- **研究來源可追溯：** W3C PROV-O 的 qualified provenance、Web Annotation 的定位與狀態 [R13][R14]；
- **跨格式自動推理基準：** TPTP 問題庫 [R9]。
因此 CRRIC 的主張不是「人類以前不知道怎麼比對公式」，而是：**AI 自主研究的發表前查核，需要把不同領域已存在的比較能力接成有型別、有作用域、可信度可分辨、歷史可追溯且不會自動抹除知識的程序。**
## 20.2 ARKE-05 的可檢驗新增部分
本篇新增的候選研究價值主要表現在工作流組合，而非獨創不可判定問題的解法：
1. 由 ARKE-04 的先例候選，轉為受 $\Lambda$ 約束的多維研究關係；
2. 將定理、方法、演算法、證明、實驗與時間來源分成獨立的身份與裁決層；
3. 對同一、強弱、局部重疊與反例建立不同見證義務；
4. 將可讀來源、可回訪原稿、合法使用、形式證明與發表主張分開；
5. 允許 AI 自主完成基本查核並且有尊重未知的停機契約；
6. 建立跨領域可測的錯誤合併、漏檢、過度保守及成本指標；
7. 把版本變更和新證據直接回饋到可追溯研究關係，而不是覆蓋研究歷史。
這些是否顯著優於現有系統，應由 H1–H8 的控制實驗判斷，而不是僅因寫出新框架就自行認證。
---
# 21. B：本篇不能推出的結論
**B1。** 不能宣稱存在一個會對所有數學定理、圖靈完備程式和物理模型在有限時間內正確判等的通用算法。
**B2。** 不能宣稱某兩篇文獻標題、字串、關鍵詞或向量相似度高，就必然是相同學術成果。
**B3。** 不能宣稱通過 Lean、SMT 或另一形式檢查器，就自動取得學術新穎性、歷史首次性、自然語言語義對應與實驗有效性。
**B4。** 不能由兩個程式在有限測試集的相同輸出推出一般外延等價，除非已有完整窮舉或其他適用見證。
**B5。** 不能由某個比較契約下的等價，推論更廣域、更強計算模型或不同測量單位下亦然。
**B6。** 不能由方法相似推定直接閱讀、抄襲、違規使用或作者意圖。
**B7。** 不能將未見先例等同於全球不存在先例；來源覆蓋與合法可達性沿用 ARKE-02／04 的限制。
**B8。** 不能把早期已提出某個結論，等同於已成功證明該結論。
**B9。** 不能把局部或條件式等價，升格為兩份完整作品在全部研究面向上的同一。
**B10。** 不能因為某版本失效而無差別宣稱所有下游研究必然錯誤；依賴關係須分型並按前提重查。
**B11。** 不能宣稱本文 H1–H8 已完成，更不能宣稱 ARKE 已顯著改善 AI 真實科研能力或驗證了 RAI／RSI。
**B12。** 不能把 ARKE 的研究比較物件當成執行權、訓練權、資料權利或正式學術裁決機構的替代來源。
---
# 22. 與後續研究、EveTrain 及獨立 ARKE 軟體的接口
## 22.1 ARKE-06：多元研究驗證
ARKE-05 將 `relation_bundle`、`shared_contract`、`translation_obligations`、`witnesses`、`unresolved` 交付給 ARKE-06。下一篇必須分別制定：定理有效性、演算法實作正確性、實驗證據品質、反例與重播、測量及因果支持的驗證責任；不得因「與舊論文等價」就跳過主張自身的正確性查核。
## 22.2 ARKE-07：雙向知識查核及歷史修正
當新研究推翻舊研究的一個具體前提、或來源版本撤回特定證明時，ARKE-05 的有型別依賴邊可指出需重新查核哪些關係。是否應修正、限縮、分叉或退役，由後續理論演化契約決定；來源版本歷史本身不應被刪除。
## 22.3 ARKE-08：學術歸屬及智慧體貢獻
ARKE-05 只能提供關係證據：先前有哪些主張、何時公開、方法在哪裡重疊、新證明或新實驗新增了什麼。這些是學術歸屬分析的資料基礎，但不是將所有智識貢獻縮減成演算法自動給分。
## 22.4 ARKE-09 至 ARKE-11：工作流、演化與發表前責任
後續可以將本篇見證義務納入 AI 自主查核執行流程、增量索引更新及最終發表閘道。其中最重要的是：**若仍有不能證成的全域新穎性、不可取得的舊證明或未決的跨表示等價，研究產物可以以較弱聲明公開，但不能偽裝成已完成全部義務。**
## 22.5 ARKE-12：跨領域實證與 RAI／RSI
未來可用 ARKE-05 比較 AI 新舊研究策略、演算法改動和實際證據，而不是只計算產出論文數量。是否真的改善研究能力，必須在保留集、可重播成本及能力測量下獨立證成。
## 22.6 EveTrain RAI Registry 的可選互通
本篇可將研究比較結果作為 EveTrain RAI 演算法候選的**外部證據與關係線索**。但 Registry 內的候選狀態、報告摘要或父候選系譜，仍不足以授予訓練權限或宣布 RSI 成立。
研究比較產物進入 EveTrain 時須遵守其獨立權限契約、來源錨點、事件歷史與 `training_authorized = false` 等未授權邊界；本文不改寫既有 RAI Registry、M2B Grant 或本地訓練執行機制。
## 22.7 獨立 ARKE GitHub 工程的最小實作界面
未來專案應優先提供：
- 來源 RTA 的版本化查詢接口；
- 研究主張的結構化比較候選；
- 可插拔語義翻譯、形式驗證與反例檢查器；
- 帶作用域的比較結果與見證封裝；
- 符合權利契約的研究來源回訪；
- 版本更新後的受影響關係查核；
- 可重播的 `INCONCLUSIVE` 與拒絕理由；
- 獨立於任何特定 LLM、單一圖格式或論文網站的 API。
這是獨立工程的**需求接口**，不是本篇已完成程式碼實作或 GitHub 遠端合併的證據。
---
# 23. 結論：研究同一性是有型別的關係，而非一個相似度
ARKE-05 的中心問題不是「AI 能不能找到看起來一樣的文獻」，而是：**AI 應如何在真正宣稱研究完成前，自主判定自己與既有知識在哪些層次相同、不同、互相包含或仍不可判定？**
本文提出 CRRIC，將此問題從模糊的自然語言相似判斷，轉化為：
$$
\text{來源定址}
\rightarrow
\text{主張分型}
\rightarrow
\text{共同語義契約}
\rightarrow
\text{有方向的關係假說}
\rightarrow
\text{見證或反例}
\rightarrow
\text{受約束裁決}
\rightarrow
\text{知識歷程更新}.
$$
這條程序並不要求 AI 擁有完美的數學判等能力，不要求所有學術研究都被翻譯成 Lean，也不要求將人類專家設為每個常規比較步驟的強制執行者。它要求的是：**在現有可用能力的範圍內，AI 主動且負責任地完成能完成的研究對照，並對無法完成的部分留下可查核的未知。**
研究成果的同一性至少要分開看待：
$$
\mathrm{Identity}_{source},
\quad
\mathrm{Relation}_{claim},
\quad
\mathrm{Relation}_{method},
\quad
\mathrm{Relation}_{proof},
\quad
\mathrm{Relation}_{evidence},
\quad
\mathrm{Relation}_{history}.
$$
任何一項成立都不自動替其他項背書。證明相同不必等於方法相同，方法相同不必等於結論相同，結論相同不必等於先前已經有有效證明；來源歷史越早，也不會讓一份錯誤證明變成正確。
如果此方法未來取得實證支持，ARKE 的意義不只是改善自動引文，而是讓 AI 的自主研究成果能進入一個**保留歷史、辨認真正增量、可反向修正舊知識、避免錯併且能繼續演化**的知識體系。
本篇留下的實際驗證義務仍是 H1–H8。它們尚未執行，故本文只完成理論建構、文獻對照、條件命題和可否證研究設計。
下一篇 **ARKE-06** 將正式處理：在不將任何單一證明器視為所有領域的唯一裁判時，AI 如何根據研究對象選擇正確的驗證方法，並讓證據、反例、數值實驗與形式證明共同構成可追溯的研究責任。
---
# 參考文獻與公開來源（查核截止：2026-10-28）
以下僅收錄本篇實際用於定位既有研究、技術標準、公開示例的來源；資料來源不等於作者或提供者認同本篇全部理論。引用 URL 是可嘗試回訪的來源地址，其長期可用性與授權狀態仍需再次檢查。
1. **[R1]** Gauthier, T., & Kaliszyk, C. (2019). *Aligning Concepts across Proof Assistant Libraries*. *Journal of Symbolic Computation*, 90, 89–123. DOI: [10.1016/j.jsc.2018.04.005](https://doi.org/10.1016/j.jsc.2018.04.005). 作者研究頁：[University of Innsbruck](https://cl-informatik.uibk.ac.at/research/publications/publications-2018/aligning-concepts-across-proof-assistant-libraries)。
2. **[R2]** Necula, G. C. (2000). *Translation Validation for an Optimizing Compiler*. *Proceedings of PLDI 2000*, 83–94. DOI: [10.1145/349299.349314](https://doi.org/10.1145/349299.349314). 書目：[DBLP](https://dblp.org/rec/conf/pldi/Necula00.html)。
3. **[R3]** Weatherall, J. O. (2019). *Part 1: Theoretical Equivalence in Physics*. *Philosophy Compass*, 14(5), e12592. DOI: [10.1111/phc3.12592](https://doi.org/10.1111/phc3.12592)。
4. **[R4]** Weatherall, J. O. (2019). *Part 2: Theoretical Equivalence in Physics*. *Philosophy Compass*, 14(5), e12591. DOI: [10.1111/phc3.12591](https://doi.org/10.1111/phc3.12591)。
5. **[R5]** Lean Team. *The Lean Language Reference: Validating a Lean Proof*. 版本會更新，2026-10-28 查核。。
6. **[R6]** Lean Team. *The Lean Language Reference: Axioms*. 版本會更新，2026-10-28 查核。。
7. **[R7]** Barrett, C., Fontaine, P., & Tinelli, C. *The SMT-LIB Standard, Version 2.7*. SMT-LIB 官方標準入口（截至查核日含 2026 年更新）：。
8. **[R8]** Rice, H. G. (1953). *Classes of Recursively Enumerable Sets and Their Decision Problems*. *Transactions of the American Mathematical Society*, 74, 358–366. 相關介紹：[Stanford Encyclopedia of Philosophy, Recursive Functions](https://plato.stanford.edu/entries/recursive-functions/)（含 Rice 定理與非平凡語義性質不可判定的說明）。
9. **[R9]** Sutcliffe, G. (2017). *The TPTP Problem Library and Associated Infrastructure: From CNF to TH0, TPTP v6.4.0*. *Journal of Automated Reasoning*, 59(4), 483–502. DOI: [10.1007/s10817-017-9407-7](https://doi.org/10.1007/s10817-017-9407-7)。資料庫：。
10. **[R10]** Camerani, G. (2021). *The #ETH is False, #k-SAT is in Sub-Exponential Time*. arXiv:2102.02624，初次公開 2021-02-03。。**引用作早期主張存在性證據，不視為證明已獲獨立接受。**
11. **[R11]** OpenAI (2026). *The Exponential Time Hypothesis is False*. 公開稿（2026-10-25 版本資訊）：。**本篇未自行驗證其完整數學正確性。**
12. **[R12]** OpenAI (2026). *The Exponential Time Hypothesis is False — Lean Formalization Scope*. 。其文件明確區分形式化涵蓋的界限與論文的較強界限。
13. **[R13]** W3C (2013). *PROV-O: The PROV Ontology*. W3C Recommendation. 。
14. **[R14]** W3C (2017). *Web Annotation Data Model*. W3C Recommendation. 。
## ARKE 內部研究脈絡（非外部獨立驗證）
- **[I1]** Neo.K with GPT，《ARKE-01｜從答案生成到研究完備：AI 自主科研的基本義務》，v0.1，2026-10-28，原始 UTF-8 Markdown。
- **[I2]** Neo.K with GPT，《ARKE-02｜全域知識可達性：學術資料來源、合法取得與覆蓋邊界》，v0.1，2026-10-28，原始 UTF-8 Markdown。
- **[I3]** Neo.K with GPT，《ARKE-03｜來源定址、超連結與研究依賴結構：可追溯知識承接論》，v0.1，2026-10-28，原始 UTF-8 Markdown。
- **[I4]** Neo.K with GPT，《ARKE-04｜先例發現與學術新穎性：AI 自主研究的前置查核》，v0.1，2026-10-28，原始 UTF-8 Markdown。
- **[I5]** Neo.K，UCPNP 與 UNPNP 研究系列、動態速率理論與相關認知／計算研究稿。本文僅承接其「任務與成本必須顯式記帳」之研究方向；**不因引用內部稿即假定經典 P/NP、任何外部複雜度問題或 AI 能力改善已被證明**。
- **[I6]** EveTrain RAI Algorithm Registry v0.1 技術契約與研究候選系譜。本篇僅提出可選研究證據接口，不宣稱軟體已整合。
---
# 正式原稿狀態與版本紀錄
**v0.1（2026-10-28）初版：**
- 建立 CRRIC 跨表示研究同一性契約與六維研究關係；
- 明定共同比較背景、翻譯見證、非平凡性與權利限制；
- 區分命題等價、單向蘊涵、演算法功能、成本、方法、證明與證據；
- 建立有型別比較、反例、未知及歷史可追溯狀態；
- 整理 P1–P10 的條件命題與論證；
- 使用 ETH 公開研究資料作為**比較問題示範而非證明正確性判決**；
- 設計 H1–H8 實驗及公平對照，全部 `NOT_RUN`；
- 延續 ARKE-01 至 ARKE-04 的主要契約，將驗證方法本身的選擇交給 ARKE-06；
- 保留所有正式數學為原始 ` $...$ ` 與 `$$...$$` LaTeX，不以渲染畫面作為 canonical source。
**提交聲明：** 本文為正式保存的研究原稿 v0.1（形式理論與方法提案），而非已經同行評審、形式系統全面驗證或完成 ARKE 軟體實作的證明。本文的文字論證、來源引證與機器可讀示例應與尚未進行的實證分開對待。正式版本以已保存的 UTF-8 Markdown 位元組為準，若有後續修訂，須以新版本及可追溯 diff 記錄，不得從聊天渲染公式回貼取代原稿。