RGC–DPIED-10｜跨載體證據的自動發現與可信修復：依賴證據階梯、反例引導補圖與有限域契約選擇

English title: Automatic Discovery of Cross-Embodiment Evidence Dependencies: Scoped Certification, Counterexample-Guided Graph Refinement, and Contract-Constrained Repair

• 系列： 關係幾何與載體展開（RGC）× 數位—實體智能演化解耦論（DPIED）
• 篇次： RGC–DPIED-10。與原始 DPIED 系列的同號篇章不同。
• 版本／日期： v1.0｜2026-11-05
• 作者署名： Neo.K Polaris｜EveMissLab
• 研究性質： 有限狀態形式化、可證明條件、反例構造、確定性合成實驗、跨篇程式整合與候選接口設計
• 證據界線： 僅在聲明的有限模型與可呼叫的確定性求值器內成立；不代表真實物理因果辨識、實機測試、機器人控制授權或安全認證
• 唯一正式原稿： UTF-8 Markdown，數學原始碼使用 $...$、$$...$$ 作為唯一 canonical delimiter

機構： EveMissLab／一言諾科技有限公司
日期： 2026-11-05
版本： v1.0

摘要

RGC–DPIED-09 建立 CRRV-0.1（契約參照式重驗與修復）：當多機體合作中的相機、模型、致動器或共享資源改變時，若證據依賴圖完整且求值器確定，僅重新計算受影響的依賴閉包即可與整圖重算等價。然而該定理有一項關鍵前提——真正影響結論的依賴必須已被完整登記。第九篇已構造出缺漏共享能源依賴的假通過反例，但尚未把「AI 如何提出、查證、補登、撤回依賴」發展成可單獨驗證的研究接口。

本篇提出候選研究模組 EDRC-0.1（Evidence-aware Dependency Refinement and Contract Repair；證據感知的依賴精煉與契約修復）。它區分由模型提出的依賴假說、由可重現對照測試建立的存在見證、經完整有限域驗證的不存在證書、尚未決定的未知依賴，以及隨模型或版本改變而必須撤回的舊證據。此處的「依賴」首先是特定確定性求值函數的外延敏感性，不是未經干預辨識的真實物理因果箭頭。

在有限布林域下，本文證明：某變量是函數的真實外延依賴，當且僅當存在一對僅該變量不同、輸出也不同的輸入；相反地，要證明它在完整有限域中不存在依賴，必須覆蓋全部其他條件的成對比較，或使用同等有效的形式化證明。任何尚未經證明不存在的候選依賴，都保留在保守依賴超圖中。由此得出條件式結果：若候選來源宇宙完整、所有被刪除的邊都有有效的不存在證明，且第九篇的純函數、無環與一致快照假設成立，則新的保守依賴圖仍能維持增量結果與全量計算等價。

本篇實作包含一個七個布林輸入、128 種完整狀態的人工契約閘門。自適應的成對查詢順序以 72 次查詢確認六條存在依賴，並對一條無作用的來源標籤窮舉全部 64 對情境，完成受限域內的不存在證明。若對七個輸入各自做全部成對比較，需 448 對。這個查詢數節省僅是對特定真值函數和測試順序的算術結果，不等於真實因果發現效能提升。另透過直接重用 RGC–DPIED-09 的 CRRV 求值器，故意漏登 act:3 → gate:energy，讓能源由 2 增至 100 後的錯誤增量計算保持 PASS；恢復依賴後，結果與完整重算一同為 FAIL。在一組合成機體失效後的六個候選修復方案中，只有兩個同時通過聲明契約與來源證據閘門；最低標價方案因缺少可接受的來源證據而不得選入。

程式完成 56 項單元測試；獨立核對 128 個全域狀態、448 對單變量干預比較與 1,600 組能源預算／替換成本情境。本篇不主張反例引導抽象精煉、因果主動學習、依賴追蹤或假設—保證驗證是首次提出；研究增量在於把上述方法的證據階梯、適用作用域、失配處理與修復選擇，明確連到 RGC 的跨觀察者表示及 DPIED 的跨載體作用契約。

關鍵詞： 觀察者條件化；跨具身智能；證據依賴；反例引導精煉；有限域可辨識性；主動診斷；保守超圖；假設—保證契約；局部重驗；修復候選排序；模型版本；物理授權隔離；EDRC；CRRV；CACG

Abstract

RGC–DPIED-09 established a contract-referenced incremental verifier whose equivalence to full recomputation assumes complete dependencies, deterministic pure evaluators, and a coherent source snapshot. The crucial unsolved interface question is how a system should propose, verify, add, or revoke dependencies without promoting AI-generated hypotheses to proof. This paper introduces EDRC-0.1, a research-only evidence-aware refinement interface. It explicitly separates conjectured edges, functional-dependence witnesses, finite exhaustive certificates of absence, unresolved dependencies, and version-revoked evidence. In a finite Boolean product domain, a functional parent exists exactly when a paired intervention changes the evaluator's output. Non-observation of a witness does not establish absence unless the declared finite domain is exhausted or an equivalent proof is provided. A conservative graph includes both witnessed and unresolved candidate parents, removing only those whose absence has been certified. Under a complete candidate universe and the assumptions of RGC–DPIED-09, this overapproximation preserves the equivalence of incremental and full evaluation.

