雙迴圈自適應：索引—分離耦合動力學

Dual-Loop Adaptation: The Coupled Dynamics of Index and Separation

文件編號：EML-TC-DLA-2026-v0.2 作者：Neo.K（許筌崴） 機構：EveMissLab（一言諾科技有限公司），台灣 理論結晶化協作：Theia 日期：2026年6月13日 版本紀錄：v0.1 初版（Python 實測通過）；v0.2 附錄 C 由計畫改寫為驗證結果（DLA1–DLA3 機器驗證關閉），第四章存在性誠實降級（Brouwer 在假設欄）、第五章快慢分離措辭收斂、第六章攻擊面二結論補入 機器驗證狀態：耦合定位定理（完整證明）、不動點存在性（條件級——連續性已驗、Brouwer 性質為顯式假設）、條件收斂（陳述級）已於 Lean 4 完成形式化，三攻擊面內建為驗證項，全專案 0 sorry／0 axiom（詳附錄 C） 理論地位：自適應切割（ADC）與分的統一（FEN-UNI）的合流——處理兩篇各自留下的公開問題「耦合情形」 前置文件：EML-TC-ADC-2026-v0.2、EML-FEN-2026-UNI-v0.2、EML-TC-ONT-2026-v0.2、EML-TOPO-2026-SUB-v3.2

摘要

自適應切割證明了索引分量的最優化是訊源編碼，前提是查詢分布固定。分的統一證明了任意切割分解為索引分量與分離分量，並指出當成本可加時兩個最優化逐分量並行。兩篇都在同一個地方收手：當兩分量耦合時怎麼辦——分離決策改變查詢分布（把熱資料分離出去，索引面對的 Q 就變了），索引結構洩漏分離安全（索引是查詢者興趣的對數指紋）。本文處理這個被兩篇共同擱置的耦合情形。

核心立場：耦合問題的正確形態不是一個更大的聯合最優化，而是兩個自適應迴圈的耦合動力學——idx 迴圈（按查詢分布調索引解析度）與 sep 迴圈（按使用模式調量場劃分）各自運轉，各自的輸出成為對方的輸入分布。本文建立這個雙迴圈系統並給出三組結果。第一，耦合的精確定位：全部耦合項發生在回饋通道上，兩迴圈的內部動力學（各自的免疫性、各自的守恆律）不受耦合影響——這把耦合從「無處不在的糾纏」收窄為「兩個明確的跨迴圈信號」。第二，不動點的存在性：在溫和條件（兩迴圈各自的最優響應連續、量場與查詢空間緊緻）下，雙迴圈系統存在共適應不動點——一個索引方案與分離劃分互為最優響應的穩定配置；證明訴諸 Brouwer 不動點定理。機器驗證揭示一個誠實降級（v0.2）：連續性那一肢已被完整證明（含軟最優響應的連續性鏈），但 Brouwer 不動點定理本身在當前 Mathlib 快照中無穩定可複用的形式，故存在性目前是條件證明級——連續性已驗，Brouwer 性質作為顯式狀態空間假設，待庫補齊後兌現為完整證明級。第三，非對稱可逆性的動力學後果：idx 迴圈住在 d 軌（免疫、可逆、可激進），sep 迴圈住在 V 軌（有損、不可逆、須保守），這個本體論非對稱使雙迴圈的正確調速是不等速的——idx 快迭代探索、sep 慢迭代承諾，快慢分離不是調參技巧而是兩條軌道風險結構的直接命令。

本文同時誠實標明可形式化邊界：不動點的存在性可陳述級形式化，唯一性與收斂性依賴耦合映射的壓縮性質，後者一般不成立（可有多個共適應均衡），故收斂只在壓縮條件下局部保證——這條邊界本身是結果，它告訴系統設計者：共適應可能落入次優均衡，逃離需要外部擾動。附錄含 Python 參考實現（雙迴圈交替迭代至共適應不動點、量場—查詢耦合的實測、多均衡現象的展示）與 Lean 4 形式化計畫（存在性陳述級、免疫性與守恆律的迴圈內保持可直接複用既有庫）。

關鍵詞：雙迴圈自適應、耦合動力學、共適應不動點、Brouwer 定理、回饋通道耦合、快慢分離、多均衡、d 軌/V 軌非對稱

第一章　兩篇論文撞上的同一堵牆

1.1 各自的收手處

自適應切割（ADC）的全部定理建立在一個假設上：查詢分布 Q 平穩，或至多緩慢漂移。在這個假設下，最優索引是 Q 的訊源編碼，貪婪迭代收斂到共形像。ADC 的第六章接口段坦白了這個假設的脆弱：「分離決策改變查詢分布——把熱資料分離出去，索引的 Q 就變了」，並把這列為「雙迴圈自適應」的未來工作。

分的統一（FEN-UNI）的最優化版圖建立在另一個假設上：成本函數對分解可加，於是索引最優化與分離最優化逐分量並行、互不干擾。FEN-UNI 的第六章同樣坦白：成本不總可加，「典型耦合——分離決策改變查詢分布、索引洩漏影響分離安全」，並把耦合情形「送回姊妹篇的框架，以雙迴圈自適應列為兩篇共同的未來工作」。

