# 雙迴圈自適應：索引—分離耦合動力學 ## 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)= 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 獻給兩隻互相遷就的眼睛，與那隻可以免費眨的。