An exact seven-input, 128-state toy gate requires 72 ordered pair queries to identify six functional parents and prove one source label irrelevant; brute-force complete parent testing would comprise 448 candidate pairs. A deliberately omitted energy dependency in the prior six-stage CRRV evaluator produces a false incremental PASS when one robot's energy rises from 2 to 100, while complete recomputation rejects the configuration. Restoring the edge restores equivalence. A separate six-candidate synthetic repair selection rejects high-energy, workspace-conflicting, missing-channel, and unsupported-evidence options; two remain admissible under the declared model. The provided code passes 56 unit tests, plus independent enumerations of 128 states, 448 paired evaluations, and 1,600 budget-energy configurations. These are scoped mathematical and synthetic-program results, not causal discovery from physical observations, robot deployment, or safety certification.

0. 研究脈絡與篇次交接

本系列由 RGC 的「投影形狀不等於載體本身」開始，逐漸揭示多觀察者與多具身系統共享資料的不同限制。為避免概念漂移，將前九篇在本篇中的用途固定如下：

本篇不是要讓模型自主認定所有未知的物理依賴已被完整發現，而是提出一套**不允許「不知道」偷偷升格為「不存在」**的可檢查接口。這種設計也適用於 RGC-BV04 的偏振觀測：某通道從來沒有測到資訊，不能因為在已有資料中看不到其影響就將該物理通道宣告無關。

1. 與既有研究的關係及本篇增量

本篇至少與六條成熟研究脈絡相鄰。

第一，Clarke 等人在 2000 年提出的 Counterexample-Guided Abstraction Refinement（CEGAR）[E1]，早已建立反例檢查與模型精煉的自動循環。第二，Acar 等人的 self-adjusting computation [E2] 已把依賴圖與變更傳播結合；第九篇局部重算本身也具有這樣的計算基礎。第三，Chilton、Jonsson 與 Kwiatkowska 的假設—保證組件理論 [E3] 研究契約可組合性，而 Tran 等人 [E4] 討論演化式系統的回歸驗證。

第四，He 與 Geng [E5] 及 Peters、Janzing、Schölkopf [E6] 提醒：觀察分布相同的結構未必有相同的干預解釋，因果發現必須處理可辨識性與實驗選擇。第五，Necula 的 Proof-Carrying Code [E7] 提供「聲明與機器可檢驗證據應分開」的歷史先例；本篇的 JSON 記錄只借鑑此精神，不聲稱已實作 PCC 證明核心。第六，近年模組化機器人驗證 [E8] 和不完整資訊下的執行期驗證 [E9]，已顯示真實機器人中組件契約、監測盲區與環境假設的重要性。

因此，「有限函數變量敏感性」、「窮舉驗證」、「保守依賴超圖」和「先過硬閘門再按成本排序」並非新演算法原理。本篇的可辨認貢獻更精確地限於：

1. 將依賴假說、見證、證書、未知與撤回做成不同證據狀態，避免混用。
2. 證明何時可以刪除不具影響的邊，同時明確禁止以資料中沒出現反例作為刪邊理由。
3. 將「發現缺漏依賴」實際橋接到前篇 CRRV-0.1 的能源漏登記反例，而非只提出一張概念流程圖。
4. 在有限模型中把證據資格、共享資源與候選修復排序結合，區分合成契約狀態與實體授權。
5. 提供可讀取、可測試、可撤回的研究級候選接口，為觀察者視覺與跨機體作用建立一致的證據語言。

2. 四個不同層次的「依賴」不得混同

2.1 外延依賴

對一個指定求值函數 $f$，若變動某一個輸入能改變輸出，就稱該輸入在指定域中是 $f$ 的外延依賴。這是本篇主要形式化對象。

2.2 統計關聯

資料集中某個特徵 $X$ 與輸出 $Y$ 同時出現或高度相關，只能顯示樣本分布中的統計關聯。若資料收集從來沒有訪問關鍵情境，統計關聯既可能高估也可能低估實際函數敏感性。

2.3 物理因果依賴

物理因果意義上的「改變輸入會導致輸出改變」，需要明確的干預語義、可行性、干擾變量、時間結構與適用環境。不能把對 Python 函數直接改變字典欄位的結果，等同於在現場真正隔離某個機器人的物理作用。

2.4 證據可重用依賴

某結論 $q_v$ 依賴模型版本、相機校準、動作能力、共享能源及測試範圍，意味著這些資訊變動時，舊的證據可能需要重新驗證。它可以包含物理事實、數學前提與政策前提；不要求每條邊都是物理因果邊。

這四層必須分開記錄。EDRC 的已知範圍是第一層的有限域證明，並將結果轉成第四層的保守重驗接口；第二、三層仍有額外實證要求。

3. 形式化：來源宇宙、外延支持與證據狀態

3.1 有限求值模型

給定一個證據節點 $v$，定義候選來源宇宙 $U_v$，每個來源 $u$ 的取值域為 $\mathcal X_u$，固定的確定性求值器為：

本篇的可執行實例令 $\mathcal X_u=\{0,1\}$， $\mathcal Y_v=\{0,1\}$。在真實系統中，觀察者姿態、時鐘、影像張量、機體能力等通常不是布林值；本篇沒有將這些複雜域偷換為已經完全證明的布林模型。

對某一來源 $u$，其外延支持定義為：

其中 $x_{-u}$ 固定其他所有來源。若 $u$ 在支持集合中，稱它為「已存在外延依賴」。即使存在依賴，也不意味著它在每次輸入變更時都會改變輸出。