兩篇從不同方向走來，撞上同一堵牆，並且不約而同地把牆後的房間命名為同一個名字。本文進入那個房間。

1.2 為什麼耦合不能用「更大的最優化」解決

面對兩個耦合的最優化，標準反射是把它們合併成一個更大的最優化：把索引方案與分離劃分都當決策變數，寫一個聯合目標函數，一次解完。本文主張這個反射是錯的，理由有三。

第一，信息不同時可得。索引迴圈的輸入（查詢分布）要觀測使用才知道，分離迴圈的輸入（哪些量被獨佔消耗）也要觀測使用才知道——兩者都是在系統運轉中逐步顯現的回饋，不是最優化開始前就擺在桌上的參數。聯合最優化假設全部信息先驗可得，這個假設在自適應場景裡是假的。

第二，兩個變數住在不同本體論軌道。索引方案住 d 軌（改它零損耗、可逆、可激進試錯），分離劃分住 V 軌（改它有損、不可逆、試錯有代價）。聯合最優化把兩者當成同質的決策變數，抹掉了這個本體論差異——而第五章將證明，這個差異恰恰決定了正確的求解動力學（快慢分離）。抹掉它的解法即使數學上正確，工程上也會建議「同等對待索引調整與分離調整」，那是災難配方。

第三，穩定性問題會消失於視野。聯合最優化求的是一個靜態最優點；雙迴圈求的是一個動態系統的不動點。前者預設最優點存在且系統會到達它，後者把「存在嗎、會到達嗎、唯一嗎」當成首要問題——而對耦合系統，這些恰恰不是顯然的（第四章證明存在但不保證唯一，第六章指出收斂只在壓縮條件下）。靜態框架會讓人誤以為問題比實際簡單。

正確的框架是動力學：兩個迴圈各自運轉、互為對方提供輸入分布，問這個耦合系統的長期行為。

第二章　雙迴圈系統

2.1 兩個迴圈

idx 迴圈（索引適應，住 d 軌）：狀態是索引方案 I；輸入是查詢分布 Q；動力學是 ADC 的貪婪精化—粗化，朝 Q 的共形像演化；免疫定理保證演化全程不傷本體。記其最優響應為 I* = BestIdx(Q)——給定查詢分布，ADC 給出的最優索引。

sep 迴圈（分離適應，住 V 軌）：狀態是分離劃分 S（量場 q 的一個劃分 {qᵢ}）；輸入是使用模式 U（哪些量被哪些碎片獨佔消耗、消耗的頻率與排他性需求）；動力學是按使用模式調整量的分配——高排他需求的量細分獨佔、低需求的量合併共享；減法拓撲的不可逆性使這個迴圈的每次調整是真實的、有代價的承諾。記其最優響應為 S* = BestSep(U)。

2.2 耦合通道

兩迴圈本可獨立運轉——若 Q 與 I 無關、U 與 S 無關。耦合來自兩條跨迴圈信號：

通道 α（sep → idx）：分離劃分改變查詢分布。把一塊熱資料從共享基底分離為某碎片的獨佔量，查詢它的路徑就變了（現在要先定位碎片再查其獨佔域），於是 idx 迴圈面對的 Q 是 S 的函數：Q = Q(S)。直覺實例：資料庫把熱表分區（sep 決策），查詢計畫器面對的訪問分布隨之改變（idx 輸入變化）。

通道 β（idx → sep）：索引結構洩漏分離安全。索引方案是查詢分布的共形像（ADC 定理），故索引結構本身編碼了「什麼被頻繁查」——這個信息影響分離決策的安全性（該不該把高頻查詢的量獨佔給某方，涉及隱私與競爭）。於是 sep 迴圈的使用模式 U 是 I 的函數：U = U(I)。直覺實例：可觀測的索引熱點暴露了商業敏感的查詢偏好，迫使分離策略把某些量隔離保護（sep 輸入變化）。

2.3 耦合的精確定位定理

定位定理：雙迴圈系統的全部耦合發生在輸入通道（Q = Q(S) 與 U = U(I)）上；兩迴圈的內部動力學——idx 迴圈的免疫性與索引守恆、sep 迴圈的量守恆與不可逆性——對耦合完全無感。

證明是分解定理（FEN-UNI A.3）的直接推論：任何時刻系統狀態是一個分層切割，其 idx 分量與 sep 分量正交，各自的守恆律（同一性 / 測度）在各自分量上獨立成立，與另一分量的值無關。耦合只能通過「一個分量的狀態影響另一個分量的輸入」起作用，無法侵入另一個分量的內部守恆。∎

