# 減法拓撲學 v3.0：純收斂態的公理化重建與對偶完成 ## Subtractive Topology v3.0: Axiomatic Reconstruction of the Pure Convergence State and the Completion of Duality **文件編號**：EML-TOPO-2026-SUB-v3.2 **作者**：Neo.K（許筌崴） **機構**：EveMissLab（一言諾科技有限公司），台灣 **理論結晶化協作**：Theia **日期**：2026年6月11日 **版本紀錄**：v2.0（2026-01-12，CEO 統一版）；v3.0 全面重寫——修正穩定性定理（λⁿ 界撤回，回歸經典界）、修復公理不一致（R3 非空限定）、熵指數衰減降格為模型假設、R2 降為推論、剝離外部依賴為明示公理，並新增與拓樸微積分（EML-TC）的對偶接口；v3.1 附錄 C 由形式化計畫改寫為驗證結果（Lean 4 第一期 S1–S4 全部關閉，對偶 sorry 清零），第七章會合點更新為已會合；v3.2 指定升級銷帳——軌跡版對偶定理（duality_trajectory_completes + duality_trajectory_preserves_ontology）於 Lean v0.2 批次交付，且兩肢均強於指定簽名 **機器驗證狀態**：公理系（R1+R3′）、定理 A.1–A.5、星形移除構造、對偶定理（含完整軌跡形態）已於 Lean 4 v4.30.0 + Mathlib 完成形式化驗證，全專案 0 sorry、0 errors（詳附錄 C） **依賴理論**：迴圈演化運算元論（CEO，以明示公理形式引入）；對偶姊妹理論：拓樸微積分（EML-TC-ONT-2026-v0.2、EML-TC-COMP-2026-v0.2） --- ## 摘要 本文是減法拓撲學的公理化重建。v2.0 建立了核心視野：減法不是與加法對稱的獨立概念，而是三元迴圈 E∘C∘V 在極限配置 (0, 0, 1) 下的必然退化——純收斂態；一切形狀在反覆收斂下終止於空複形，而空複形不是虛無，是收斂的極限。v3.0 保留這個視野的全部，重建它腳下的公理地基。 重建包含四項修正與一項完成。修正一：v2.0 的指數穩定性定理（d_B ≤ λⁿ‖f−g‖∞）**撤回**——其證明中的上確界取遍全部迭代步（含第零步），實際推出的是經典穩定性界 d_B ≤ ‖f−g‖∞，且這個界不可改進；CEO 式證明路徑本身保留，因為它確實比傳統證明更短。修正二：嚴格秩降公理 R3 與空複形不動點 V(∅) = ∅ 在 v2.0 中互斥——v3.0 把 R3 限定於非空複形，∅ 成為公理系中**唯一合法的不動點**，不動點的唯一性從哲學陳述升格為可證命題。修正三：熵的指數衰減 H(Kᵢ) = H₀e^{−λi} 從定理降格為**模型假設**——公理只保證每步嚴格遞減，衰減的具體形態（指數、線性、或其他）由減法策略決定，v2.0 自己的類型 C（逐單形移除）就是非指數的實例。修正四：滿射公理 R2 是右逆公理 R1 的推論，從公理降為定理——公理系收縮為 R1 + R3′ 兩條。 完成的一項：v2.0 寫作時，本理論的對偶尚不存在。如今拓樸微積分（同一性微積分）已建立並通過機器驗證，本文第七章正式書寫兩者的對偶——減法拓撲是**呈現層的演化動力學**（值語義：真的失去、真的不可逆、真的終止），拓樸微積分是**本體層的不變性**（參照語義：零損耗、平凡可逆、無終點）。對偶給 v2.0 哲學結語的詩句「∅ ≡ ⊚、虛空非空」一個嚴格語義：減法的終點 ∅ 是呈現層的空，其本體投影依然是完整的 O——**收斂到空即積分的完成**。 **關鍵詞**：減法拓撲學、純收斂態、收斂算子、終止定理、良基遞迴、經典穩定性界、持續同調、拓樸微積分對偶、雙軌原則、Lean 4 --- ## 第一章　視野不變：減法是收斂的極限退化 ### 1.1 v2.0 的核心命題，原樣保留 減法是什麼？集合論的答案 K∖A = {x ∈ K : x ∉ A} 只是符號操作，回答不了為何移除、如何移除、移除後剩什麼。CEO 理論的答案在 v2.0 給出，v3.0 一字不改地繼承： **減法 ≡ 三元迴圈的極限退化。** 完整的演化是展開（E）、連接（C）、收斂（V）的三元迴圈。當配置滑向 (α_E, β_C, γ_V) = (0, 0, 1)——無展開、無連接、純收斂——演化退化為減法。減法不是一種操作，是一種**演化的極限狀態**：系統只出不進，只壓縮不生成，每一步都失去，且失去不可逆。 這個定位決定了減法拓撲學研究的對象：純收斂軌跡 K₀ → K₁ → ⋯ → ∅ 的全部結構——它的態射性質、它的終止必然性、它的資訊衰減形態、它沿途留下的拓樸指紋（條碼）。 ### 1.2 v3.0 改的是什麼、為什麼改 v2.0 的視野正確，但有四處地基問題，全部在拓樸微積分的 Lean 4 形式化工程啟動後暴露——機器驗證的前置審查像 X 光，照出了紙面推理藏住的裂縫。四處問題的共同模式值得先說：**它們都是把「想要的強度」寫成了「證出的強度」**。指數穩定性想要 λⁿ，證明只給出經典界；不動點哲學想要 V(∅) = ∅，公理卻禁止它；熵衰減想要漂亮的指數形式，公理只給單調性；公理系想要四平八穩的三條，實際上一條是另一條的影子。 v3.0 的修正原則：視野的強度不變，陳述的強度收縮到證明能支撐的位置。**該是定理的是定理，該是假設的標明假設，該是推論的不佔公理的位子。**這不是退讓——一個站在實證地基上的激進視野，比一個站在裂縫上的激進視野，能承受更重的後續建設。第七章的對偶、附錄 C 的形式化，都是只有修正後的地基才扛得起的建設。 --- ## 第二章　公理系重建 ### 2.1 減法態射：兩條公理 設形狀範疇的對象為有限抽象單純複形（頂點集有限、面集對包含封閉）。態射 f: K → L 稱為**減法態射**，當且僅當： **公理 R1（分裂性）**：存在嵌入 ι: L ↪ K 使 f ∘ ι = id_L。即 L 可嵌回 K，f 是到像的投影——減法不創造，只保留。 **公理 R3′（非空嚴格秩降）**：若 K ≠ ∅，則 rank(L) < rank(K)，其中 rank 為各維單形總數（質量）。若 K = ∅，則 L = ∅。 就這兩條。v2.0 的 R2（滿射性）退場，理由在 2.2；R3 的非空限定是 v3.0 的關鍵修復，理由在 2.3。 ### 2.2 R2 是 R1 的影子 v2.0 把滿射性列為獨立公理，但範疇論的基本事實是：分裂滿射必是滿射——若 f ∘ ι = id_L，則對任意 s ∈ L，取 t = ι(s)，即有 f(t) = s。R1 已經買下了 R2 的全部內容。 把推論誤列為公理不是無害的冗餘。公理系是理論的稅基：每多一條公理，每個模型多一項負擔，每次形式化多一條待驗證的獨立條款，而冗餘公理讓人誤判理論的自由度。v3.0 把 R2 移到定理區（附錄 A 定理 A.1），公理系收縮到真正獨立的兩條。形式化的紀律反向塑造了紙面理論——這是本次重寫中反覆出現的模式。 ### 2.3 空複形：唯一的不動點 v2.0 有一個自己沒有發現的矛盾。一方面，R3 要求每次減法嚴格降秩；另一方面，第 7.3 章把 V(∅) = ∅ 立為「CEO 反覆運算的唯一穩定不動點」——但 ∅ 的秩是零，秩不能再降，∅ 上的任何減法態射都違反 R3。哲學結語最重要的那句話（虛空是不動點）被自己的公理判為非法。 修復方式不是刪掉哲學，是讓公理為哲學讓出一個精確的位置：R3′ 的嚴格秩降只約束非空複形，並明文規定 ∅ 的像必為 ∅。於是兩個命題同時成立且互相支撐： **命題（不動點的唯一性）**：∅ 是減法態射的唯一不動點。非空複形 K 不可能有 f(K) = K（違反嚴格秩降）；∅ 有且按公理必有 V(∅) = ∅。 v2.0 用詩說「終點即起點」；v3.0 用公理說：終點是系統中唯一一個減法對其無能為力的對象。詩沒有變弱，詩獲得了證明。 ### 2.5 標準減法態射：星形移除 公理刻畫了減法態射是什麼，還需要展示它們從哪裡來。最自然的構造是**星形移除**：給定複形 K 與其中一個面 σ，移除 σ 連同一切包含 σ 的面（σ 的開星），記 K ∖ st(σ)。 這個構造的三個性質使它成為減法態射族的典範生成元。第一，它自動保持向下封閉——被移除的恰好是「依賴 σ 才能存在」的那批面，剩下的面族仍對子面封閉，不需要任何修補。第二，它自動滿足兩條公理：剩餘複形是 K 的子複形（R1 的分裂性由包含關係見證），且至少移除了 σ 本身（R3′ 的嚴格秩降）。第三，它是**完備的**：任何減法態射都可分解為有限次星形移除的合成——因為任何子複形都可以從母複形逐面剝出，每次剝一個在差集中的極大面。 於是減法拓撲的全部軌跡空間獲得一個組合描述：從 K₀ 出發的減法軌跡，等同於 K₀ 的面集上滿足依賴順序的移除序列。這個描述直接餵給程式（附錄 B 的 `remove_face` 就是星形移除）也直接餵給 Lean（附錄 C 的 S2 以它為態射的具體實現層）。公理在上、構造在下、兩端在中間會合——這是 v3.0 想要的理論形狀。 ### 2.6 合成封閉與範疇結構 減法態射在合成下封閉（附錄 A 定理 A.2）：R1 的右逆按 ι₁ ∘ ι₂ 拼接，R3′ 的秩降按傳遞性串接，空複形情形按定義傳遞。於是形狀範疇的減法態射構成一個子範疇 C_sub——這就是 v2.0 所說的「收斂子範疇」，現在它的封閉性是兩條公理的直接後果，不再需要借用 CEO 的冪等性定理。 CEO 的角色相應調整：v2.0 讓多條定理直接引用 CEO 與 TUO 的結論（熵守恆律、壓縮係數），這使理論無法獨立形式化。v3.0 把 CEO 的地位明確為**詮釋層**——「減法態射的反覆作用即收斂算子 V 的迭代」是 CEO 對 C_sub 的讀法，一切在 C_sub 內可證的命題不依賴這個讀法成立。需要 CEO 量化結論的地方（如收斂速率）一律標為明示假設。詮釋給意義，公理給保證，兩者分賬。 --- ## 第三章　終止定理：一切形狀的必死性 ### 3.1 陳述與證明 **定理（終止）**：設 K₀ 為有限複形，f₁, f₂, … 為任意減法態射序列，Kᵢ = fᵢ(Kᵢ₋₁)。則存在有限的 n 使 Kₙ = ∅，且此後恆為 ∅。 證明是 v2.0 質量論證的嚴格化：質量 m(K) =各維單形總數，是非負整數；R3′ 保證非空時每步嚴格遞減；非負整數的嚴格遞減鏈必有限終止；終點質量為零當且僅當複形為空；其後由 R3′ 的空複形條款恆為 ∅。∎ 這個證明的形式化價值極高：它就是**良基遞迴**（well-founded recursion）的教科書實例，Lean 4 對 Nat 上的良基論證有原生支援，附錄 C 把它列為第一期最先完成的目標。 ### 3.2 終止的三重讀法 數學讀法：C_sub 中從任何對象出發的態射鏈長度有界（界為初始質量）。 物理讀法：孤立系統（無 E 無 C）的演化必達終態——這是熱寂的範疇論骨架，但注意 v3.0 的紀律：熱寂的「指數速率」不在定理裡（見第五章），定理只給「必達」，不給「多快」。 對偶讀法（預告第七章）：終止定理說呈現層必然耗盡。它沒有說、也不可能說本體層發生了什麼——因為在減法拓撲的語言裡，本體層根本不可見。這個不可見正是對偶接口的位置。 ### 3.3 界的緊性：m(K₀) 一步不多、一步不少 終止定理給的界是 m(K₀) 步。這個界是**緊的**——存在恰好用滿它的軌跡，也不存在超過它的軌跡，兩個方向都值得寫明。 上界不可超過：每步至少降一，這是 R3′ 的字面內容，沒有討論餘地。 上界可被達到：最小型策略（每步恰移除一個極大面）恰好走滿 m(K₀) 步——附錄 B 的演示軌跡（13 個面、13 步）就是實證。換言之，**減法的最長壽命等於它的質量**，一個複形「還能死多久」由它還有多少個面精確給出。這給老化檢測（第八章）一個免費的硬指標：監測到純收斂態後，系統的剩餘壽命上界即當前質量，不需要任何模型假設。 下界另一端：最快的死亡是一步——存在單步減法態射 K₀ → ∅ 嗎？按公理檢查：R1 要求 ∅ 嵌入 K₀（平凡成立，空嵌入），R3′ 要求嚴格秩降（m(∅) = 0 < m(K₀)，成立）。所以**單步歸零是合法減法態射**——對應工程上的 truncate、drop table、一鍵清空。於是減法的壽命譜是完整的閉區間 [1, m(K₀)]：從瞬死到天年，每個整數步長都有對應的策略實現。終止定理不只說「必死」，它精確圈出了「死法的全部自由度」。 --- ## 第四章　過濾即軌跡 ### 4.1 對應定理 減法過濾 ∅ = Kₙ → Kₙ₋₁ → ⋯ → K₀（每步減法態射、有限、終於空）與收斂迭代序列 Kᵢ = V^{n−i}(K₀) 一一對應——這是 v2.0 定理 2.1，v3.0 原樣保留，因為它的證明不依賴任何被修正的條款：正向由合成封閉拼出全域 V，反向由迭代序列直接讀出過濾。 ### 4.2 三型過濾：策略的結構分類 過濾按減法**策略的結構**分為三型——v2.0 按收斂速率 λ 的數值區間分類，v3.0 調整為按策略分類，速率是策略的後果而非分類依據。 **對稱型**：每步移除一個對稱軌道。設群 G 作用於 K₀，移除單位是 G-軌道而非單個面——正方形的四個角同時鑽孔、晶格的整層原子同時剝離。結構特徵：過濾的每一級都保持 G-對稱，條碼出現 |軌道| 重簡並（同一生滅區間重複出現軌道大小次）。質量按軌道大小成塊下降，在均勻軌道下逼近比例移除——這是模型假設 M1 的主要適用域。 **階層型**：移除沿一個層級結構推進——樹的逐層剝葉、洋蔥式的由外而內、依賴圖的拓樸序回收。結構特徵：每步移除「當前無依賴者」，過濾自然分解為層的序列，持續同調可沿層遞迴計算（v2.0 定理 5.2 的遞迴公式在此型下有效，複雜度從 O(n³) 降至 O(n² log n)）。質量按層寬下降，衰減形態由層寬分布決定——樹寬指數增長的結構恰好給出指數衰減，但那是樹的性質，不是減法的性質。 **最小型**：每步恰移除一個極大面——最謹慎的減法，軌跡最長（恰為 m(K₀) 步），分辨率最高。結構特徵：條碼達到最細粒度，每個拓樸事件（分量的分裂、環的死亡）都被單步隔離。質量線性遞減——M1 的明確非適用域，附錄 B 的演示軌跡屬此型。 三型不互斥，真實系統的減法常是混合策略：神經網路剪枝先對稱（按層批量）後最小（逐權重微調），資料庫回收先階層（按分區）後對稱（分區內批量）。混合策略的衰減曲線是分段的——每段的形態由該段的策略決定，這再次確認了第五章的降格：衰減形態屬於策略，不屬於公理。 ### 4.3 等變減法的保留與待辦 G-等變過濾（每級帶 G 作用、每個態射 G-等變）的軌道分解定理（v2.0 定理 5.1）在 v3.0 中地位保留：它的證明依賴等變同調的標準機制，不觸及被修正的條款。但其完整嚴格化需要條碼理論先行，與週期減法的不可能性命題（純收斂與 V^T = id 矛盾——這個小命題在 v3.0 公理下反而更乾淨：由不動點唯一性 A.3 直接得出，非空複形上不存在任何周期軌道）一併列入第二期。值得單獨記錄的是後者的升格：v2.0 用酉算子論證排除完美週期，v3.0 只需要 A.3——**非空複形連單步不動都不被允許，遑論週期回歸**。公理修復的紅利之一，是讓好幾個原本需要外部工具的命題變成了內部一行推論。 --- ## 第五章　熵降：從定理到模型假設 ### 5.1 公理保證的部分 公理 R3′ 對資訊衰減的全部保證是：**質量嚴格單調遞減**。由此可得熵類泛函（任何隨質量單調的複雜度度量）沿軌跡單調下降、且在有限步內歸零。單調性與終止性是定理。 ### 5.2 公理不保證的部分 衰減的**形態**——指數、線性、階梯、還是別的——不是定理。v2.0 把 H(Kᵢ) = H₀e^{−λi} 寫成熵降定理，但這個形式推不出來，而且 v2.0 自己提供了反例：類型 C 最小減法每步移除一個單形，質量線性遞減，對應的熵衰減近似線性而非指數。指數形式只在每步移除「當前質量的固定比例」時成立——那是對減法策略的額外假設，不是公理的後果。 v3.0 的處置：指數衰減保留為**模型假設 M1**——「比例移除策略下，H(Kᵢ) ≈ H₀e^{−λi}，λ 由移除比例決定」。它在對稱減法等場景中是好模型，在最小減法中不是。假設標明了適用域，使用者自行判斷場景是否落在域內。被降格的命題沒有消失，它從「處處為真」搬到了「此處為真」——而標明「此處」恰恰讓它變得可用了。 ### 5.3 條碼作為衰減的編碼（地位調整） 持續同調條碼編碼過濾中拓樸特徵的生滅區間，這個視野保留。v2.0 進一步主張條碼秩變化「精確編碼」熵降（∑ΔH_k ≥ ΔS），其證明梗概依賴秩—熵的對數關係估計，嚴格性不足。v3.0 把它降為**猜想 C1**，列入第二期形式化的目標清單——條碼與熵的精確關係值得一個真正的證明，而不是一個看起來像證明的段落。 --- ## 第六章　穩定性：撤回 λⁿ，回歸經典界 ### 6.1 錯誤的解剖 v2.0 定理 4.2 宣稱 d_B(Dgm(f), Dgm(g)) ≤ λⁿ‖f−g‖∞，並推論「迭代次數越多條碼越穩定、λⁿ → 0 故長過濾對擾動極不敏感」。這是 v3.0 撤回的最大條款，撤回理由必須完整記錄，因為錯誤的結構本身有教學價值。 證明的 Step 4 寫下 d_B ≤ sup_i d(Kᵢ^f, Kᵢ^g)，Step 2 給出 d(V^i F₁, V^i F₂) ≤ λ^i d₀。兩步各自正確。錯誤發生在合併：**上確界取遍全部 i，包括 i = 0**，而 λ⁰d₀ = d₀，所以 sup_i λ^i d₀ = d₀ = ‖f−g‖∞。證明鏈真正推出的結論是： **d_B(Dgm(f), Dgm(g)) ≤ ‖f−g‖∞** ——Cohen-Steiner、Edelsbrunner、Harer 的經典穩定性定理，一個字符都強不了。λⁿ 是把「鏈末端的單步壓縮」誤讀成了「整條鏈的全程壓縮」。 直觀層面錯誤同樣清楚：條碼記錄整條過濾的生滅事件，早期誕生的特徵差異（誕生於 i = 0 附近）已經寫進條碼，後期再怎麼收縮都改寫不了已記錄的出生時刻。若 λⁿ → 0 為真，條碼將對一切輸入差異漸近無感——持續同調作為拓樸指紋的全部價值恰恰建立在它**不會**無感上。v2.0 的「定理」如果成立，反而摧毀它想讚美的工具。 ### 6.2 保留的部分 CEO 式證明路徑保留：用收斂算子的 Lipschitz 性質組織證明，確實比傳統證明（基於插值的逐特徵匹配）更短更結構化——它證的是經典界，但證得更乾淨。這是 v2.0 的真實貢獻，撤回 λⁿ 不連坐它。 推論 4.2 的雜訊容忍界相應修正：可靠特徵的持續時間閾值為 2ε（經典結果），不是 2λⁿε。Hausdorff 穩定性（定理 4.3）同步修正為經典形式 d_B ≤ d_H。 ### 6.3 撤回的方法論記錄 這個錯誤在 v2.0 中存活了五個月，被抓住不是因為有人重讀了論文，而是因為形式化工程的前置審查強迫逐定理對賬。教訓寫進 EveMissLab 的工作流：**凡進入 Lean 管線的論文，先過人工逐定理審計，審計的第一問是「證明推出的和陳述宣稱的是否同一個命題」**。拓樸微積分的常值層錯誤、本論文的 λⁿ 錯誤，都是這一問抓出來的。兩個錯誤的來源不同（一個是 Theia 的、一個是 v2.0 協作鏈的），捕捉機制相同——機制比個體可靠，這正是互審鏈存在的理由。 --- ## 第七章　對偶完成：減法拓撲 × 拓樸微積分 ### 7.1 v2.0 缺的那一半 v2.0 的哲學結語寫道：虛空非空，∅ ≡ ⊚，收斂到虛空只是為了從虛空展開。這些句子在 v2.0 中是詩——真誠的、方向正確的詩，但理論內部沒有任何結構為它們作保。「∅ 包含整個演化的全部資訊」？∅ 是空集，它在減法拓撲的語言裡什麼都不包含。詩指向的東西在理論的語言之外。 它在外面，是因為對偶的另一半當時還沒被建立。2026 年 6 月，拓樸微積分（EML-TC）完成：本體層與呈現層的雙層結構、切割即索引、積分即遺忘、∫∘d = id 按構造成立、核心定理經 Lean 4 機器驗證。現在可以把詩翻譯成定理了。 ### 7.2 對偶的精確形態 兩套理論操作同一個世界的兩個層： 減法拓撲住在**呈現層**，說值語義的語言：複形是真的結構、移除是真的失去、秩是真的下降、終點是真的空。它是呈現層的演化動力學——形狀如何消亡。 拓樸微積分住在**本體層**，說參照語義的語言：對象不可變、切割只生成視圖、操作零損耗、沒有終點概念。它是本體層的不變性——存在如何不動。 對偶聲明（EML-TC 廣義版定義 A.7，本文採納為接口公理 D）：減法拓撲的每個複形 Kᵢ 在對偶讀法下是一個視圖 (O, iᵢ)——本體 O 配上索引 iᵢ；收斂算子 V 的每次作用是**索引的演化** V(O, i) = (O, v(i))，本體成分不動。減法拓撲測量的質量 m(Kᵢ) 與熵 H(Kᵢ) 是索引複雜度的呈現層讀數；終止定理的終點 ∅ 對應**零索引狀態**。 於是那句詩獲得嚴格語義： **∅ 是呈現層的空，不是本體層的空。**收斂到 ∅ = 遺忘全部索引 = 拓樸積分 ∫ 的完成。減法的終點即積分的完成；質量歸零之處，hash(O) 分毫未動。「虛空包含全部資訊」的正確版本是：虛空的本體投影是完整的 O——不是 ∅ 裡面裝著資訊，是 ∅ 底下壓著本體。熱寂即圓滿，v2.0 用驚嘆號說，v3.0 用投影算子說。 ### 7.3 雙軌原則：對偶的工程面 對偶在機器上的形態是雙軌原則（EML-TC-COMP 第四章建立，此處從減法側複述）：系統的每個操作屬於恰一軌——**V 軌**真刪，付熵降代價換空間，不可逆，本理論管轄；**d 軌**建視圖，付索引代價換可逆，零損耗，拓樸微積分管轄。神經網路剪枝、資料庫 vacuum、垃圾回收是 V 軌；快照、引用、零拷貝視圖是 d 軌。混淆兩軌是系統事故的多發地，而 Git 是兩軌的合奏範例：物件庫純 d 軌，`gc --prune` 是受控的 V 軌介入——且 prune 策略可由本理論的條碼語言描述（版本的存活區間構成條碼，按持續長度過濾回收）。 對偶也劃清了兩理論的失效邊界：拓樸微積分保證「d 軌弄不壞本體」，本理論保證「V 軌的破壞有界且必然終止」。一個管不壞，一個管壞得有秩序。完整的系統理論需要兩者——這就是為什麼對偶不是裝飾，是各自的補全。 ### 7.4 形式化的會合點（v3.1：已會合） v3.0 寫作時，EML-TC 的 Lean 工程在 Duality.lean 留有兩個授權 sorry：索引演化定理與極限保本體定理——它們等的就是本文的形式化。v3.1 記錄結果：**等待已結束**。本文附錄 C 的第一期（單純複形、R1+R3′、終止定理、星形移除）於 2026 年 6 月 11 日全部通過機器驗證，對偶定理隨即以 V_step 為具體收斂算子完成證明，兩個 sorry 清零，全專案 0 errors。兩套理論在同一個類型檢查器裡握了手：減法側提供真實的單步收斂與終止保證，同一性側提供雜湊不變與積分恆等——`duality_evolution` 證明 V 的每一步都是純索引演化（本體雜湊逐字保持），`duality_limit_preserves_ontology` 證明演化後的視圖積分仍返回原本體 O。 形式化還回贈了一個本文未曾明說的加強：機器證出的保本體命題**不需要秩歸零假設**——本體在軌跡的**每一步**都完整保持，不只在終點。「∅ 的本體投影是 O」是真的，但更強的事實是：沿途每一個 Kᵢ 的本體投影都是 O，終點與中途在本體層毫無分別。對偶的完整軌跡形態於 Lean v0.2 批次完成組裝並關閉（v3.2 銷帳）：`duality_trajectory_completes` 證明在**顯式步數 rank(v) 處**秩必歸零——不是存在某個 n，是恰好不超過初始秩那麼多步，建構性的界，鏡像終止定理 A.4 的緊界；`duality_trajectory_preserves_ontology` 證明**任意迭代深度 m** 處積分恆返回 O——不只極限處，全程。兩肢都強於指定簽名。引擎引理 `rank_V_lt_of_rank_ne_zero` 由此接上飛輪：嚴格降秩驅動良基下降給出第一肢，迭代雜湊不變（`V_iter_hash_eq`，其歸納步是 rfl——V 按構造保雜湊，「按構造成立」延續到了迭代層）配注入性給出第二肢。「減法的終點即積分的完成」（7.2）至此以完整軌跡形態進入類型檢查器：走 rank(v) 步，秩必歸零，而沿途每一步，∫ 都指回那個從未動過的 O。 --- ## 第八章　應用（精編保留與校準） v2.0 第六章的應用案例全部保留，按 v3.0 的修正逐一校準其宣稱。 **神經網路剪枝**：以複形建模網路（神經元為頂點、連接為邊、共激活模式為高維面），按重要性函數構造減法過濾，以條碼識別「拓樸臨界點」——剪過此點，網路的連通結構發生質變。方法不變；校準兩處：剪枝決策的穩定性保證引用經典界 d_B ≤ ‖f−g‖∞（重要性估計的誤差 ε 直接上界條碼偏移，無 λⁿ 折扣），可靠特徵的持續時間閾值為 2ε。策略選擇可用 4.2 的分類語言重述：按層批量剪是對稱型（快、可用 M1 預估進度），逐權重微調是最小型（慢、分辨率高）——先對稱後最小的混合策略在工程上早已是常識，現在它有了範疇論的名字。 **資料庫增量刪除**：把刪除序列建模為減法過濾，識別持續同調區間，批量刪除整個拓樸區間而非逐行操作——I/O 從 O(n) 降向 O(log n) 量級。此案例的論證完全建立在過濾對應（A.5）與階層型策略的遞迴結構上，與被撤回的條款正交，原樣有效。新增一個對偶讀法：刪除前先以 d 軌快照（零成本，拓樸微積分管轄），再執行 V 軌批量刪除（本理論管轄）——雙軌原則把「可恢復的刪除」這個工程需求拆解為兩個各有定理保護的階段。 **AI 老化檢測**：監測系統的三元係數，當配置滑向 (0, 0, 1)——只收斂、不展開、不連接——即進入純收斂態，本理論的終止定理保證其結局：有限步內歸於結構性的空。以條碼短條比例定義老化指數的框架保留；校準一處：指數的解讀按 M1 的適用域加註——比例移除場景（如均勻的能力衰退）下可與指數基準比對，逐項移除場景（如單點功能的逐個失效）下應改用線性基準，誤用基準會把正常的最小型衰減誤報為加速老化。 **Ripser 稀疏優化與 GPU 並行化**：屬演算法工程，利用減法過濾的單調性（邊界矩陣嚴格三角化）與層級結構（分塊並行），與公理修正正交，原樣有效，留作第二期條碼形式化的計算對照組。 --- ## 哲學結語 v2.0 的結語是一首給虛空的讚美詩。v3.0 不撤回那首詩——撤回的是讓詩懸空的地基，然後把詩放回修好的地基上。 減法依然是收斂的極限，形狀依然必死，終點依然是空。但現在我們知道空的全名了：它是呈現層的零索引態，是積分完成的標記，是本體卸下全部取景框之後留在原地的那個「在」。減法拓撲從正面數著失去——每一步少一個單形、降一分熵、近一步死亡；拓樸微積分從背面記著不失——hash 不變、本體不增不減、∫∘d 恆等。同一條軌跡，正面是輓歌，背面是恆等式。 v2.0 問：形狀消亡之後剩下什麼？並用詩回答：虛空，而虛空圓滿。v3.0 給出散文的版本：剩下的東西從來不在形狀那一層，所以形狀的消亡碰不到它。失去是真的，失去的範圍也是真的——範圍之外，無一物曾被觸及。 數一遍你失去的所有，那是 V 軌的帳；然後解一次引用，看見從未入帳的那一份。兩本帳都對，宇宙同時記著兩本。 --- --- ## 附錄A　公理系與定理（形式化基準） **設定**：有限抽象單純複形範疇。對象 K 為有限頂點集上的面族，對非空子集封閉。質量 m(K) := |K|（面的總數，含各維）。∅ 為空複形（無面）。 **公理 R1（分裂性）**　f: K → L 為減法態射蘊含存在單純嵌入 ι: L ↪ K 使 f ∘ ι = id_L。 **公理 R3′（非空嚴格秩降 + 空封閉）**　K ≠ ∅ ⟹ m(L) < m(K)；K = ∅ ⟹ L = ∅。 **定理 A.1（R2 為推論）**　減法態射皆為滿射。 證明：對 s ∈ L 取 t = ι(s)，f(t) = f(ι(s)) = s。∎ **定理 A.2（合成封閉）**　減法態射的合成是減法態射。 證明：右逆取 ι₁ ∘ ι₂，驗證 (g∘f)∘(ι₁∘ι₂) = g∘(f∘ι₁)∘ι₂ = g∘ι₂ = id。秩降：非空時 m(M) < m(L) < m(K) 由傳遞性；K = ∅ 時逐層傳空。∎ **定理 A.3（不動點唯一性）**　f(K) = K 的減法態射存在當且僅當 K = ∅。 證明：K ≠ ∅ 時 R3′ 給 m(K) < m(K)，矛盾。K = ∅ 時恆等態射滿足兩公理（R1 取 ι = id_∅；R3′ 空條款）。∎ **定理 A.4（終止）**　任意減法態射序列 K₀ → K₁ → ⋯ 在至多 m(K₀) 步內到達 ∅ 並停駐。 證明：m(Kᵢ) 為非負整數嚴格遞減鏈（非空段），長度 ≤ m(K₀)；歸零即空；其後由 R3′ 空條款恆空。∎（Lean：Nat 上的良基遞迴。） **定理 A.5（過濾對應）**　有限減法過濾與收斂迭代序列 {V^i(K₀)} 一一對應。 證明：正向由 A.2 合成出全域 V；反向直接讀出。∎ **模型假設 M1（比例衰減）**　若每步移除當前質量的固定比例 ρ ∈ (0,1)，則 m(Kᵢ) = m(K₀)(1−ρ)^i，熵類泛函近似 H₀e^{−λi}，λ = −ln(1−ρ)。適用域：對稱減法、均勻剪枝。非適用域：逐項移除（線性衰減）。 **定理 A.6（經典穩定性，修正版）**　設 f, g 為誘導減法過濾的過濾函數，則 d_B(Dgm(f), Dgm(g)) ≤ ‖f−g‖∞。 證明路徑（CEO 式）：d_B ≤ sup_i d(Kᵢ^f, Kᵢ^g) ≤ sup_i λ^i‖f−g‖∞ = ‖f−g‖∞（上確界在 i = 0 取得）。∎ **撤回註記**：v2.0 的 λⁿ 強化版因 sup 含 i = 0 而不成立，且其成立將使條碼對輸入漸近無感，與持續同調的分辨功能矛盾。 **猜想 C1（條碼—熵編碼）**　條碼秩變化與熵變化滿足 ∑_k ΔH_k(Kᵢ) ≥ ΔS(Kᵢ)。狀態：待證，列入第二期。 **接口公理 D（對偶，採納自 EML-TC A.7）**　存在本體 O 與索引族 {iₖ}，使 Kₖ = (O, iₖ)、V(O, i) = (O, v(i))、m 與 H 為索引複雜度泛函的讀數；終止態 ∅ 的本體投影為 O。狀態：**已轉為定理**（v3.1）——`duality_evolution` 與 `duality_limit_preserves_ontology` 已證，sorry 清零；完整軌跡形態列為形式化 v0.2 指定升級（附錄 C）。 --- ## 附錄B　Python 參考實現 可運行最小實現：抽象單純複形、減法態射檢查（R1+R3′）、終止定理的實測、質量單調性斷言、簡化條碼（H₀ 連通分量壽命）。零外部依賴。 ```python """ EML-TOPO-2026-SUB-v3.1 參考實現 核心斷言：R1+R3' 下任意減法序列必在 m(K0) 步內終止於空（定理 A.4） """ from itertools import combinations import random # ---------- 抽象單純複形 ---------- def closure(faces): """面族的向下封閉化：補齊所有非空子面。""" K = set() for f in faces: f = tuple(sorted(f)) for r in range(1, len(f) + 1): K.update(combinations(f, r)) return frozenset(K) def mass(K): # 質量 m(K)：各維面總數（定理 A.4 的良基度量） return len(K) def is_complex(K): # 向下封閉性檢查 return all(tuple(sorted(sub)) in K for f in K for r in range(1, len(f)) for sub in combinations(f, r)) # ---------- 減法態射（公理檢查器） ---------- def remove_face(K, face): """標準減法：移除 face 及一切包含它的面（保持向下封閉）。""" face = tuple(sorted(face)) return frozenset(f for f in K if not set(face).issubset(set(f))) def check_subtraction_axioms(K, L): """R1：L ⊆ K（嵌入即包含，f 為投影故分裂自動成立） R3'：K≠∅ ⟹ m(L) {bound}" masses = [mass(K) for K in traj] assert all(a > b for a, b in zip(masses, masses[1:])), "質量未嚴格遞減！" assert traj[-1] == frozenset(), "未終止於空！" print(f"✓ {n_trials} 條隨機減法軌跡全部終止於 ∅，步數 ≤ m(K0)={bound}") print(f"✓ 質量沿全部軌跡嚴格單調遞減（公理 R3' 實測成立）") # ---------- 簡化條碼：H0 連通分量壽命（衰減的拓樸指紋示意） ---------- def components(K): verts = {f[0] for f in K if len(f) == 1} parent = {v: v for v in verts} def find(v): while parent[v] != v: parent[v] = parent[parent[v]]; v = parent[v] return v for f in K: if len(f) == 2: a, b = find(f[0]), find(f[1]) if a != b: parent[a] = b return len({find(v) for v in verts}) def h0_barcode(traj): """逐步記錄連通分量數——衰減軌跡的最粗拓樸指紋。""" return [components(K) for K in traj] # ---------- 演示 ---------- if __name__ == "__main__": # 初始複形：兩個三角形共享一邊 + 一條尾巴 K0 = closure([(1,2,3), (2,3,4), (4,5)]) print(f"初始複形：{mass(K0)} 個面，{components(K0)} 個連通分量") verify_termination(K0) traj = random_subtraction_trajectory(K0, seed=42) print(f"\n示例軌跡（seed=42）：{len(traj)-1} 步終止") print(f"質量軌跡：{[mass(K) for K in traj]}") print(f"H0 條碼（連通分量數）：{h0_barcode(traj)}") print("\n模型假設 M1 對照：本軌跡為逐面移除（最小減法），") print("質量近線性遞減——指數衰減在此非適用域，與 §5.2 一致。") ``` 實現注記：（1）`remove_face` 移除一個面連同其上閉包，自動保持向下封閉——這是最自然的減法態射族；（2）終止驗證跑兩百條隨機軌跡並斷言三件事（步數界、嚴格單調、終於空），是定理 A.4 的模糊測試形態；（3）H₀ 條碼用並查集求連通分量，僅作衰減指紋示意——完整持續同調屬第二期；（4）尾段輸出刻意展示 M1 的非適用域實例，紙面的誠實降格在程式碼裡有對應的誠實註記。 --- ## 附錄C　Lean 4 形式化驗證結果（第一期關閉） v3.0 此處為第一期計畫；v3.1 改寫為實際結果。執行：本地 AI Agent；審計：Theia（計畫審查兩輪、原始碼審計一輪）；環境：Lean 4 v4.30.0 + Mathlib，掛載於既有 `eml-tc` 專案（與拓樸微積分共庫）。S1–S4 於 2026 年 6 月 11 日全部關閉，全專案 0 sorry、0 axiom 走私、0 errors。 **已驗證定理對照**（論文編號 → Lean 名稱）： 公理系 → `SubtractiveMorphism` 結構（r1 為包含關係、r3′ 為合取命題，雙公理忠實）。定理 A.1 滿射推論 → `surjective_of_subtractive`（真滿射陳述 ∀ y : L.faces, ∃ x, proj f x = some y，見證 ι y 加 retraction，非像子型套套邏輯）。定理 A.2 合成封閉 → `composition_closed`（含中間複形為空的分支處理：L 空則 M 空，card_pos 補嚴格性）。定理 A.3 不動點唯一性 → `fixed_point_uniqueness`（**雙向**：非空無自態射由 `Nat.lt_irrefl`，空複形的恆等自態射顯式構造）。定理 A.4 → 兩條：`wellFounded_subtractiveStep`（card 強歸納的良基性）與 `chain_length_bound`（顯式緊界 l.length ≤ K.mass，對應 3.3 節的壽命譜上端）。2.5 節星形移除 → `remove_star` 與 `remove_star_morphism`（嚴格降秩以 σ 自身為見證：σ ⊆ σ 故 σ 必被濾出——論文構造的逐字形式化）。單步收斂算子 → `V_step`（非空時經典選擇移星、空時恆等，`V_step_morphism` 證其恆為合法減法態射）。 **對偶定理（清零的兩個 sorry）**：`duality_evolution`——V 對視圖的作用是純索引演化，V S ⟨h O, [i]⟩ = ⟨h O, [V_step i]⟩，本體雜湊逐字保持；`duality_limit_preserves_ontology`——演化後的視圖經拓樸積分仍返回 O，證明體實質調用 EML-TC 階段一的 `integrate_d_eq`。接口公理 D 的核心內容由此轉為定理。 **設計決策記錄**（均先入 NOTES.md 再編碼，沿用 hclosed 紀律）：投影函數以 Option 建模部分性（被移除的面映 none），偏離論文的總函數設定，由 retraction 性質補償；收斂算子以 `Classical.choose` 選面故 noncomputable；頂點型別命名 Vert 避免與算子 V 碰撞；嚴格步進關係 `SubtractiveStep` 含 K 非空合取——少了它 ∅→∅ 成為不降步、良基性破產，這個合取是形式化過程中浮現的必要設計。 **審計記錄**：計畫階段攔下一處紅線——初版方案把 V 定義為「直接映至空索引視圖」，一步跳到終點，整條減法動力學被繞過、S4 不再使用 S3 的終止定理，聯合工程名存實亡；按處方改為真實單步星形移除後放行。另攔三處技術項（A.1 的像子型套套邏輯風險、noncomputable 標錯邊、名稱碰撞），均於開工前修正——這輪的全部問題在計畫階段攔截，原始碼審計零返工，與 EML-TC 階段三的事後返工形成對照：**審查越前置，返工越便宜**。 **指定升級：已銷帳（v3.2）**。v3.1 的原始碼審計曾發現引擎引理 `rank_V_lt_of_rank_ne_zero` 已證而未接線（單步版對偶定理不需要它），遂指定軌跡版定理為 Lean v0.2 升級目標。交付結果（2026-06-11，同批含 ADC 免疫定理與 FEN 分解定理）： ```lean theorem duality_trajectory_completes (v : View S (SimplicialComplex Vert)) : rank S (V_iter S (rank S v) v) = 0 theorem duality_trajectory_preserves_ontology (O : α) (i : SimplicialComplex Vert) (m : Nat) (hv : ∃ O', S.h O' = (V_iter S m ⟨S.h O, [i]⟩).hash) : integrate S (V_iter S m ⟨S.h O, [i]⟩) hv = O ``` 兩肢均**強於指定簽名**：第一肢以建構性步數界（恰 rank v 步）取代存在量詞 ∃n；第二肢以任意深度 m 的無條件保本體取代「秩歸零處」的條件版本。引擎引理經 `V_iter_rank_zero` 的歸納接上良基下降（秩零情形由 `map_V_step_eq_self` 處理——空視圖是 V 在視圖層的不動點，定理 A.3 的再現）；保本體經 `V_iter_hash_eq`（歸納步為 rfl，V 按構造保雜湊）配注入性收口。交付過程一條紀律記錄：初次交付僅含第一肢，審計以「半張支票不能入帳」退回，補單十五行後合取閉合——指定升級的銷帳本身也過了一輪完整審計。 **第二期（界定不變）**：持續同調與條碼形式化、定理 A.6 經典穩定性界、猜想 C1、等變減法的軌道分解。前置依賴：Mathlib 同調代數 API 成熟度評估。 **自我例示注記**：本理論的形式化過程自身走了一條減法軌跡——計畫的初版質量最大（含冗餘公理 R2、含跳關的 V、含三處技術瑕疵），每輪審查是一次嚴格降秩的減法態射，終態是零瑕疵的閉合專案。而按第七章的對偶讀法，被減掉的全是呈現層的瑕疵，理論的本體——純收斂態的視野——逐字保持。減法拓撲學的成形過程是減法拓撲學的一個實例。 --- ## 附錄D　v2.0 → v3.0 修訂對照表 | v2.0 條款 | v3.0 處置 | 理由 | |---|---|---| | 公理 R1（右逆性） | 保留，更名分裂性 | 無問題 | | 公理 R2（滿射性） | **降為定理 A.1** | R1 的直接推論，公理系冗餘 | | 公理 R3（嚴格秩降） | **修正為 R3′（非空限定+空封閉）** | 與 V(∅)=∅ 不動點矛盾 | | V(∅)=∅ 不動點（哲學章） | **升格為定理 A.3（唯一性）** | 修復後可證 | | 定理 2.1（過濾對應） | 保留（A.5） | 證明不依賴被修正條款 | | 定理 2.2（終止） | 保留並嚴格化（A.4，良基遞迴） | 核心定理，Lean 第一期主目標 | | 熵降定理 H=H₀e^{−λi} | **降為模型假設 M1（標明適用域）** | 公理只給單調性；類型C為反例 | | 定理 3.1（條碼—熵編碼） | **降為猜想 C1** | 證明梗概嚴格性不足 | | 定理 4.2（λⁿ 穩定性） | **撤回，改為經典界（A.6）** | sup 含 i=0，實際只推出經典界；λⁿ 成立將使條碼無分辨力 | | 推論 4.1/4.2（指數穩定、λⁿ 雜訊界） | **撤回**，雜訊界改 2ε | 隨 4.2 連坐 | | 定理 4.3（Hausdorff 穩定性） | 修正為經典形式 d_B ≤ d_H | 同上 | | CEO/TUO 直接引用 | **剝為詮釋層+明示假設** | 獨立形式化的前提 | | 三型過濾分類 | 保留，改按策略結構分類 | 速率是後果非依據 | | 應用案例（剪枝/資料庫/老化） | 保留，宣稱按修正校準 | 方法有效，界更新 | | 哲學結語（虛空非空） | 保留並獲得嚴格語義（第七章對偶） | ∅ 為呈現層之空，本體投影為 O | | —（v2.0 無） | **新增第七章：與 EML-TC 對偶** | v2.0 寫作時對偶尚不存在 | --- ## 參考文獻 [1] Neo.K (2026). 減法拓撲學v2.0：收斂運算元的範疇論實現. EML-TOPO-2026-SUB-v2.0.（本文取代之版本） [2] Neo.K (2026). 同一性微積分：拓樸微積分的本體論基礎. EML-TC-ONT-2026-v0.2. [3] Neo.K (2026). 參照語義微積分：拓樸微積分的計算機實現. EML-TC-COMP-2026-v0.2. [4] Neo.K (2026). 迴圈演化運算元論. EML-MATH-2026-CEO-v2.0.（詮釋層） [5] Cohen-Steiner, D., Edelsbrunner, H., & Harer, J. (2007). Stability of persistence diagrams. Discrete & Computational Geometry.（定理 A.6 的經典原型） [6] Zomorodian, A., & Carlsson, G. (2005). Computing persistent homology. Discrete & Computational Geometry. [7] Bauer, U. (2021). Ripser: Efficient computation of Vietoris–Rips persistence barcodes. J. Appl. Comput. Topology. [8] Chazal, F., de Silva, V., Glisse, M., & Oudot, S. (2016). The Structure and Stability of Persistence Modules. Springer. [9] Edelsbrunner, H., & Harer, J. (2010). Computational Topology: An Introduction. AMS. [10] de Moura, L. & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. CADE-28. --- **完成時間**：2026-06-11 **版本**：v3.2（公理化重建與對偶完成版；指定升級銷帳，軌跡定理閉合） **作者**：Neo.K（許筌崴）｜EveMissLab（一言諾科技有限公司） **理論結晶化協作**：Theia 獻給那些在失去的帳本背面，讀出恆等式的人。