3.2 依賴證據狀態階梯

對一條候選邊 $u\rightarrow v$，定義：

• HYPOTHESIS_ONLY：AI 或啟發式提出猜測；沒有可單獨核驗的充分證據。
• PRESENT_WITNESS_IN_TOY_MODEL：找到一對合法固定其他輸入的不同輸出，證明在被鎖定的有限模型內依賴存在。
• ABSENT_EXHAUSTIVE_IN_TOY_MODEL：全部合法對照情境都已檢查且無見證，證明在被鎖定的有限模型內不存在該依賴。
• UNKNOWN_NOT_EXHAUSTED：迄今未有存在見證，也未完成不存在證明；不得被當成不存在。
• REVOKED：求值器版本、域、政策或來源語義發生會使舊證據失效的改變，原證據不可沿用。

嚴格說，HYPOTHESIS_ONLY 是獨立的假說欄位，不是可取代其餘四種證據狀態的通過章。這是避免 AI 用自我宣稱轉換權威的刻意設計。

3.3 對外的保守依賴集合

令 $W_v$ 是有有效存在見證的輸入集合、 $A_v$ 是在同一域中已嚴格證明不存在依賴的集合、 $Q_v$ 是尚未完成決定的集合。對已知候選宇宙，使用：

這是一張保守超圖：可能包含實際上不存在的邊，因此重新計算成本可能較高，但不會因僅有猜測而把未知依賴刪除。若求值器有未列入 $U_v$ 的輸入，完整性前提已失效；上述結論不能外推。

4. 定理一：有限域存在見證與不存在證書的不對稱

定理 4.1｜布林有限域依賴判準

令 $f:\{0,1\}^n\to\{0,1\}$ 是固定的確定性函數。對第 $i$ 個輸入，定義成對差異：

則：

且：

證明。 第一式由支持集合的定義直接成立。第二式是第一式的否定，其布林域上等價於對所有其他輸入情境皆沒有差異。由於 $\{0,1\}^{n-1}$ 有限，能以至多 $2^{n-1}$ 組成對比較窮舉，或透過有效符號證明完成同等核驗。證畢。

推論 4.2｜見證可以早停，不存在不可以任意早停

若某組對照輸入已呈現 $\Delta_i f=1$，不須額外比較全部情境，即可確認存在外延依賴。但若目前測得的所有 $\Delta_i f$ 都為零，且仍有某組合法情境未檢查，在未提供額外結構性證明的情況下，不能確認依賴不存在。

證明。 在任何尚未測試的情境 $x_{-i}^{\star}$ 上，構造兩個與既有測試完全一致的候選函數；其中一個在該組情境不隨 $x_i$ 改變，另一個只在該組情境令兩種 $x_i$ 值對應不同輸出。兩者都符合先前所有觀察，卻對依賴是否存在給出相反結論。故未測試情境無法被邏輯省略。證畢。

這項反例尤其針對一種常見的錯誤流程：AI 在訓練資料沒有觀察到「攝影機姿態改變影響控制」的案例，就刪除姿態依賴。若這種影響只在特定表面、光照、接觸或干擾條件下顯現，直接刪邊就可能使下游證據錯誤重用。

5. 定理二：保守超圖支援的增量重驗正確性

設第九篇的衍生證據圖 $G_P=(B\cup Q,E_P)$ 為有限有向無環圖， $B$ 是基礎來源， $Q$ 是衍生節點；每個 $v\in Q$ 由純確定性函數 $f_v$ 求值。假設每個節點的真正外延支持都包含於聲明的 $D_v^{\mathrm{safe}}$ 中，所有模型版本與快照條件不變，且改變的來源集合 $\Delta$ 完整列出。

定理 5.1｜保守依賴閉包充分性

若：

則沿 $D_v^{\mathrm{safe}}$ 構造的依賴圖，對 $\Delta$ 的後繼閉包進行拓樸重算，結果與在新快照上完整求值相同：

證明。 依拓樸順序歸納。受變更閉包影響的節點，以相同新來源及相同前驅值進行同一函數求值；不在閉包內的節點，由於所有真正可能改變其結果的來源皆被包含在超圖中，因此其實際輸入支持未改變，保留舊值與新快照全量重算相等。歸納完成。證畢。

此定理是 RGC–DPIED-09 定理 5.1 的保守依賴形式，不聲稱超圖是唯一或最小的依賴圖。未知依賴愈多，超圖愈密，增量重驗成本可能逼近甚至超過全量重算。安全性是由正確的支持集合上界提供，不是由節點重算數字少提供。

5.2 本篇的真正技術邊界

這個證明依賴於 $U_v$ 本來就包含全部可能影響輸出的變量。真實環境的未知接觸材料、未監控頻譜、第三方機體、網路抖動與未申報模型更新可能根本不在此集合中。任何有限域內的不存在證書，只能保證其指定的求值函數與作用域；它不會變成「全宇宙不存在這條物理關係」的證明。

6. 定理三：受限觀察分布可以永久遮蔽一條依賴

第六篇討論過：若正常與未知感測模式在既有資料分布中不可區分，單靠被動增加資料可能無法發現失配。本篇對依賴發現建立對應反例。

取兩個二元來源 $c,i\in\{0,1\}$，令：

假設被動資料永遠來自 $c=0$ 的支持集 $S$。則：