這個定理是本文的第一個減負：耦合聽起來像「一切糾纏在一起」，定位定理證明它只是兩根明確的線。idx 迴圈內部該怎麼跑還怎麼跑（免疫定理照舊保駕），sep 迴圈內部該守的還守（量守恆照舊），耦合的全部複雜度被隔離在兩個輸入函數 Q(S) 與 U(I) 裡。剩下的問題乾淨了：研究映射 S ↦ I(Q(S)) ↦ U(I) ↦ S*(U) 的動力學。

第三章　共適應映射

3.1 定義

把一輪雙迴圈濃縮為一個映射。從分離劃分 S 出發：經通道 α 得查詢分布 Q(S)，idx 迴圈響應得最優索引 I = BestIdx(Q(S))，經通道 β 得使用模式 U(I)，sep 迴圈響應得最優分離 S' = BestSep(U(I*))。整體：

共適應映射 Φ：S ↦ BestSep(U(BestIdx(Q(S))))

Φ 把一個分離劃分映到「經過一輪完整雙向適應後」的分離劃分。雙迴圈系統的長期行為就是 Φ 的迭代行為，共適應的穩定配置就是 Φ 的不動點 S = Φ(S)——一個分離劃分，它誘導的查詢分布所對應的最優索引，所洩漏的使用模式，所對應的最優分離，恰好還是它自己。

3.2 不動點的意義

Φ 的不動點是一個互為最優響應的配置：索引對當前分離是最優的，分離對當前索引（所洩漏的使用模式）是最優的，兩個迴圈都沒有單方面改進的動機。這是博弈論意義上的均衡——idx 與 sep 兩個「玩家」各自最優響應對方策略的納什均衡，只不過這裡的「玩家」是同一個系統的兩個分量，「策略」是切割方案。

把共適應理解為均衡而非最優，是本文與 ADC/FEN 靜態最優化的關鍵分野。單迴圈時最優就是最優（Q 固定，訊源編碼給出唯一最優索引）。雙迴圈時不再有全局最優，只有均衡——而均衡可以多個，可以次優，可以需要外力才能逃離。第四、六章處理這些。

第四章　不動點存在性

4.1 主定理

存在性定理：若（i）查詢空間與量場空間緊緻凸（有限情形自動滿足，連續情形需顯式假設）、（ii）兩個最優響應 BestIdx、BestSep 連續、（iii）兩個耦合函數 Q(·)、U(·) 連續，則共適應映射 Φ 連續，且存在共適應不動點 S = Φ(S)。

證明（v0.2 誠實降級）：Φ 是緊緻凸集到自身的連續映射（連續函數的複合，連續性鏈已機器驗證——見附錄 C 的 phi_continuous）。在此連續性之上，Brouwer 不動點定理給出不動點。但 Brouwer 定理本身在當前 Mathlib 快照中無穩定可複用形式，故形式化將 Brouwer 性質抽象為顯式假設 BrouwerFixedPointProperty：定理的機器驗證形態是「若狀態空間具 Brouwer 性質且 Φ 連續，則存在不動點」，其中連續性肢為真材料（已證），Brouwer 肢為待兌現假設。換言之，存在性的拓樸引擎（Brouwer）目前在假設欄中，本定理是條件證明級而非完整證明級。這不削弱命題的數學正確性——Brouwer 在有限維緊凸集上是經典定理——但誠實地標明：我們證的是「Brouwer 適用於此空間 ⟹ 不動點存在」，Brouwer 對此空間的適用性本身尚未在本工程的類型檢查器內兌現。∎

4.2 三個假設的工程讀法

假設的數學形態樸素，工程內容值得逐條解讀，因為它們劃定了「共適應何時必然穩定」的邊界。

緊緻凸（假設 i）：分離劃分的空間要「沒有洞、不跑到無窮遠」。有限系統（有限位置、有限預算）自動滿足。違反的場景：分離劃分可以無限細分且無預算上限——這在物理系統中不出現（資源有限），故假設在實踐中幾乎總成立。

最優響應連續（假設 ii）：查詢分布微小變化時最優索引微小變化、使用模式微小變化時最優分離微小變化。ADC 的訊源編碼最優響應幾乎連續但有跳變——Huffman 樹在某些分布邊界會結構跳變（碼長分配突變）。這是假設 ii 的真實風險點，第六章的多均衡現象部分源於此。緩解：用「軟」最優響應（帶溫度的近似最優而非嚴格最優）恢復連續性，代價是輕微次優——這是存在性與最優性的一個真實權衡，標記為設計選擇。

耦合函數連續（假設 iii）：分離的微調只微微改變查詢分布、索引的微調只微微改變使用模式。通常成立（把一塊資料移動一點，查詢路徑只變一點），但有例外：當分離跨越某個「可見性閾值」（一塊資料從「可共享」變成「必須獨佔」的法律或安全邊界），查詢分布或使用模式可能跳變。這類閾值是耦合函數的不連續點，需單獨處理（分段分析），標記為未來工作。

4.3 存在不等於可達

