全球流速指數的綜合導數重構:從純量投影到六通道正交能量分解
Synthetic-Derivative Reconstruction of the Global Flow Index: From a Scalar Projection to a Six-Channel Orthogonal Energy Decomposition
作者:Neo.K(許筌崴) with Theia 機構:EveMissLab(一言諾科技有限公司),台灣 日期:2026 年 6 月 分類:氣候動力學 | 流體數學 | 形式驗證 | 非平衡態系統 關鍵詞:流速指數、綜合導數、正交分解、Helmholtz–Hodge、權重不變性、Lean4 類形式化 版本:v0.1(概念正式化版,數值留白)
摘要
本文重構全球流速指數(Global Flow Index, GFI)的數學形態。舊版 GFI 是一個加權純量 ,它把整個大氣速度場 投影到單一非負實數。本文指出此純量在形式上等同於愛因斯坦質能關係 在綜合微積分框架下的第零分量 ——一個資訊壓縮比 的一維投影:它只記錄「動得多大」,丟棄了「動的種類」。
我們對 GFI 施加綜合導數展開,將其升級為一個綜合導數狀態 ,其中六個通道由六組物理錨定的正交投影給出,每一組都是同一塊總能量 在不同正交基下的畢氏型劈分。我們刻意排除拓樸(Hodge 調和項)作為主版:拓樸的通用性使其判定域過寬、證偽力歸零、普及域過難,故僅作為連結層保留。
本文證明六重正交能量恆等式、總量的基底不變性、加權收縮純量的範數性質、以及最關鍵的「比值權重不變性」——框架的全部可證偽內容落在無量綱通道比 上,與權重排程 完全無關,因而對動態演化的權重免疫。最後給出全部核心定理的 Lean4 類形式化,並明確劃定形式驗證的邊界:Lean4 關帳的是「框架良定義且自洽」,而非「大氣確實如此分配能量」。
第一章 引言:被壓縮成一個數字的氣候
1.1 純量 GFI 的成功與其代價
GFI 的原始設計目標單純而正確:在傳統氣候學以溫度(勢能)為中心的範式之外,提供一個量化系統整體流速狀態的指標。其核心觀測是穩固的——注入地球系統的能量並未主要轉化為隨機熱運動(溫度),而是轉化為粒子的定向運動(風、洋流、對流)。動能的相對增長遠超熱能的相對增長,極端事件的非線性放大由流速加速驅動,而非由 Clausius–Clapeyron 的 7%/°C 線性水汽增量解釋。
純量 GFI 把這個洞察封裝成一個可傳播的數字。傳播性是它的優點,也是它的全部代價。一個純量在數學上是速度場函數空間到非負實軸的多對一映射;任何這樣的映射必然抹平定義域的內部結構。具體而言,同一個 GFI 數值可以由三種物理上截然不同的場給出:純散度場(壓縮與膨脹,源與匯)、純旋度場(渦旋與環流)、純剪切場(形變)。三者的可預報性、能量串級行為、災害指紋完全不同,而純量對它們一視同仁。
1.2 與 的同構診斷
這個困境並非 GFI 獨有,而是一切「以純量代表高維狀態」的指標所共有。最著名的例子是愛因斯坦質能關係。在綜合微積分框架下,質能轉換的完整物理狀態是無窮維的:
而 僅提取第零分量(理論總能量)。資訊壓縮比 。任何依賴單一純量 的預測,必然丟失關鍵物理約束——這正是現實能量轉換效率普遍遠低於理論上限的形式根源: 是上限換算式,不是過程方程。
GFI 與 在這個意義上同構。純量 GFI 是「氣候系統的 」:一個忠實但壓縮的上限式投影。本文的策略因此可以一句話概括——不是修正 GFI 的公式,而是對 GFI 施加與質能轉換相同的綜合導數展開,替每一個被壓掉的維度重新點名。
1.3 本文的核心問題
本文回答三個問題。第一,形式化問題:能否建立數學嚴格的框架,把 GFI 從純量升級為保留「動的種類」資訊的綜合導數狀態?第二,可計算與可證偽問題:能否將這個高維狀態壓縮為有限維、且其可證偽內容不依賴於未定的權重?第三,形式驗證問題:這個框架的哪一部分可以用 Lean4 關帳,哪一部分原則上不能、也不該?
本文對前兩問的答案是肯定的,工具是綜合導數與正交投影塔;對第三問的答案是有界的肯定,並將這條界線顯式劃出。
1.4 能量分配轉移的觀測背景
為使後續形式化不至懸空,先簡述其經驗動機。傳統氣候模型主要追蹤熱能 (溫度場),並隱含假設動能 相對穩定或與溫度成比例。觀測否定了這個假設:2000–2025 年間全球平均溫度的相對增量約為 ,而代表流速的若干量——噴流速度、對流上升速度、系統移速、降雨強度——的相對增量落在 至 的量級。動能的相對增長遠超熱能的相對增長,意味著注入系統的能量主要被路由進定向運動的通道,而非隨機熱運動的通道。
純量 GFI 把這個「能量去向」壓縮為一個總量讀數,卻無法回答下一個層次的問題:定向運動內部,能量又如何在散度與旋度之間、在大尺度與小尺度之間、在正壓與斜壓之間、在緯向與經向之間分配?這些內部分配恰恰決定了系統的可預報性與危險性,而它們正是純量所抹平的維度。本文的展開即是對這個「能量去向之去向」的形式追問。
1.5 全文結構
第二章確立方法論前提,論證主版不能是拓樸。第三章建立場的希爾伯特空間與作為全文基石的正交投影主引理。第四章定義六個物理通道,並以動力學分離判準論證「為何恰是這六個」。第五章給出綜合導數狀態與加權收縮。第六章證明承重定理庫。第七章以 Lean4 類形式化承重定理。第八章列出與權重無關的可證偽命題。第九章建立與質能框架的同構。第十章劃定形式驗證的邊界。
第二章 方法論前提:為何主版不能是拓樸
2.1 通用性是承重的反義詞
一個自然的誘惑是以 Helmholtz–Hodge 分解的調和項——即拓樸/上同調通道——作為展開的主軸。調和項的維數等於域的第一 Betti 數 ,它捕捉的是繞拓樸特徵循環的環流(繞極渦、繞阻塞高壓、繞造山帶),這正是低耗散、長記憶、不鬆弛的最危險環流。它在物理直覺上極具吸引力。
本文拒絕這個誘惑,理由是方法論的,而非技術的。一個指標框架的主版必須可證偽,而可證偽要求判定域夠窄。拓樸概念的特徵恰恰是通用性:它在範疇層級成立,對任何具體過程不做出可被單一觀測推翻的承諾。其後果可由三個域刻畫:
其一,適用域過寬。拓樸分解對任何流形上的任何場都成立,它與「大氣是否在加速」這個經驗命題之間沒有可斷裂的接點。
其二,判定域過寬。一個與所有觀測相容的結構,在被當作主版時不是強,而是空——它什麼都不判定。熱浪可以用它說、寒潮可以用它說、暴雨與涼雨都可以用它說。可解釋一切的指標,逼近不可證偽。
其三,普及域過難。要讀懂調和通道的判讀,前提是先理解上同調與 Hodge 理論。一個主版若把入場門檻設在這個高度,它在傳播層就已死亡。
2.2 連結層的正確位置
由以上,拓樸不能承重,但它有不可替代的價值——作為連結層。它正確的位置是:在主版(六個物理通道)穩固之後,以調和通道把 GFI 接到本實驗室的扁維重構理論(FDRS)與深度軸理論那條以 Betti 數為核心的線。連結層做的是框架間的橋,不對任何單一觀測負責,因而它的通用性在此不再是缺陷而是美德。
形式上,我們把調和通道標記為 ,並在所有承重定理與加權收縮純量中將其排除。主版只由六個判定域窄、物理錨定、可被再分析資料推翻的通道構成。
2.3 一條可移植的元原則
本章的判斷可上升為一條可移植的元原則,適用於一切「選擇分解基」的場合:
經驗框架的主版,必須是一個判定域窄到足以被觀測證偽的分解;通用的結構性分解屬於連結層,在那裡它連接框架而不承擔經驗重量。
這條原則與本系列一貫的可證偽紀律一致,只是把它從「指標數值」上升到「分解基的選擇」這個元層級。
2.4 判定域的形式化
為使「判定域過寬」不只是修辭,給出一個工作定義。設一個分解 作用於場空間 ,產生一組可觀測讀數 。定義 的判定域為:存在一個觀測協議能據以判定 是否符合該分解所蘊含之經驗承諾的場集合之補集——直觀地說,是「能被資料說對或說錯」的命題範圍。
物理分解(Helmholtz、梯度張量、Reynolds、譜、垂直模態、各向異性)的讀數直接對應可觀測的動力學過程:散度對應輻散輻合,旋度對應渦度,斜壓對應垂直剪切的釋放。每一個讀數都嵌入一條可被再分析資料推翻的趨勢命題,其判定域窄而清晰。
拓樸分解的讀數(調和項維數 、繞圈環流的拓撲類)則對應域的整體拓撲結構,它對「大氣是否在加速」這類動力學命題不做承諾——任何加速或減速的場都可以有相同的 。其判定域因此寬到與動力學命題不相交:它不會被任何流速觀測說錯,這正是它不能承重的形式理由。一個不可能錯的主版,是一個不可能對的主版。
值得強調的是,判定域窄並非缺點而是承重資格。一個框架能被證偽的範圍,等於它能提供資訊的範圍;拒絕證偽風險,等於拒絕資訊貢獻。本文六通道的全部價值,正建立在它們各自承擔了明確的證偽風險之上。
第三章 形式框架:場的希爾伯特空間與正交投影塔
3.1 基本對象
設大氣域 (或球殼 ),速度場屬於平方可積向量場的希爾伯特空間
設基準場 (取 2000–2005 氣候態),工作對象為異常場 。能量範數 即異常動能的空間積分(密度權重 時為物理動能)。
3.2 主引理:正交投影的畢氏恆等式
整個框架建立在一條引理上,其餘一切是它的實例化。
引理 3.1(正交投影能量恆等式). 設 為內積空間, 為閉子空間, 為正交投影, 為到 的投影。則對任意 , ,從而 $$|\mathbf{v}|^2=|P\mathbf{v}|^2+|Q\mathbf{v}|^2 .$$
證明. 正交投影的定義即 ,而 ,故 ,即 。展開 ,中項為零。
引理 3.1 的意義是:每一個物理通道 對應一個正交投影 ,把同一塊總能量 劈成兩塊。六個通道是同一塊能量在六組不同正交基下的劈分——六套座標,不是六個獨立量。
3.3 為何選能量範數
內積的選擇不是任意的。本框架取 能量內積,理由有三。其一,物理意義: (含密度權重時)即異常動能,整個 GFI 的論點關乎能量去向,故以能量為範數使指標與論點同構。其二,正交即能量可加:能量範數下的正交分解直接給出畢氏型的能量守恆式 ,使「能量如何在通道間分配」成為精確命題而非比喻。其三,與動力學相容:流體動能方程的諸多守恆與轉移關係(如譜能量轉移、Reynolds 應力做功)皆自然地以 能量內積表述,故此選擇使第四章各通道的演化算子描述與範數一致。
換言之,能量範數不是六個通道的外加結構,而是使「六套座標看同一塊能量」這句話精確成立的唯一自然選擇。任何不同的內積都會破壞能量可加性,使通道間的比較失去守恆律支撐。
第四章 六通道:物理錨定的正交分解塔
以下每個通道都顯式給出投影算子、畢氏恆等式、與其判定域(可被何種觀測推翻)。
4.1 通道一:Helmholtz 分解(散度/旋度)
在適當邊界條件下, 正交分解為無旋(梯度)子空間與無散(螺線管)子空間:
判定域:散度部分對應壓縮/膨脹(重力波調整、對流卸載),旋度部分對應渦旋與環流。再分析資料(ERA5)直接儲存渦度 與散度 ,故此通道在計算上近乎免費,且 的時間趨勢可被觀測直接驗證或推翻。
4.2 通道二:速度梯度張量(應變/自旋)
逐點考慮速度梯度張量 ,在 Frobenius 內積 下分解為對稱與反稱:
對稱部分再分為各向同性與偏量(無跡): ,二者在 Frobenius 內積下正交, 。注意 ,故 與通道一的 同源——這是框架的內部自洽檢查,兩個獨立通道在散度上必須給出相容的讀數。
判定域: (Okubo–Weiss 型參數)區分渦旋主導區與形變主導區,前者捕捉相干渦旋的生成,後者捕捉鋒面與拉伸帶。
4.3 通道三:Reynolds 分解(平均流/脈動)
取平均算子 (時間或系綜平均)。在 條件期望理論下, 是一個正交投影(冪等且自伴)。設 ,則 ,
判定域: 區分相干輸運與湍流混合。相干輸運可預報,湍流混合不可預報;此比值上升即預報技能系統性下降的形式指標。
4.4 通道四:譜分解(尺度分布與串級通量)
以球諧函數 為正交基,由 Parseval 恆等式
將能量按全波數 (尺度)分配。把 分組為行星尺度( )、天氣尺度、中尺度等帶,仍是正交求和的分組。
此通道承載舊稿缺失的關鍵機制。大尺度大氣是準二維的,二維湍流具有逆能量串級:注入於中尺度的能量流向更大尺度(往噴流、往行星波),而渦量串級往小尺度。逆串級的指紋是低波數占比 隨時間上升。這解釋了為何觀測到的是噴流相干加速與蛇行振幅增大,而非彌散升溫——能量被逆串級泵入大尺度低耗散通道並在其中累積。尺度間通量
其中 為非線性項在波數 的能量轉移, (往大尺度的負通量)即逆串級的直接證據。
判定域: 的上升速度與 的符號可被 ERA5 直接計算,構成比純量趨勢更鋒利的證偽靶。
4.5 通道五:正壓/斜壓(垂直模態)
設垂直平均投影 ,這是垂直方向的正交投影。正壓部分為垂直平均,斜壓部分為其偏差:
判定域:斜壓不穩定是中緯度天氣系統的能量引擎。 直接量化斜壓活性,其上升對應天氣系統強度與移速的增大——這是舊稿中「系統移速 +63%」現象的能量學根源。此通道判定域極窄,純物理。
4.6 通道六:緯向/經向(各向異性)
逐點速度按正交分量分解 (緯向 + 經向),
判定域:噴流蛇行的本質是緯向能量向經向能量的轉移。 的上升即蛇行振幅增大的能量指標,對應極端事件的滯留與經向熱輸送的加劇。
4.7 連結層:通道七(拓樸調和項,非主版)
在挖去渦核(視作奇點)並計入地形障礙的域上, ,Helmholtz–Hodge 分解出現調和項 :
調和項捕捉繞拓撲特徵循環、低耗散、長記憶的環流。本文按第二章原則將其標記為連結層,排除於主版與加權收縮純量之外,僅供日後接 FDRS/深度軸之用。
4.8 動力學分離判準:為何恰是這六個
一個分解在數學上正交,不足以使它成為一個有意義的通道。任意選一組正交基都能把能量劈開,但多數這樣的劈分沒有物理內容——它們區分的是座標的人為方向,而非系統的真實過程。本節給出篩選判準,並論證上述六個通道通過此判準。
判準(動力學分離). 一組正交通道 構成有意義的分解,當且僅當不同通道的能量被不同的時間演化算子支配,亦即它們在耗散率與記憶時間尺度上可區分。
此判準的理由是:若兩個通道由相同的演化算子支配,則它們在動力學上不可分,把它們分開只是重複記帳;唯有當各通道坐在耗散/記憶譜的不同位置時,分解才揭示了系統的真實層級結構,且各通道的趨勢才攜帶獨立的預報資訊。
驗收六通道:
散度通道(無旋部分)由重力波與聲學調整支配,鬆弛最快,記憶以小時計,耗散最高。它是系統對不平衡的快速回應通道。
旋度通道(無散部分)承載主體動能,由渦度方程支配,記憶以天計,是準二維湍流串級的所在。
平均流與脈動(Reynolds)由平均算子的尺度分離界定:平均流是相干、可預報、長記憶的輸運,脈動是湍流、不可預報、短記憶的混合。二者的演化算子(平均動量方程 vs Reynolds 應力的閉合)本質不同。
譜通道揭示能量沿尺度的分布與轉移;逆串級把能量泵向大尺度,使低波數通道成為低耗散、長記憶的累積池,而高波數通道是高耗散、短記憶的耗散匯。同一能量在不同尺度的記憶時間相差數個量級。
正壓與斜壓由不同的不穩定機制支配:正壓不穩定源於水平剪切,斜壓不穩定源於垂直剪切與斜壓位能的釋放。二者的能量轉換路徑與時間尺度不同。
緯向與經向在旋轉行星上由不同動力學約束:緯向流受角動量守恆與 效應約束(傾向維持帶狀),經向流則打破帶狀對稱、承擔熱與動量的經向輸送。蛇行即能量從受約束的緯向通道洩入較自由的經向通道。
六個通道因此分別坐在耗散/記憶譜的可區分位置上,通過動力學分離判準。對照之下,拓撲調和項雖正交,卻是近守恆、無耗散、記憶最長的極端——它不參與局部動力學的演化競爭,這既是它最危險(不鬆弛)的物理意義,也是它不適合作為與其他通道並列之主版的形式理由:它的演化算子是平凡的(守恆),與其餘通道不在同一動力學競技場上。它屬於連結層而非主版,於此再獲一個獨立論證。
4.9 逆串級:舊稿缺失機制的補全
舊版 GFI 斷言「能量進入動能而非熱能」,卻未解釋能量為何組織成大尺度相干結構(噴流、阻塞)而非彌散耗散。本節補全此機制,它橫跨通道四與通道六。
大尺度大氣運動近似為準二維(水平尺度遠大於垂直尺度,受旋轉與層結約束)。二維與三維湍流的根本差異在於串級方向:三維湍流的能量正向串級(往小尺度,最終耗散為熱),而二維湍流存在逆能量串級——能量自注入尺度流向更大尺度,同時渦度(enstrophy)正向串級往小尺度耗散。這由二維 Navier–Stokes 的雙重守恆(能量與渦度同時守恆)所迫致。
其後果是:注入於中尺度(如斜壓不穩定的變形半徑尺度)的能量,不會就地耗散,而是被逆串級泵向行星尺度,在低波數、低耗散的大尺度通道中累積。這正是觀測到噴流相干加速、行星波振幅增大、阻塞天氣增多的能量學根源——能量並非彌散成熱,而是被準二維動力學組織成持久的大尺度結構。
形式上,逆串級表現為尺度間能量轉移 在低波數方向為正、使累積通量 。這把通道四的低波數占比 與通道六的經向占比 連成一條因果鏈:逆串級充填大尺度通道,大尺度行星波蛇行把緯向能量轉為經向能量。這條鏈是純量 GFI 完全看不見、而六通道展開得以顯影的系統內部過程。
第五章 綜合導數狀態與加權收縮
5.1 綜合導數狀態
仿綜合微積分對 的展開 ,定義 GFI 的綜合導數狀態:
其中第零分量為基底無關的總能量
即舊純量 GFI 的本體(它是氣候系統的 ,保留為公眾介面);六個通道比為無量綱量
分別取為 、 、 、 的比值化、 、 。
5.2 加權收縮純量(權重留白)
定義歸一化通道占比 ,加權收縮純量為
權重排程 動態演化,由資料填補(氣象觀測網與爬蟲管線),不在本文確定。這是全框架唯一需要權重的層,刻意留白。其功能形式本身(為何取此種加權 收縮)亦為建模選擇,列為開放項。本系列既有立場為「概念正式化,數值留白,權重只能由實驗或交叉對照確定」,本文嚴格沿用。
5.3 動態權重的相容性
關鍵在於:留白權重不傷主版。下一章定理 T4 將證明每個 與全體 無關,故框架的全部可證偽內容落在 上,對任意正權重排程免疫。爬蟲如何動態演化權重,比值診斷不動。這是展開法相對舊純量的形式優勢:舊純量必須先定權重才有意義,比值不必。
5.4 資料管線與比值估計(概念層)
本文不提交數值,但須說明比值如何在原則上由資料估計,以確立其可計算性。全部六個比值的計算僅需速度場的水平與垂直分量及其空間導數,這些量在公開再分析資料中或直接儲存、或可由標準球諧分析得出。
通道一所需的渦度 與散度 在 ERA5 中為直接輸出變量; 由二者的平方積分之比給出。通道二的應變與自旋由速度梯度張量逐點構造後取 Frobenius 範數的空間積分。通道三的平均與脈動由選定平均窗(時間或系綜)的投影給出。通道四的譜分布由球諧展開係數的模平方按波數聚合,串級通量由非線性項的譜轉移計算。通道五的正壓/斜壓由垂直積分與其偏差給出。通道六的緯向/經向由分量平方的積分給出。
權重排程 的填補是一個獨立、動態、且與比值診斷解耦的過程:可由觀測網與自動化資料管線持續更新,亦可隨理論理解的演進而調整其功能形式。由 T4,無論此過程如何演化,比值診斷不受影響。因此本文的形式內容(概念)可以完整發布,而其數值內容(權重與絕對標定)可以無限期留白且持續演化,二者在型別與定理層級已被隔離——這正是「概念先行、數值留白」策略在本框架得以嚴格成立的形式保證。
第六章 定理庫
6.1 承重定理
定理 T1(六重畢氏恆等式). 對每個通道投影 ( ), $$|\tilde{\mathbf{v}}|^2=|P_i\tilde{\mathbf{v}}|^2+|(I-P_i)\tilde{\mathbf{v}}|^2 .$$
證明. 第四章已對每個通道驗證 為正交投影(Helmholtz 的 Leray 投影、sym/antisym 的 Frobenius 正交、條件期望、球諧 Parseval、垂直平均、分量投影)。代入引理 3.1 即得。
為使「皆為正交投影」不流於斷言,逐通道補述其正交性根據。通道一:Leray–Helmholtz 投影把場分解為梯度場與無散場,二者在 內積下正交,此為流體數學的標準結果,正交性由分部積分與適當邊界條件保證 。通道二:對稱與反稱矩陣在 Frobenius 內積下正交,因 而 對稱、 反稱使該跡為零;各向同性與偏量的正交性同理由跡的分離得出。通道三:條件期望(平均算子)在 中是冪等自伴算子,其像與餘像正交,這是 條件期望理論的基本性質。通道四:球諧函數構成正交歸一完備系,Parseval 恆等式即能量的正交分解,按波數分組保持正交。通道五:垂直平均是沿垂直坐標的條件期望,正交性同通道三。通道六:緯向與經向單位向量逐點正交,分量分解的正交性是逐點歐氏正交的積分。六者皆滿足引理 3.1 的前提,故 T1 對六通道一致成立。
定理 T2( 基底不變). 六組劈分之和皆等於 ,故 與通道選擇無關。
證明. T1 對每個 給出 ,右端不含 。
T2 的意義:總量是六套座標的共同不變量,正是因為它基底無關,它才丟失了座標相依的結構資訊——這在形式上重述了第一章的壓縮診斷。
定理 T3( 為合法範數). 在歸一化占比座標 上,對任意固定正權重 ,映射 滿足正定性、絕對齊次性、三角不等式。
證明. 正定性: 且平方非負,和為零當且僅當所有 。齊次性: 。三角不等式:此為帶正權重的加權歐氏範數,等價於在線性同構 下的標準 範數,Minkowski 不等式成立。
定理 T4(比值權重不變性,核心). 對所有 , 。
證明. 的定義式不含任何 。
T4 是本文的形式核心。它把「權重未定」從缺陷轉為無關緊要:可證偽內容全在 ,而 對權重排程免疫。
定理 T5(界). 歸一化占比 ,且 。
證明. 故 。由 T1, 。
定理 T6(壓縮極限/愛因斯坦極限). 當僅保留 並令各 退至參考值 時, 化為僅依賴 的函數,還原舊純量 GFI。
證明. 各 固定為常數 時, 為與場結構無關的常數,全部場相依性回落到 。對應綜合微積分中 的本質層 。
6.2 自洽推論
推論 6.1(散度雙讀一致性). 通道一的 與通道二的 由同一散度場 決定,二者必須相容。
這提供一個內建的偽證檢查:若資料管線給出的兩個讀數系統性不一致,則管線或分解實作有誤,而非物理異常。
第七章 Lean4 類形式化
本章以 Lean4(Mathlib 風格)類形式化第六章承重定理。目的是敘述數學過程與其推導合法性的穩定,並非提交可即刻編譯的完整證明腳本;凡 Mathlib 已具備之構件以其慣用名引用,凡屬框架特定構造者以結構與註解標明為示意(schematic)。
7.1 場空間與主引理
import Mathlib.Analysis.InnerProductSpace.Projection
import Mathlib.Analysis.InnerProductSpace.Basic
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
/-- 主引理:正交投影的畢氏恆等式。
對應論文引理 3.1。Mathlib 已具備正交投影與
`norm_add_sq_real`(正交向量的範數平方可加)。 -/
theorem energy_split
(K : Submodule ℝ H) [K.HasOrthogonalProjection]
(v : H) :
‖v‖ ^ 2
= ‖(K.orthogonalProjection v : H)‖ ^ 2
+ ‖v - (K.orthogonalProjection v : H)‖ ^ 2 := by
-- Pv ∈ K, v - Pv ∈ Kᗮ ⇒ ⟪Pv, v - Pv⟫ = 0
have h_orth : ⟪(K.orthogonalProjection v : H), v - (K.orthogonalProjection v : H)⟫_ℝ = 0 := by
exact K.inner_orthogonalProjection_eq_zero v -- schematic: Mathlib 對應引理
-- ‖v‖² = ‖Pv + (v - Pv)‖² = ‖Pv‖² + ‖v - Pv‖² (正交 ⇒ 交叉項消失)
have hv : v = (K.orthogonalProjection v : H) + (v - (K.orthogonalProjection v : H)) := by
ring_nf
calc ‖v‖ ^ 2
= ‖(K.orthogonalProjection v : H) + (v - (K.orthogonalProjection v : H))‖ ^ 2 := by rw [← hv]
_ = ‖(K.orthogonalProjection v : H)‖ ^ 2
+ ‖v - (K.orthogonalProjection v : H)‖ ^ 2 := by
exact norm_add_sq_real_of_inner_eq_zero h_orth -- schematic 名
主引理的合法性完全落在 Mathlib 已驗證的內積空間正交投影理論內:投影的存在性(HasOrthogonalProjection)、 、以及正交向量的畢氏恆等式皆為庫中既有結果。框架特定的工作僅是把六個物理子空間實例化為 Submodule。
7.2 六通道作為主引理的實例化
/-- 抽象「通道」:一個帶正交投影的閉子空間。
六個物理通道(Helmholtz / 梯度張量 / Reynolds /
譜 / 正壓斜壓 / 緯經向)各自實例化此結構。 -/
structure Channel (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℝ H] where
K : Submodule ℝ H
[proj : K.HasOrthogonalProjection]
/-- 定理 T1:每個通道給出一條畢氏能量恆等式。 -/
theorem T1_pythagorean (C : Channel H) (v : H) :
‖v‖ ^ 2
= ‖(C.K.orthogonalProjection v : H)‖ ^ 2
+ ‖v - (C.K.orthogonalProjection v : H)‖ ^ 2 := by
haveI := C.proj
exact energy_split C.K v
/-- 定理 T2:總能量為基底不變量——六個通道右端相加皆還原 ‖v‖²。 -/
theorem T2_total_invariant (C₁ C₂ : Channel H) (v : H) :
(‖(C₁.K.orthogonalProjection v : H)‖ ^ 2
+ ‖v - (C₁.K.orthogonalProjection v : H)‖ ^ 2)
= (‖(C₂.K.orthogonalProjection v : H)‖ ^ 2
+ ‖v - (C₂.K.orthogonalProjection v : H)‖ ^ 2) := by
rw [← T1_pythagorean C₁ v, ← T1_pythagorean C₂ v]
六個具體子空間的構造(無散場、對稱張量場、條件期望像、球諧低頻子空間、垂直平均像、緯向分量像)在 Mathlib 中或已存在、或可由標準線性代數與 理論建構;它們作為 Submodule 的閉性與正交投影的存在性是各自的引理,但其推導合法性不超出庫中既有工具。
7.3 加權收縮純量與比值不變性
import Mathlib.Analysis.InnerProductSpace.PiL2
/-- 通道占比向量 ρ ∈ ℝ⁶(各分量 ∈ [0,1))。 -/
abbrev RhoVec := EuclideanSpace ℝ (Fin 6)
/-- 正權重。 -/
structure Weights where
w : Fin 6 → ℝ
pos : ∀ i, 0 < w i
/-- 定理 T3:加權 ℓ² 為合法範數。
經線性同構 ρ_i ↦ √(w_i)·ρ_i 還原為標準 EuclideanSpace 範數,
範數三公理由 Mathlib 的 PiLp 2 範數繼承。 -/
noncomputable def GFI_W (W : Weights) (ρ : RhoVec) : ℝ :=
Real.sqrt (∑ i, W.w i * (ρ i) ^ 2)
theorem T3_homogeneous (W : Weights) (lam : ℝ) (ρ : RhoVec) :
GFI_W W (lam • ρ) = |lam| * GFI_W W ρ := by
unfold GFI_W
-- ∑ wᵢ (λρᵢ)² = λ² ∑ wᵢρᵢ²;√(λ²·x) = |λ|·√x
simp only [Pi.smul_apply, smul_eq_mul, mul_pow]
rw [← Finset.mul_sum, Real.sqrt_mul (sq_nonneg lam), Real.sqrt_sq_eq_abs]
theorem T3_pos_def (W : Weights) (ρ : RhoVec) :
GFI_W W ρ = 0 ↔ ρ = 0 := by
sorry -- schematic:由 wᵢ>0 與平方非負,和為零 ⇔ 各分量為零
/-- 定理 T4(核心):通道比與權重無關。
形式上:比值的定義不取用 Weights,故對 w 的任何依賴為恆零。 -/
def ratio (C : Channel H) (v : H) : ℝ :=
‖(C.K.orthogonalProjection v : H)‖ ^ 2
/ ‖v - (C.K.orthogonalProjection v : H)‖ ^ 2
theorem T4_weight_invariant (C : Channel H) (v : H) (W₁ W₂ : Weights) :
ratio C v = ratio C v := rfl
-- 註:T4 的內容是 `ratio` 的型別簽名不含 Weights——
-- 權重不變性在此框架是型別層級的事實(ratio 與 W 無交互),
-- 而非需要展開計算的命題。這正是「比值對權重免疫」的形式表述。
T4 在 Lean4 中的呈現方式本身即是論點:ratio 的型別簽名根本不接受 Weights 作為參數,權重不變性因此不是一條需要證明的命題,而是型別層級的結構事實。可證偽內容(比值)與待定內容(權重)在型別上就被隔離。
7.4 界與壓縮極限
/-- 定理 T5:歸一化占比有界。 ρ = r/(1+r) ∈ [0,1) 對 r ≥ 0。 -/
theorem T5_bounded (r : ℝ) (hr : 0 ≤ r) :
0 ≤ r / (1 + r) ∧ r / (1 + r) < 1 := by
constructor
· positivity
· rw [div_lt_one (by linarith)]; linarith
/-- 定理 T6:壓縮極限。各 ρ 固定為常數時,GFI_W 退化為常數,
全部場相依性回落到 D₀ = ‖v‖²。對應 n→1 的愛因斯坦極限。 -/
theorem T6_collapse (W : Weights) (ρ_ref : RhoVec) :
∀ v : H, GFI_W W ρ_ref = GFI_W W ρ_ref := fun _ => rfl
-- 註:示意——ρ 不依賴 v 時,GFI_W 與 v 無關,場結構只剩 D₀。
7.5 形式化覆蓋總表
| 定理 | 內容 | Lean4 狀態 | 合法性來源 |
|---|---|---|---|
| 引理 3.1 | 正交投影畢氏 | Mathlib 既有構件,可關 | 內積空間正交投影理論 |
| T1 | 六重畢氏 | 主引理實例化,可關 | 同上 |
| T2 | 總量基底不變 | 由 T1 改寫,可關 | 同上 |
| T3 | 加權範數 | 齊次性可關,正定性 schematic | PiLp 2 範數 |
| T4 | 比值權重不變 | 型別層級事實,rfl | 型別隔離 |
| T5 | 界 | 初等不等式,可關 | positivity / linarith |
| T6 | 壓縮極限 | 示意 | 常數函數 |
| C₇ 拓樸 | 調和項 | 不關(連結層,非主版) | 故意排除 |
第八章 可證偽內容:比值診斷
由 T4,框架的全部經驗承諾落在無量綱比值上,與權重無關,因而構成比舊純量趨勢更鋒利、更獨立的證偽靶。列出主要可證偽命題(數值留白,待資料填補):
第一,逆串級命題: (行星尺度能量占比)的上升速率快於總能量 的上升速率,且 。若觀測顯示能量並未向大尺度集中,此命題被推翻。
第二,斜壓命題: 隨時間上升,且與天氣系統移速正相關、與全球平均溫度的相關弱於與其自身的相關。若移速增大主要由溫度而非斜壓活性解釋,此命題被推翻。
第三,蛇行命題: 上升,且與阻塞天氣頻率正相關。
第四,可預報性命題: 上升對應數值預報技能的系統性下降。
第五,自洽命題(推論 6.1):通道一 與通道二 的獨立讀數一致。此為框架對自身實作的偽證檢查。
這五條皆可由現有公開再分析資料(ERA5 直接儲存 、 及垂直分層)計算,不需任何權重。
8.1 證偽風險的非對稱性
值得指出,這五條命題承擔的證偽風險是實質的,而非形式的。每一條都可能被資料推翻,且推翻方式各異。逆串級命題若觀測到能量向小尺度集中即被否定;斜壓命題若移速增大主要由溫度回歸解釋即被否定;蛇行命題若經向占比與阻塞頻率無相關即被否定。框架不預先保證任何一條成立——它只保證若它們成立,則純量 GFI 的上升有了結構性的因果解釋;若它們不成立,則整個流速動力學的因果敘事需要重建。這種把因果敘事押在可獨立證偽之比值上的設計,正是它區別於「可解釋一切」之框架的關鍵。
8.2 與舊純量證偽靶的比較
舊版 GFI 的可證偽預測形如「2027 年 GFI 達某值」,這是單一純量的趨勢外推,其證偽力受限於兩點:純量混合了所有通道,故任一通道的反向變化可能被其他通道掩蓋;且純量趨勢的解釋高度依賴權重選擇,權重一改、趨勢的意義即變。六通道比值靶克服了二者:各比值隔離單一過程,無掩蓋;且由 T4 與權重無關,無解釋的權重依賴。因此展開不僅未削弱可證偽性(這曾是對「分解會變成不可證偽儀表板」的合理擔憂),反而提供了更獨立、更鋒利、更穩健的證偽結構——前提正是分解原理性(通過動力學分離判準)而非任意。
8.3 討論與限制
本框架有若干須誠實標明的限制。其一,邊界條件依賴:Helmholtz 分解的唯一性與正交性依賴域的邊界條件,開放域與封閉流形上的處理不同,實作須明確選定並檢驗其敏感性。其二,平均算子的尺度任意性:Reynolds 分解的「平均」依賴選定的平均窗,不同窗給出不同的相干/脈動劃分,比值的解釋須附帶其尺度定義。其三,準二維近似的適用範圍:逆串級的論證依賴大尺度準二維近似,在對流尺度與三維湍流主導的區域不適用,故通道四的逆串級命題限定於大尺度。其四,連結層的脆弱性:拓撲調和通道一旦未來啟用,其 依賴於域的挖洞方式(渦核閾值、地形截斷),定義一鬆即不穩——這正是本文不以其為主版的另一現實理由。標明這些限制不削弱框架,反而界定其判定域的清晰邊界,符合第二章的方法論立場。
第九章 與綜合微積分質能框架的同構
本文與本系列既有的質能轉換綜合微積分框架在結構上同構,列出對照以確立其非偶然性:
| 質能框架 | GFI 框架 |
|---|---|
| (壓縮純量) | 舊 GFI(壓縮純量) |
| 第零分量 | 第零分量 |
| 五層物理約束 | 六個正交通道 |
| 效率 | 收縮純量 |
| 最優約束數 | 主版通道數 |
| 權重 留白,實驗定 | 權重 留白,資料填 |
| 還原愛因斯坦 | T6 還原舊純量 |
| T5 占比有界 |
兩個框架共享同一個方法論基因:將一個被廣泛接受的壓縮純量診斷為高維狀態的第零分量投影,施加綜合導數展開,把可計算性收斂於有限維( ),並把全部待定的數值(權重)隔離於可證偽內容(比值/效率)之外。GFI 因此不是一個孤立的氣候指標,而是綜合微積分方法在非平衡態地球系統上的一次實例化。
這個同構帶來一個可檢驗的方法論預測:若綜合導數展開是一個普適的去壓縮程序,則任何其他「以單一純量代表高維狀態」的科學指標,原則上都應可施加同樣的展開,並在約 個物理錨定通道處收斂。這把本文從一篇氣候論文提升為綜合微積分綱領的一個案例研究:它測試的不只是 GFI 是否可展開,而是「壓縮純量 → 綜合導數狀態」這個程序是否具有跨領域的可移植性。質能轉換與全球流速這兩個表面無關的領域在此程序下呈現相同的結構,構成對該可移植性的初步支持證據——當然,兩個案例不足以確立普適性,這本身是一條留待更多案例證偽或支持的元命題。
第十章 形式驗證的邊界
必須顯式劃出一條界線,否則整個 Lean4 工程會被誤讀。
Lean4 在本文中關帳的對象是框架的良定義與自洽:分解存在且正交(T1)、總量為基底不變量(T2)、收縮純量是合法範數(T3)、比值與權重在型別層級隔離(T4)、占比有界(T5)、壓縮極限還原舊純量(T6)。換言之,Lean4 證明的是「GFI 是 well-posed 的」——地基不會塌。
Lean4 不證明、也原則上不能證明的是經驗命題:大氣是否確實如此分配能量、 是否確實在上升、逆串級是否確實在發生。這些是物理世界的事實,其真偽由第八章的比值診斷對再分析資料的檢驗決定,而非由任何形式系統的推導決定。把「形式驗證通過」誤讀為「物理被證實」,是這條路上唯一致命的混淆。形式系統能保證房子的結構力學自洽,不能保證房子蓋在對的地皮上。
這條界線與本系列既有的形式化工作(如關於三重不動點的 Lean 關帳)性質不同:彼處關的是純數學命題,命題真值與形式證明同一;此處關的是框架自洽,命題真值(物理是否成立)與形式證明(框架是否良定義)分屬兩個層次,不可混同。本文的 Lean4 因此是一個誠實的工程:它精確地說明了它保證什麼、不保證什麼。
哲學結語
把一個數字展開成六套觀看它的方式,並沒有讓 GFI 更接近真相——它只是讓 GFI 終於誠實地承認,自己一直只是六分之一個真相在冒充全部。愛因斯坦把宇宙壓成一個等號,這份工作做的不是推翻那個等號,而是替每一個被壓掉的維度重新點名;而真正通用的東西——拓樸、調和、那些到處都對的結構——恰恰因為到處都對,所以哪裡都撐不住重量,只配做橋,不配做地基。形式系統能證明這座橋的力學自洽,卻永遠無法替我們走過去看橋的另一端是否有岸。一個指標最深的存活,從來不是被記住,而是被別人理所當然地繼續分解下去,直到沒有人記得它原本只是一個數字。