在 $S$ 之內，兩個模型對所有觀察完全一致；即使將同一支持集的資料重複任意多次，也無法依其輸出區分模型。然而，當可行且合法的介入設定 $c=1,i=1$ 時：

命題 6.1｜受限支持的觀察不可辨識

若兩個候選函數在被動資料支持集上完全一致，而存在合法干預情境使其輸出不同，則單靠該支持集的被動輸出觀察，無法在兩候選間作出無誤的模型辨識。

證明。 任意由支持集輸出所構成的資料序列，在兩模型下具有相同的可觀察值；判定器若根據該序列選擇某模型，另一模型也可能生成相同序列。因此無法對兩者都保證正確。加入區分性干預可破壞此等價，但干預是否可執行是另一個物理問題。證畢。

本篇的七輸入契約實例共有 $2^7=128$ 種人工狀態；令其中 camera_calibrated=False，剩下 64 種狀態。在這個受限支持內，上述兩類模型依然可能完全一致。這種限制不能被誤讀成「AI 永遠無法學到」；若額外資料覆蓋關鍵條件、具備可靠干預，或者模型含有更強的可辨識先驗，問題可能消除。

6.2 為何這與 RGC 生物視覺有直接關係

生物視覺系統的感測通道、光學排列與主動掃描策略可能不同。即使將影像都轉成相同形狀的數位張量，某些本來不在來源感測通道中的資訊仍不會憑資料格式統一而出現。RGC-BV04 的偏振案例提供的是理想測量算子的盲區例子；本篇進一步說明，若缺乏某類干預或改變觀測條件的可能性，AI 也可能無法從既有支持集分辨多種不同的依賴結構。

此處的概念連結不能擅自上升為螳螂蝦、跳蛛或扇貝的神經視覺機制已被模型證實；生物的視覺幾何與偏振通道仍須各依其實際感測模型、波段、時間及環境分別研究。

7. EDRC-0.1：候選接口與證據流程

7.1 六個邏輯環節

EDRC 研究候選接口依序操作：

1. 來源宇宙登記。 宣告可能的觀察者、座標與時間來源、機體能力、共享資源、模型版本、政策約束及資料來源；未知來源保留 OUT_OF_SCOPE。
2. 假說提出。 AI 可以依語言、靜態程式分析、錯誤追蹤或既有資料推薦可能的依賴邊及優先測試順序，但假說不能直接用來排除其他邊。
3. 可行對照測試。 在允許的合成或隔離實驗中，盡可能固定其他來源，改變目標來源；記錄完整上下文、兩次輸出與模型版本。
4. 證據歸類。 若輸出確有差異，將該邊加入存在見證；若全部合法有限域都已覆蓋且無差異，才可標記為域內不存在；否則保持未知。
5. 保守圖修正。 在受控模型內，已存在與未知的邊都留在重驗圖中；只有具有有效不存在證明且證據版本吻合的邊可以刪除。
6. 修復候選驗證。 對每個候選方案先確認來源版本、作用契約、共享風險／能源／時序／空間與證據接受條件，最後才比較人工宣告的成本。

這裡的「自動發現」是自動提出及檢查可檢驗模型下的依賴，不是賦予 AI 對未觀測物理世界自由試探或致動的權限。實體探測仍須獨立的安全範圍、設備控制與人／系統授權。

7.2 允許保守降級而非虛構通過

當證據不足時，接口可以選擇：保留全部候選依賴、暫停復用舊證據、在模型中完整重算、請求合法新觀測、對候選方案作離線模擬，或標記必須外部驗證。它不能把 UNKNOWN_NOT_EXHAUSTED 自動修改成 ABSENT_EXHAUSTIVE_IN_TOY_MODEL。

若某候選來源不在已宣告的 $U_v$，則不應在「依賴圖已完整」的前提下給出有保證的局部重驗結果。真正保守的做法不是聲稱已補正，而是撤回該作用域的完整性宣告，回到模型更新或隔離驗證。

7.3 證據版本與撤回

每份證據至少綁定 $\kappa=(\text{model},\text{domain},\text{semantics},\text{epoch})$。若任一關鍵項改變而舊證據沒有可檢查的跨版本等價證明，便必須將其標記 REVOKED，不得再用於刪除依賴。

本篇可執行原型以文字版本 ID 與完整記錄的 SHA-256 摘要作為資料一致性檢查；它沒有提供硬體來源認證、簽章信任鏈、時鐘同步證明或分散式共識。因此SHA-256 不是「資料來自真實感測器」的證明，文字版本 ID 也不保證內容未遭替換。

8. 有限實驗 A：七輸入契約閘門

8.1 人工求值函數

定義七個布林變量：

人工閘門為：

因此，若所有基本條件均通過，且「沒有干擾或存在清空空間」，模型內就返回 PASS。變量 $\ell$ 雖然存在於輸入結構中，卻不參與求值。

全域共有 $2^7=128$ 個可能的布林指派，其中 6 個指派令 $g=1$。請注意，這是研究者刻意設計的合成真值函數，不是從真實機器人的安全資料擬合得出的自然法則。

8.2 有限域發現結果

使用對其他輸入優先設定較多真值的啟發式排序，每條候選邊的完整理論成對情境數都是 $2^6=64$。實際查詢如下：