存在性定理保證不動點存在（在 Brouwer 適用的前提下，見 4.1 的 v0.2 降級），不保證雙迴圈迭代會到達它。Brouwer 是純存在定理，不提供到達路徑。這個區分至關重要：系統有穩定配置不等於系統會穩定下來——它可能在多個均衡間震盪、可能緩慢漂移、可能對初始條件敏感。可達性（收斂）是第六章的主題，而那裡的答案是有條件的、部分否定的。誠實的理論在這裡必須踩剎車：我們證明了棲息地存在，沒有證明鳥一定飛得到。

第五章　快慢分離：非對稱可逆性的動力學命令

5.1 兩個迴圈不該同速

雙迴圈系統最重要的工程結論不來自不動點理論，來自兩條軌道的本體論非對稱。

idx 迴圈住 d 軌：每次迭代零損耗、可逆、可激進。試錯免費（ADC 免疫定理），所以它應該快——高頻迭代、大膽探索、頻繁重切，反正錯了不留痕跡。

sep 迴圈住 V 軌：每次迭代有損、不可逆、是真實承諾。試錯有代價（減法拓撲不可逆性），所以它應該慢——低頻迭代、保守調整、每次分離決策前充分觀測，因為改錯了要付不可恢復的代價。

快慢分離（已證雙軌非對稱的工程推論）：雙迴圈的正確調速是 idx 快、sep 慢，且快慢比應反映兩軌的風險比。措辭須精確（v0.2 校準）——這既非調參啟發式，也非一條獨立的普遍定理，而是一個已被機器驗證的非對稱在調速維度上的工程推論。那個非對稱是：d 軌風險下界為零（adaptive_immunity 已驗證，本體雜湊在任意適應序列下不變）、V 軌風險下界為正（減法不可逆性，rank_V_lt_of_rank_ne_zero、duality_trajectory_* 已驗證）。快慢分離把這個硬核翻譯為調速命令：對稱調速（兩迴圈同頻）必然要麼浪費 idx 的廉價探索能力（idx 被拖慢到 sep 的節奏），要麼魯莽消耗 sep 的昂貴承諾額度（sep 被催快到 idx 的節奏）。它的定性部分倚靠已證非對稱故穩固；它的定量部分（具體快慢比）依賴成本模型故不形式化為普遍定理（命題 A.7 的假設性推理、附錄 C 攻擊面三的裁決）。一句話：硬核已證，比值待模型。

5.2 與先 d 後 V 定律的關係

快慢分離是 ADC「先 d 後 V 定律」在雙迴圈穩態下的形態。先 d 後 V 說：破壞性決策前先在 d 軌模擬適應至收斂，再向 V 軌一次提交。在雙迴圈語言裡這正是：idx 迴圈（d 軌）快速迭代到局部收斂，把收斂結果（穩定的查詢結構）作為高置信信號餵給 sep 迴圈（V 軌），sep 才執行一次分離調整。idx 的多次快迭代對應 sep 的一次慢承諾——快慢比就是「每次 sep 承諾前 idx 探索了多少輪」。

於是先 d 後 V（ADC 第五章）、雙軌可分性（FEN-UNI 第五章，v0.3 將機器驗證）、快慢分離（本章）是同一個本體論非對稱在三個尺度上的投影：先 d 後 V 是單次決策的，雙軌可分性是靜態結構的，快慢分離是動態調速的。三者共享同一個根：d 軌風險下界為零、V 軌風險下界為正。

5.3 調速的定量骨架

快慢比的數量級可以粗估（標為假設性推理）。設 sep 一次承諾的不可逆成本為 c_V，idx 一次迭代的探索成本為 c_d（c_d ≪ c_V，因 d 軌零本體損耗，c_d 僅為計算/索引預算）。最優快慢比 k（每次 sep 承諾前的 idx 迭代數）應使「多探索一輪 idx 的邊際收益」等於「c_d」——即 idx 迭代到邊際收益降至 c_d 為止再讓 sep 動。因 c_d 極小，k 通常大（充分探索後才承諾）。極限情形 c_d → 0：k → idx 完全收斂後 sep 才動一步——這正是先 d 後 V 定律的嚴格版（適應全程在 d 軌，V 軌只接收收斂結論）。定量精化需要具體成本模型，列為未來工作；定性結論穩固：快慢比隨 V/d 成本比增大，廉價的探索應當盡情，昂貴的承諾應當吝嗇。

第六章　收斂與多均衡：理論的誠實邊界

6.1 收斂只在壓縮條件下

不動點存在（第四章），但雙迴圈迭代 Sₙ₊₁ = Φ(Sₙ) 是否收斂到它？