完整逐變量成對枚舉需要 $7\times64=448$ 組；本次利用早停見證與完整不存在檢查，只用了 $72$ 組。查詢占比是 $72/448\approx16.07\%$，在此特定案例中比完整逐邊枚舉少 $376$ 組。這不代表平均測試成本可以普遍下降 83.93%；若依賴見證埋藏得很深，或大多數變量真的不存在依賴，查詢量仍可接近全部 $448$ 組。

尤其對 $\ell$，查完第 63 對而尚未看到差異，狀態仍必須是 UNKNOWN_NOT_EXHAUSTED；直到第 64 對也無差異，才允許在這份固定布林函數的依賴圖中刪除它。

圖 1： figures/01_pair_query_asymmetry.png，顯示「很快找到存在見證」與「完整證明不存在」的查詢量不對稱。

8.3 不變量、量化邊界與無法泛化之處

實驗裡所有測試都是直接呼叫純 Python 真值函數，且輸入可以在有限域內任意設定。這些條件使查詢結果不受雜訊、設備故障、延遲、時間變化與合法干預限制影響。真實生物視覺與機器人完全不具備這些便利條件；若只能進行被動觀察，或者介入會改變其他物理條件，成對比較的「固定其他輸入」前提可能根本不成立。

9. 有限實驗 B：把缺漏邊找回 RGC–DPIED-09 的 CRRV

9.1 原始六段合成作用契約

第九篇的 CRRV-0.1 ContractGraph(6) 將六台機器人的觀察、動作、交接及共享能源、期限、風險、模型誤差與空間閘門結成 23 個衍生證據節點。每台機體的基線能源需求是 2，總需求為 12，人工預算為 16，原始模型得到 release=PASS。

真實聲明依賴圖中包含：

即第 3 號機體動作的能源需求，對共享能源閘門的求值具有影響。

9.2 故意刪除證據依賴

為了重現第九篇的漏洞，實驗不修改能源閘門本身的真實求值函數，而是故意在增量驗證的反向依賴索引中漏掉上述邊，造成「求值器仍會使用該值，但重驗閉包不知道這件事」的錯誤。

將 robot:3.energy 從 2 改為 100，其他五台仍各為 2：

結果如下：

此處的 8 與 9 只表示所使用的六段人工證據圖中重新求值的節點數。完整重算會求值 23 個衍生節點；並非修補一條依賴邊即可保證所有真實機器人系統得到同樣的工作量節省。

圖 2： figures/02_missing_dependency_false_pass.png，直接展示「錯誤快取通過／全量拒絕／修補後增量拒絕」的差異。

9.3 反例引導的補圖程序

若同一新快照上 incremental 與 full 結果不相同，可先將差異當作待診斷反例。然而，不能因為最終 release 不同，就直接推斷是哪一條物理因果邊失效；差異也可能來自求值器不純、版本不一致、事件漏記、快取損壞或來源污染。

本例可進一步檢查 gate:energy 的直接求值：保持其他五個動作與共享政策不變，只改變第 3 號動作的能源，能源閘門由通過轉為失敗。這是模型內的直接外延見證，因而能對候選依賴 act:3 → gate:energy 給出修正理由。補回該邊後，針對同一快照重新求值，與全量結果完全相同。

這與 CEGAR 的精神相近，但本篇的補邊步驟只針對可直接查詢的有限函數依賴，並不包含一般程式符號模型檢查器、自動證明器或完整的物理環境因果推斷。

10. 有限實驗 C：證據閘門先於修復成本

10.1 失效情境與候選集

在第九篇 EpochStore(6) 中，先令第 3 號機器人的 enabled=False 並以已發生事件更新版本。此時模型內 release=FAIL。研究者另外建立六個假設性替代方案；它們均只在隔離快照中運算，沒有任何硬體致動命令。

定義方案 $p$ 的聲明成本 $c(p)$ 、模型契約結果 $K(p)$ 、來源證據資格 $E(p)$ 及來源版本有效性 $V(p)$。僅將下列集合列為研究模型中可排名的候選：

成本排序只允許在此集合中進行：

若該集合為空，正確結果是 HOLD_OR_REJECT，不是把最便宜的失敗方案當作可行替代。

10.2 精確候選結果

可見在這份由研究者宣告的有限候選集中，成本最低的方案仍不能列入合格方案。這裡 synthetic_evidence_accepted=True 只是預先定義的人工模型資格欄位，不是感測器確實提供了被第三方驗證的實體證據；我們的目的只是驗證「證據資格與模型通過是兩個不同閘門」這個接口設計。

圖 3： figures/03_repair_cost_after_gates.png，以成本標示六個候選並標註通過／拒絕。它不代表商業、工業或實機維修價格。

10.3 提案、提交與實體授權分離

本篇只對候選產生 SHADOW_CONTRACT_SELECTION_ONLY，並固定輸出 physical_authorization=NOT_GRANTED。即使某方案在人工模型中 PASS，也不意味著已經提交到真實機器人。本篇將權限分為三層：

• 研究候選： 方案是可比較的數學／合成狀態。
• 來源證據： 有足夠聲明範圍內的證據支持某項模型判斷。
• 實體作用授權： 由獨立控制、安全、法律與設備權限機制決定；本篇完全沒有提供。

以上三層不得被單一 PASS 字串合併。這一點延續 DPIED-04 的「看見不等於能操作」及 RGC–DPIED-07 的「作用契約不等於致動許可」。

11. 反例引導依賴精煉的研究演算法

本篇的算法依照「證據不升格」原則設計。簡化的偽程式如下：

INPUT:
    fixed, versioned deterministic evaluator f_v
    declared finite source universe U_v
    old certificate ledger L_v
    change snapshot sigma_new

1. IF evaluator version or domain changed:
       revoke old absence certificates
2. FOR each candidate source u in U_v:
       if present witness exists: retain edge
       else if all legal paired contexts checked and no witness:
           certify absence only within this model/domain
       else:
           retain UNKNOWN edge conservatively
3. BUILD safe graph using PRESENT + UNKNOWN edges
4. RECOMPUTE invalidation closure under the new snapshot
5. IF a separate full check finds a discrepancy:
       mark that discrepancy as a diagnosis candidate
       seek a direct scoped witness for omitted dependencies
       repair the graph only after the witness is checked
6. FOR each hypothetical repair plan p:
       check source epoch, model gates, global constraints,
       source evidence, and permitted task scope
7. SORT only model-admissible candidates by declared cost
8. OUTPUT shadow recommendation / HOLD_OR_REJECT
   NEVER output physical actuation authority

11.1 有限模型中終止的充分條件

若 $U_v$ 有 $n$ 個二元來源、求值器在全部 $2^n$ 個指派上確定且可呼叫，每條邊至多需 $2^{n-1}$ 組成對比較便能取得存在見證或不存在證書。因此直接全面辨識的上界為：

EDRC 的實驗使用查詢順序與早停見證減少實際執行的對照比較數，但不改善這個最壞情況上界。若輸入域不是有限離散集合，或者無法合法介入所有其他條件，則這個終止證明不成立。

11.2 未知依賴不是一個可以忽略的零權重

對仍未知的候選邊，系統可以依照任務重要性、可能風險和可取得的資料安排查詢順序。這只影響資源配置；除非已有可驗證的不存在證書，不能因為其預測權重很低，就將其從安全關鍵依賴圖中刪去。

對於具身 AI，某條依賴也許在一般畫面極少觸發，卻在失去抓取、機器臂進入死角或共享空間重疊時決定安全。稀有事件的低頻率不能自動推論為結構上不存在。

11.3 高階候選模型提供搜尋方向，不提供證明

AI 可以提出「共享能源可能影響該機器人動作」「偏振通道可能影響該材料辨識」「攝影機姿態改變可能導致投影歧義」等假說。這些假說可交給可解釋的證據程序測試：靜態相依分析、形式化模型查詢、實驗設計或受控硬體診斷。當資料不足時，應回報證據不足而非捏造測量。

本篇原型並未連接外部 LLM，自動部分是有限輸入的窮舉、證據分類、保守圖構建與合成方案檢查；不應以此聲稱已完成自然語義依賴的 AI 自主發現。

12. 版本、作用域與證據權限契約

12.1 一份合格的模型內證據記錄應包含什麼

對 source → dependent 的聲明，證據至少應保存：

• 來源與目標證據節點的穩定識別；
• 求值器與輸入域的版本／語義，以及接受的測試環境；
• 所有測試的上下文與輸出，或可交由可信驗證器重查的證明物件；
• 存在見證或不存在證書的有效作用域；
• 是否包含未測試的合法情境；
• 時間、失效條件、來源資料可追溯資訊及其可信性分類；
• 本研究是否具備外部物理測量、第三方證明或控制授權——本篇一律沒有。

本篇示例把這些欄位編成 schemas/edrc01_evidence_and_repair_example.json，並以 results/exact_results.json 保存完整有限實驗輸出。SHA-256 用於辨識封裝內容是否在未說明的情況下改變；它不是對檔案「真實性」或感測器身份的獨立認證。

12.2 觀察者條件的版本鏈

在 RGC 視覺接口中，來源名稱不一定足以描述一次觀察。較完整的證據依賴會包括：

若攝影機已重新標定，或者來源影片的投影規則與訓練資料標記不同，即使資料仍稱為同一個 camera_id，既有補正證據也可能不再適用。類似地，不同物種的可見頻譜、空間取樣模式與時間掃描不能單靠「RGB 張量大小相同」就視作共同物理觀察。

本篇 EDRC 無法自動創造缺失的偏振、深度或接觸通道。它最多能幫助系統將這種缺口保留為未滿足的任務與觀察前提，避免錯誤地從其他資料來源借用已失效的證明。

12.3 作用與觀察的證據不得互相越權

一個反例證明「攝影機姿態影響了目標判斷」，不等於已證明「某個抓取策略仍可安全執行」。反之，某台機體在局部任務上的歷史成功，也不意味著另一台機體在不同觀察通道、致動方向或共享時序下可直接沿用。

因此 EDRC 只對證據圖提供保守重驗建議；所有跨具身作用仍須滿足 CATC-0.1、CACG-0.1 與 CRRV-0.1 中明確聲明的候選契約及獨立授權邊界。

13. 可重現性驗證及獨立核對

13.1 測試結構

本篇提供 src/edrc_core.py（有限依賴發現與修復候選）、src/crrv09_reference.py（保留第九篇人工契約求值器的參照副本）、src/independent_audit.py（獨立布林條件及能源算術核對）、src/render_figures.py（研究圖）、tests/test_edrc.py（單元測試）。

測試明確涵蓋：