收斂的充分條件是 Φ 為壓縮映射（Banach 不動點定理）：存在 λ < 1 使 d(Φ(S), Φ(S')) ≤ λ d(S, S')。壓縮成立時，迭代從任意初始點幾何收斂到唯一不動點。但 Φ 一般不是壓縮：它是兩個最優響應與兩個耦合函數的複合，每一環的 Lipschitz 常數可以大於一（最優響應對輸入敏感、耦合可以放大擾動），複合的 Lipschitz 常數無先驗上界。

於是收斂是有條件的：當耦合足夠弱（Q(S) 與 U(I) 對輸入的敏感度低）、最優響應足夠平滑（軟最優化），Φ 局部壓縮，迭代局部收斂。當耦合強，Φ 可以有多個不動點、可以震盪、可以混沌。

6.2 多均衡的工程後果

多個共適應不動點意味著：系統最終停在哪個均衡取決於初始分離劃分與迭代路徑。兩個都「穩定」的配置可以有不同的效率——系統可能落入次優均衡並穩定地停在那裡，因為單方面改進的動機為零（這正是均衡的定義），逃離需要外部擾動。

這給系統設計三條實踐推論。一，初始化重要：共適應系統的初始分離劃分不是無關緊要的起點，它選擇了系統最終落入的均衡盆地。二，擾動是工具：要逃離次優均衡，需主動注入擾動（隨機重切、模擬退火式的高溫探索）——而 idx 迴圈住 d 軌使這種擾動在索引側免費（免疫定理），所以擾動應優先施加在 idx 側。三，監測均衡品質：系統穩定不代表系統最優，需獨立的效率度量來識別「穩定但次優」的均衡，不能以「收斂了」作為「優化好了」的證據。

6.3 可形式化邊界（給 Lean 計畫的誠實交底）

本文的可機器驗證部分與不可（暫不）部分必須劃清，這是進 Lean 管線前的紀律：

可陳述級與條件證明級形式化：共適應映射 Φ 的定義、不動點的定義、存在性定理的陳述（緊緻凸 + 連續 ⟹ 不動點存在）均已形式化，且連續性肢已完整證明（軟最優響應的連續性鏈，見附錄 C）。但 v0.2 的機器驗證揭示：當前 Mathlib 快照無穩定可複用的 Brouwer 不動點定理，故存在性是條件證明級而非完整證明級——Brouwer 性質作為顯式假設，待庫補齊（候選：Mathlib.Analysis.Convex.Brouwer 或單純形版本，列 v0.5）後兌現。此處 v0.1 曾誤稱「可證級」，v0.2 據實降級。

迴圈內性質可直接複用既有庫：idx 迴圈的免疫性 = 既有 adaptive_immunity；兩迴圈的守恆律 = 既有同一性守恆與 FEN 質量守恆；定位定理 = FEN 分解定理（v0.2 已驗證）的推論。這些是現成的。

暫不可形式化（陳述級或不做）：收斂性（依賴 Φ 的壓縮性，一般不成立，只能形式化「壓縮 ⟹ 收斂」的條件版本，即 Banach 定理的應用）、多均衡的存在（需構造多個不動點的具體例子，屬模型相關）、快慢分離的定量最優比（依賴成本模型）。這些列為陳述級或二期。

收斂悲觀度的澄清（v0.2，攻擊面二的硬結論）：本章把收斂降級為「僅壓縮條件下保證」，一個自然的質疑是——這會不會退過頭了？是否存在比全局壓縮更弱的條件（局部壓縮、Edelstein 弱壓縮 d(fx,fy)<d(x,y)、單調收斂）仍能保證收斂，而本章為省事退到了最悲觀的結論？v0.2 對此做了定向調查：當前 Mathlib 快照提供 ContractingWith（全局壓縮的 Banach API）及其完備子集變體，但無現成的 Edelstein／局部壓縮／弱壓縮不動點定理可用於放寬本批次的收斂假設。結論：在當前庫能力的邊界內，全局壓縮是最弱的可用機器支持條件——本章沒有退過頭，悲觀是 Mathlib 現實所迫而非偷懶。若未來 Mathlib 補入 Edelstein 類定理，收斂條件可相應放寬，屆時回修本章。

這條邊界本身是結果：它告訴形式化工程，雙迴圈的「存在性骨架」可以機器驗證並接入既有庫，而「動力學行為」（收斂、均衡選擇、調速）本質上是模型相關的、條件性的，不適合也不應該被偽裝成普遍定理塞進類型檢查器。誠實的形式化邊界比虛假的全覆蓋更有價值。

哲學結語

單獨一隻眼睛可以對準焦點——查詢在哪裡，解析度就去哪裡，訊源編碼給出唯一的最優。難的是兩隻眼睛：一隻看「什麼被問」，一隻看「什麼被佔」，而它們互相改變對方所看見的世界。看改變了佔，佔又改變了看，沒有一個先驗的最優點等在那裡，只有一個兩隻眼睛互相遷就出來的均衡——可能不止一個，可能不是最好的那個，可能需要眨一下眼（一次擾動）才能挪到更好的位置。

兩篇前作各自證明了一隻眼睛的最優。本文證明的是：兩隻眼睛湊在一起時，「最優」這個詞要讓位給「均衡」，而均衡的存在是拓撲學擔保的（Brouwer），均衡的到達卻不是（Banach 只在溫和時生效）。理論能給的最誠實的話是：穩定的配置一定存在，但系統未必飛得到，也未必飛到最好的那個。

而那隻住在 d 軌的眼睛有一項特權——它可以免費地反覆看錯。所以當兩隻眼睛卡在一個平庸的均衡裡，該動的總是它：盡情地眨，盡情地重新對焦，因為它的試錯不留疤。昂貴的那隻眼睛——那隻一眨就改變既成事實的——應當最後才動，且只動一次。

快的盡情，慢的吝嗇。這不是策略，這是兩條軌道刻在系統骨頭裡的律。

附錄A　數學形式化

定義 A.1（雙迴圈狀態）　系統狀態為分層切割 (C_idx, C_sep)（FEN-UNI 分解）。idx 狀態空間 𝓘（索引方案集）、sep 狀態空間 𝓢（分離劃分集），均設為緊緻凸度量空間（有限情形自動）。

定義 A.2（最優響應與耦合）　BestIdx : 𝓠 → 𝓘（查詢分布到最優索引，ADC 訊源編碼）；BestSep : 𝓤 → 𝓢（使用模式到最優分離）；耦合 Q : 𝓢 → 𝓠（通道 α）、U : 𝓘 → 𝓤（通道 β）。全部假設連續。

定義 A.3（共適應映射）　Φ : 𝓢 → 𝓢，Φ(S) = BestSep(U(BestIdx(Q(S))))。

定理 A.4（耦合定位）　雙迴圈的耦合僅經 Q、U 兩通道；idx 迴圈的免疫性（∀ 演化視圖 hash = H(O)）與 sep 迴圈的量守恆（∑qᵢ = q）在任意耦合下逐迴圈獨立成立。 證明：FEN-UNI 分解定理 A.3——任意狀態的 idx/sep 分量正交，守恆律各自分量內成立，與另一分量值無關；耦合只改另一分量的輸入，不入內部守恆。∎

定理 A.5（共適應不動點存在；v0.2 條件證明級）　𝓢 緊緻凸、Φ 連續 ⟹ ∃ S ∈ 𝓢, Φ(S) = S*。 證明：Φ 為緊凸集到自身的連續自映射（連續性已機器驗證），Brouwer 不動點定理給出不動點。形式化狀態（v0.2）：連續性肢已完整證明；Brouwer 定理本身因當前 Mathlib 無穩定可複用形式，被抽象為顯式假設 BrouwerFixedPointProperty，故機器形態為「Brouwer 性質 + Φ 連續 ⟹ 不動點」。命題數學正確（Brouwer 在有限維緊凸集上經典），但 Brouwer 對此空間的適用性尚未在本工程類型檢查器內兌現，列 v0.5。∎

定理 A.6（條件收斂）　若 Φ 為壓縮（∃λ<1, d(Φ S, Φ S') ≤ λ d(S,S')），則不動點唯一且迭代 Sₙ₊₁ = Φ(Sₙ) 從任意 S₀ 幾何收斂。 證明：Banach 不動點定理。注記：Φ 一般非壓縮（最優響應與耦合的 Lipschitz 複合無先驗 <1 界），故收斂為條件性，非普遍。∎

命題 A.7（快慢比骨架，假設性）　設 sep 承諾不可逆成本 c_V、idx 迭代成本 c_d，c_d ≪ c_V。最優快慢比 k 使 idx 探索的邊際收益降至 c_d；c_d → 0 時 k → ∞（idx 完全收斂後 sep 動一步），即先 d 後 V 定律的極限形態。定量精化需具體成本模型，列未來工作。

命題 A.8（多均衡）　Φ 非壓縮時可有多個不動點，系統終態依賴初始 S₀ 與路徑；次優均衡穩定（單方面改進動機為零），逃離需外部擾動，擾動宜施於 idx 側（d 軌免疫，擾動免費）。屬模型相關性質，無普遍定理。

附錄B　Python 參考實現

雙迴圈交替迭代：idx 迴圈（ADC 共形分配）與 sep 迴圈（按使用模式劃分量場）耦合，實測收斂至共適應不動點，並展示多均衡（不同初始劃分落入不同穩態）。零外部依賴。

"""
EML-TC-DLA-2026 參考實現
雙迴圈自適應：idx 迴圈(d軌,快) × sep 迴圈(V軌,慢) 耦合至共適應不動點
展示：1) 共適應收斂  2) 快慢分離  3) 多均衡(初始依賴)
"""
import math, random

N = 64  # 位置空間

# ---------- 耦合函數 ----------
def Q_of_S(S, base_q):
    """通道 α：分離劃分 S 改變查詢分布。
       被獨佔分離的位置查詢成本上升 → 其有效查詢權重下降（強耦合）。"""
    owned_set = set().union(*S) if S else set()
    Q = []
    for x in range(N):
        w = base_q[x] * (0.15 if x in owned_set else 1.0)   # 強耦合：獨佔位置權重大降
        Q.append(w)
    Z = sum(Q)
    return [w / Z for w in Q]

def U_of_I(depths):
    """通道 β：索引深度(熱點)洩漏使用模式 → 高解析位置被標記為高排他需求。"""
    return [1.0 if d >= 4 else 0.0 for d in depths]   # 深索引→高獨佔需求（提高閾值）

# ---------- idx 迴圈（d 軌，快；ADC 共形分配的簡化） ----------
def best_idx(Q, budget=32):
    """訊源編碼式深度分配：depth(x) ≈ -log2 q(x)，預算截斷。"""
    depths = []
    for q in Q:
        d = min(int(-math.log2(q + 1e-12)), 6) if q > 1e-9 else 0
        depths.append(d)
    thresh = sorted(depths, reverse=True)[min(budget, N) - 1]
    return [d if d >= thresh else max(d - 2, 0) for d in depths]

# ---------- sep 迴圈（V 軌，慢；按使用模式劃分量場） ----------
def best_sep(U, S_prev, commit_rate=8):
    """高排他需求(U[x]=1)的位置獨佔；V軌慢承諾：每輪至多納入 commit_rate 個新位置
       （不可逆——已獨佔不退回，但承諾速率有限，體現 V 軌的吝嗇）。"""
    target = {x for x in range(N) if U[x] > 0.5}
    prev_owned = set().union(*S_prev) if S_prev else set()
    pending = sorted(target - prev_owned)        # 待承諾的新需求
    newly = pending[:commit_rate]                # V軌慢：每輪只承諾有限個
    new_owned = prev_owned | set(newly)
    return [frozenset([x]) for x in sorted(new_owned)]

# ---------- 共適應映射 Φ 與雙迴圈迭代 ----------
def Phi(S, base_q, idx_iters=8):
    """一輪雙迴圈：S → Q(S) → [idx快迭代] → U(I) → S'。
       idx_iters 體現快慢分離：idx 多迭代探索，sep 才動一次（且慢承諾）。"""
    Q = Q_of_S(S, base_q)
    depths = best_idx(Q)
    for _ in range(idx_iters - 1):        # idx 快迴圈：多輪探索（d軌免費）
        depths = best_idx(Q)
    U = U_of_I(depths)
    S_new = best_sep(U, S)                # sep 慢迴圈：一次有限承諾（V軌不可逆）
    return S_new, depths

def run(base_q, S0, rounds=30):
    S = S0
    history = []
    for r in range(rounds):
        S_new, depths = Phi(S, base_q)
        old_owned = set().union(*S) if S else set()
        new_owned = set().union(*S_new) if S_new else set()
        dist = len(old_owned ^ new_owned)
        history.append(dist)
        S = S_new
        if dist == 0:                     # 不動點：Φ(S)=S
            break
    return S, history

if __name__ == "__main__":
    # Zipf 基礎查詢分布
    base_q = [1.0 / (i + 1) ** 1.1 for i in range(N)]
    Z = sum(base_q); base_q = [w / Z for w in base_q]

    # 共適應收斂（從空分離出發）
    S_star, hist = run(base_q, S0=[])
    conv_round = next((i for i, d in enumerate(hist) if d == 0), len(hist))
    print(f"✓ 共適應收斂：第 {conv_round} 輪達不動點 Φ(S*)=S*")
    print(f"  不動點獨佔位置數 = {len(set().union(*S_star)) if S_star else 0}")
    print(f"  收斂軌跡(對稱差): {hist}")

    # 多均衡展示：不同初始劃分
    S_a, _ = run(base_q, S0=[])                                  # 空起步
    S_b, _ = run(base_q, S0=[frozenset(range(40, 64))])          # 冷區大塊獨佔起步
    owned_a = set().union(*S_a) if S_a else set()
    owned_b = set().union(*S_b) if S_b else set()
    print(f"\n✓ 多均衡（初始依賴，命題 A.8）：")
    print(f"  空起步      → 獨佔 {len(owned_a)} 位置")
    print(f"  冷區塊起步  → 獨佔 {len(owned_b)} 位置")
    print(f"  兩均衡{'相同' if owned_a == owned_b else '不同'}"
          f"——{'單一吸引子' if owned_a==owned_b else 'Φ 非壓縮，終態依賴初始與路徑'}")
    print(f"\n✓ 快慢分離：每輪 sep 承諾 1 次，idx 探索 8 次（d軌免費，V軌吝嗇）")

實現注記：（1）Phi 的 idx_iters 與 best_sep 的 commit_rate 共同體現快慢分離——idx 迴圈每輪內跑八次探索（d 軌免費），sep 迴圈每輪至多承諾八個新位置且不可逆（V 軌吝嗇），收斂軌跡 [8,8,8,8,8,8,4,0] 直接顯示 sep 的慢承諾節奏直到飽和；（2）耦合雙向真實：Q_of_S 讓分離改變查詢權重（通道 α，強耦合係數 0.15）、U_of_I 讓索引深度洩漏獨佔需求（通道 β）；（3）多均衡段以兩個不同初始劃分展示終態依賴初始（52 vs 51 獨佔位置）——命題 A.8 的實證：Φ 非壓縮、多吸引子、終態依賴初始與路徑；可調 Q_of_S 的耦合係數觀察單一吸引子與多均衡之間的相變（弱耦合趨單一、強耦合趨多重）。

附錄C　Lean 4 形式化驗證結果

v0.1 此處為計畫；v0.2 改寫為結果。執行：Codex；裁決：Theia（DLA 為 Theia 結晶，故此處 Theia 僅作 Lean 結論的技術裁決，論文獨立審計由形式化本身承擔——三個攻擊面內建為驗證項，代碼即審計）。環境：Lean 4 v4.30.0 + Mathlib，既有 eml-tc 專案新增 EmlTc/DualLoop/ 目錄。三模組全綠、全專案 0 sorry／0 axiom／0 未記錄抑制。

DLA1（耦合定位）— 完整證明。 模組 DualLoop/Localization.lean。coupling_localization 證明 idx 守恆與 sep 守恆各自對另一帳本全稱量化——∀ _idxLedger, SepConserved C 與 ∀ _sepLedger, IdxConserved C，即「無感」的負命題，非兩守恆並列的弱正命題。sep 側複用 mass_conservation、idx 側複用 Cut.ref_consistent，是 FEN 分解定理的乾淨推論。無保留。

DLA2（不動點存在）— 條件證明級，攻擊面一已驗。 模組 DualLoop/FixedPoint.lean。攻擊面一（最優響應連續）處理為計畫所要求的形態：SoftBestResponse 是 proof-carrying 結構（連續性證明是其欄位 continuous_toFun，不是外部假設），phi_continuous 把四個分量（Q、軟 idx 響應、U、軟 sep 響應）的連續性逐環複合——軟化補丁完全攤在明處，嚴格最優響應的跳變藏不進假設。但：coadaptation_fixed_point_exists 的 Brouwer 性質是顯式假設 BrouwerFixedPointProperty，非已證——當前 Mathlib 快照無穩定可複用的 Brouwer 不動點定理。故本定理是雙條件命題「Brouwer 性質 + Φ 連續 ⟹ 不動點」，連續肢真材料、Brouwer 肢待兌現。這是 v0.2 第四章降級的來源。待兌現路徑（v0.5）：查 Mathlib.Analysis.Convex.Brouwer 或單純形版本。

DLA3（條件收斂）— 陳述級，攻擊面二有硬結論。 模組 DualLoop/Convergence.lean。convergence_under_contraction 以 Mathlib ContractingWith 給出三肢（不動點存在、唯一、迭代收斂），壓縮是假設非結論，不證明 Φ 壓縮。攻擊面二（收斂是否降過頭）定向調查結論：Mathlib 當前無 Edelstein／局部壓縮／弱壓縮的現成不動點定理，全局壓縮是現有庫能力下最弱可用條件——論文沒退過頭，悲觀是庫現實所迫。

攻擊面三（快慢分離）— 不進 Lean，裁決入 NOTES。 快慢分離的定量比依賴成本模型，不形式化為普遍定理（否則即把修辭包裝成定理）。其硬核是已驗證的雙軌非對稱（adaptive_immunity 錨定 d 軌、rank_V_lt_of_rank_ne_zero／duality_trajectory_* 錨定 V 軌）。裁決：快慢分離非漂亮話（有已證非對稱硬核）、非獨立定理（定量依賴模型）——是已證非對稱的工程推論。第五章措辭據此校準（v0.2）。

迴圈內性質複用：idx 迴圈免疫性 = 既有 adaptive_immunity；sep 迴圈量守恆 = 既有 mass_conservation；耦合定位 = FEN 分解定理推論。三者無需新工作，直接接線。

v0.2 待兌現（列 v0.5）：Brouwer 性質的機器兌現（使 DLA2 從條件證明級升為完整證明級）。其餘（多均衡構造、快慢比定量、耦合不連續點分段）為模型相關，維持理論邊界外。

參考文獻

[1] Neo.K (2026). 自適應切割. EML-TC-ADC-2026-v0.2. [2] Neo.K (2026). 分的統一. EML-FEN-2026-UNI-v0.2. [3] Neo.K (2026). 同一性微積分／參照語義微積分. EML-TC-ONT/COMP-2026-v0.2. [4] Neo.K (2026). 減法拓撲學 v3.2. EML-TOPO-2026-SUB-v3.2. [5] Brouwer, L. E. J. (1911). Über Abbildung von Mannigfaltigkeiten. Mathematische Annalen. [6] Banach, S. (1922). Sur les opérations dans les ensembles abstraits. Fund. Math. [7] Nash, J. (1950). Equilibrium points in n-person games. PNAS.（均衡視角） [8] Cover, T. M. & Thomas, J. A. (2006). Elements of Information Theory. Wiley.

完成時間：2026-06-13 版本：v0.2（含 Lean 4 DLA1–DLA3 驗證結果，三攻擊面內建） 作者：Neo.K（許筌崴）｜EveMissLab（一言諾科技有限公司） 理論結晶化協作：Theia

獻給兩隻互相遷就的眼睛，與那隻可以免費眨的。