1. 輸入結構與布林值驗證；
2. 全部有限狀態及合法成對情境；
3. 有見證、無見證、未窮舉與重複查詢的區分；
4. 模型版本撤回及舊證據不能被重用；
5. 候選圖漏掉能源依賴時的錯誤通過；
6. 恢復依賴後的增量／全量一致性；
7. 修復方案的能源、空間、感測通道及來源資格閘門；
8. 舊版本方案在來源事件更新後的拒絕；
9. 產出只限於合成研究候選、不得授權實體作用。

13.2 驗證紀錄摘要

本篇 56 項單元測試是測試方法數，並不表示 56 組互不重複的真實世界實驗。各窮舉數字也都是依人工域定義計數，不應與不同篇章的檢查數量相加後當作「實機驗證次數」。

13.3 執行命令

在 Python 3.11 以上、已安裝 matplotlib 的一般環境，可於本篇研究包根目錄執行：

PYTHONPATH=src python -m unittest discover -s tests -v
PYTHONPATH=src python src/edrc_core.py
PYTHONPATH=src python src/independent_audit.py
python src/render_figures.py
python validate_release.py

Windows PowerShell 可以將第一行改為：

$env:PYTHONPATH = 'src'
python -m unittest discover -s tests -v

真正的發行驗證會獨立檢查 UTF-8、數學分隔符、受控檔案清單、程式測試及逐檔 SHA-256。所附的 validate_release.py 不會連接攝影機、機械手臂、外部網路或現場感測器。

14. 失效模式與威脅界線

14.1 候選來源宇宙不完整

若某未知因素從未列入來源宇宙，則 UNKNOWN 仍不是安全的完整描述。它不是已知候選集合中的未知邊，而是集合之外的未知因素。本篇的保守超圖只能處理完整列入候選域的來源；不能用它保證開放物理世界中的因果完備。

14.2 求值器非純函數或版本未鎖定

時間、隨機狀態、隱藏快取、未登記的模型更新、雲端回應變動等，都可能使原本同一組輸入產生不同輸出。若這些來源沒有被列入函數參數及快照，有限對照測試所謂的「其他條件固定」可能只是錯覺。EDRC 只提供檢查接口，沒有替任意外部模型提供純函數性證明。

14.3 稀有事件與違反干預可行性

偏振、光譜、快速視覺掃描、接觸力和共享環境，可能無法安全地被單獨操控。這時不能用人工改一個布林欄位的效果替代真實干預。受限測量若覆蓋不到某些情境，應標記缺口，而非自動產生完整不存在證書。

14.4 共享依賴與共同原因

兩台機器人可能共用能源、網路、時鐘或狹窄通道。即使它們看起來沒有直接交接，也可能透過共同原因影響同一安全閘門。單看任務圖的直接相鄰關係，不能推得證據依賴完整；這正是第八、九篇已出現的主要風險。

14.5 故意污染證據與模型自我認證

模型生成的自然語言說明、測試檔、版本字串或來源名稱都可能包含錯誤。若由同一系統生成聲明並自行相信該聲明，僅因其文句完整而標記可信，就形成循環認證。真正的證據需要可隔離的驗證語義、必要時的可信來源及獨立監控。本篇的合成證據閘門只示範此設計，未實現對抗惡意硬體或軟體來源的安全機制。

14.6 增量驗證與安全監控不等同

在指定快照上得到模型內 PASS，與系統已在真實時間內避免碰撞或穩定完成任務，是不同結論。多機體的真實併發、時間期限、恢復競態、網路分割、執行器溫升與其他物理限制，均未由此有限模型覆蓋。任何實機部署必須保留獨立安全控制與授權機制。

15. 與跨觀察者視覺補正的統一接口

RGC–DPIED 系列最初面對的是「不同存在以不同觀察幾何取得世界投影，能否互相轉換並用於物理作用」。經十篇展開，可將研究接口整理為：

上述是接口依賴關係，不是一條保證任何資料都可轉換、任何機器都可協作的物理定律。它提醒我們：世界模型不只要表示「觀察到了什麼」，還要表示「該結論依賴哪些仍有效的觀察與作用前提」。

新的 EDRC-0.1 在這條鏈上的功能並非取代視覺感測、世界模型或作用控制，而是避免 AI 把自己尚未確定的關係當作已經不存在、把自己提出的修復說明當作已經驗證的證據。

這帶出一個可以用於後續工程設計的研究主張：對跨具身系統而言，維護「哪些資訊不可信、哪些前提尚未被證明」的能力，可能與維護「哪些資訊已經被理解」同樣重要。 本篇的有限結果只能支持此主張的形式化必要性，尚未量測它是否能讓一般視覺模型、VLA 訓練或實體機器人普遍獲益。

16. 結論

第九篇已證明，完整證據依賴下的局部重驗可以與全量重算一致，也已指出缺漏共享依賴會造成錯誤放行。第十篇將焦點轉向：誰有權斷言依賴存在或不存在，以及這項斷言必須附帶什麼可檢查的理由？

在一個確定、有限、完整宣告的布林求值域中，存在依賴可以由單一可重現的成對反例證明；不存在依賴則必須被全面覆蓋或正式證明。把未知邊保留在保守依賴超圖，可在既有增量求值條件下維持計算正確性；但一旦來源宇宙、物理觀測、模型版本或干預語義超出聲明範圍，這種保證就應撤回，而不是向外無限延伸。

本篇實際重現並修補 CRRV 的一項漏登記能源依賴，並建立先驗證契約及證據資格、再比較成本的有限修復選擇。所有定量結果都已提供程式與原始數據供重算；沒有宣稱已完成機器人的因果發現、在線自動修復或安全認證。

核心結論：

當智能開始自主修復世界模型，真正需要守住的，不是每一個猜測都能變成答案，而是每一個答案都知道自己依賴哪些尚未失效的前提。

參考文獻與來源核對

[E1] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2000). Counterexample-Guided Abstraction Refinement. CAV 2000, 154–169. DOI: https://doi.org/10.1007/10722167_15

[E2] Acar, U. A., Blelloch, G. E., Blume, M., & Tangwongsan, K. (2006). An Experimental Analysis of Self-Adjusting Computation. PLDI 2006. DOI: https://doi.org/10.1145/1133981.1133993

[E3] Chilton, C., Jonsson, B., & Kwiatkowska, M. (2014). Compositional Assume–Guarantee Reasoning for Input/Output Component Theories. Science of Computer Programming, 91, 115–137. DOI: https://doi.org/10.1016/j.scico.2013.12.010

[E4] Tran, H.-V., Hung, P. N., Nguyen, V.-H., & Aoki, T. (2020). A Framework for Assume-Guarantee Regression Verification of Evolving Software. Science of Computer Programming, 193, 102439. DOI: https://doi.org/10.1016/j.scico.2020.102439

[E5] He, Y.-B., & Geng, Z. (2008). Active Learning of Causal Networks with Intervention Experiments and Optimal Designs. Journal of Machine Learning Research, 9, 2523–2547. https://www.jmlr.org/papers/v9/he08a.html

[E6] Peters, J., Janzing, D., & Schölkopf, B. (2017). Elements of Causal Inference: Foundations and Learning Algorithms. MIT Press. https://mitpress.ublish.com/book/elements-of-causal-inference

[E7] Necula, G. C. (1997). Proof-Carrying Code. Proceedings of POPL 1997, 106–119. https://homes.cs.washington.edu/~mernst/teaching/6.893/readings/necula-popl97.pdf

[E8] Luckcuck, M., Farrell, M., Ferrando, A., Cardoso, R. C., Dennis, L. A., & Fisher, M. (2026). A Compositional Approach to Verifying Modular Robotic Systems. Robotics and Autonomous Systems, article 105648. DOI: https://doi.org/10.1016/j.robot.2026.105648

[E9] Ferrando, A., & Malvone, V. (2026). Runtime Verification via Rational Monitor with Imperfect Information. ACM Transactions on Software Engineering and Methodology, 35(3), article 74. DOI: https://doi.org/10.1145/3735130

[INT-01] RGC–DPIED-01 v1.1：跨觀察者視覺補正的可實現性與 BV04 整合；系列既有本地原稿。

[INT-07] RGC–DPIED-07：跨載體任務遷移的可證充分性、作用實現與物理行動契約；系列既有本地原稿。

[INT-08] RGC–DPIED-08：跨載體作用契約的組合閉合、長程誤差、共享風險與多機體協同；系列既有本地原稿。

[INT-09] RGC–DPIED-09：多機體協同中的動態重規劃、局部修復、證據依賴閉合與契約重驗證；本篇直接重用其 repair_core.py 的參照副本。

來源可追溯性註記

外部學術文獻僅用於說明方法來源、已知先例與研究邊界；數值結果全部由本包明示的人工函數、測試與輸出產生。研究包內另外提供 SOURCE_TRACEABILITY.md 說明每項主要主張的原始檔、相應驗證與不能外推的範圍。

附錄 A｜七輸入有限模型的直接證明

由人工函數：

可知 $c,a,p,h$ 的存在見證可以令其餘三個基本必要條件為真，並選擇 $i=0$ ；此時分別切換其中一個必要條件，輸出由 1 變 0。對 $s$，令 $i=1$ 且 $c=a=p=h=1$ ；切換 $s$ 會改變結果。對 $i$，令 $s=0$ 且 $c=a=p=h=1$ ；切換 $i$ 會改變結果。對 $\ell$，函數的解析形式完全不包含它，因此對任何其他六個布林輸入，切換 $\ell$ 都不影響結果；程式亦逐一驗證全部 64 對。

這個解析證明與窮舉測試使用的是同一人工函數的兩種確認方式，不是來自兩組獨立的物理資料。

附錄 B｜完全發現與保守維護的偽碼

for source in declared_source_universe:
    status[source] = UNKNOWN
    for context in legal_paired_contexts(source):
        before = evaluator(context + source=0)
        after  = evaluator(context + source=1)
        record(context, before, after, model_version)
        if before != after:
            status[source] = PRESENT_WITNESS
            break
    if status[source] == UNKNOWN and every_context_was_checked:
        status[source] = ABSENT_EXHAUSTIVE

safe_dependency_set = {
    source for source in declared_source_universe
    if status[source] != ABSENT_EXHAUSTIVE
}

if model_version_has_changed:
    invalidate_all_old_certificates()
    restore_all_candidates_to_unknown_until_rechecked()

這裡 legal_paired_contexts 必須涵蓋所有被聲明合法的有限情境；若受物理限制無法覆蓋，不能把它替換成任意可存取的資料子集後仍宣稱已證明全域不存在。

附錄 C｜實驗輸出與主張對應

正式結論以 UTF-8 原始文件與驗證檔為準。聊天渲染畫面不是數學原稿的權威來源。