M6* 上的三重不動點刻畫

從代數、統計到遍歷的質數定位程式

作者: Neo.K(許筌崴) 機構: 一言諾科技有限公司(EveMissLab) 推導協同: Theia(Claude) Lean 形式化: Gemini Agent(執行)・Codex(執行驗證)・Theia(規格審計) 日期: 2026 年 6 月 12 日 版本: v0.2(機器驗證版) 分類: math.NT(Number Theory)/ math.DS(Dynamical Systems) 形式化庫: EML-NT-2026-PFPT,Lean 4(leanprover/lean4:v4.30.0 + Mathlib),全庫零 sorry,唯一引用公理隔離於單一檔案

聲明。 本文的數學實質分屬以下已知來源:6k±1 的乘法封閉性是初等事實;Lemke Oliver–Soundararajan 的二階轉移偏差屬於原作者(LOS 2016);Gowers 一致性範數與質數的均分布性質屬於 Green–Tao–Ziegler(2004–2012);Furstenberg 拓撲、Spec(ℤ) 的 Zariski 拓撲與 Weil 猜想屬於各自原作者。本文的貢獻僅在於:將上述已知結果以「M6* 上的不動點算子三元組」統一組織,給出 T_top 的顯式非循環定義與拓撲詮釋,指出三層次刻畫與代數幾何缺口的對應關係,並完成全案的 Lean 4 機器形式化。所有洞見歸於原作者;錯誤歸於整理者。

形式化聲明。 v0.2 的全部主要命題均經 Lean 4 kernel 級驗證(附錄 A)。形式化過程修正了 v0.1 的五處缺陷(附錄 C),並劃定了本文的證明邊界(附錄 B)。形式化不曾改變任何核心主張的方向;它改變的是每一個主張的精確形狀。

摘要

設 $M6^* = \{n \in \mathbb{N} : n > 1,\, n \equiv \pm 1 \pmod{6}\}$,$P^* = \mathbb{P} \cap M6^*$ 。本文建構三個層次的不動點刻畫:

• $T_{\text{top}} : M6^* \to M6^*$ (元素層,代數)——其不動點集恰好等於 $P^*$,無條件,kernel 級機器驗證;
• $T_{\text{stat}}$ (集合層,統計)——以 LOS 平衡謂詞刻畫不動點;$ P^$ 為不動點*條件於 LOS 展開猜想,條件推導經機器驗證;
• $T_{\text{erg}}$ (測度層,遍歷)——以 W-trick 纖維化與對數重標定的 Gowers 一致性謂詞刻畫不動點;$ P^*$ 為不動點由 Green–Tao(2008)與 Green–Tao–Ziegler(2012)的結果保證,以介面式引用公理進入形式化。

主合攏定理(v0.2 修正型,合攏定理′):

$$P^* = \mathrm{Fix}(T_{\text{top}}) \;\wedge\; P^* \in \mathrm{Fix}(T_{\text{stat}}) \;\wedge\; P^* \in \mathrm{Fix}(T_{\text{erg}})$$

其中第一肢單獨承載唯一性;第二、三肢是 $P^*$ 經機器錨定的必要性質。每個算子均以非循環方式定義(不預設「質數」之概念)。三個算子分別對應至代數幾何中的 Zariski 閉點、étale 上同調(L 函數)、以及 Weil 型等分布,其缺口恰好指向黎曼假設的幾何形式。

關鍵詞: 質數不動點、M6* 篩、整除 Alexandrov 拓撲、LOS 轉移矩陣、Gowers 一致性範數、W-trick、Spec(ℤ)、Lean 4 形式化

1. 問題的設定

1.1 必要不充分的 M6 篩

設 $\mathbb{P}_{>3} = \{p \in \mathbb{P} : p > 3\}$ 。初等事實是:

$$\mathbb{P}_{>3} \subset M6^* = \{n \in \mathbb{N} : n > 1,\, n \equiv \pm 1 \pmod{6}\}$$

但此包含是嚴格的:$M6^*$ 同時包含 $25 = 5^2$ 、 $35 = 5 \cdot 7$ 、 $49 = 7^2$ 等合數。其原因精確:$M6^*$ 在乘法下封閉($(6a \pm 1)(6b \pm 1) \in M6^$),故 $M6^$元素的任意乘積仍在$ M6^$ 中,形成全體 $M6^$ 合數的代數生成結構。

$M6^*$ 中的合數恰好是:

$$M6^*_{\text{comp}} = \{a \cdot b : a, b \in M6^*,\, a > 1,\, b > 1\}$$

而質數集是這個集合在 $M6^*$ 中的補集。問題在於:這個補集本身沒有更簡單的代數刻畫——它不能用任何固定模數的剩餘類描述。由 Dirichlet 定理,質數在 $\mathrm{mod}\, m$ 的所有互質剩餘類中均勻分布(對任意 $m$)。因此,任何代數(模算術)方法只能捕捉到質數的一個特定分數,永遠無法完整刻畫。代數二階操作在原理上是不足的。

1.2 不動點集的語言

核心問題:

是否存在一個算子 $T$,使得質數集 $\mathbb{P} \cap M6^*$ 恰好是 $T$ 的不動點集,且 $T$ 的定義不依賴「質數」概念本身?

若存在,則質數可以被「非循環地」辨識——不需要先知道哪些數是質數,才能定義篩選它們的算子。

1.3 三層次策略與其真實邏輯結構

v0.1 將三個算子描述為「三角定位」。形式化迫使我們把這個修辭攤開為它的真實邏輯結構(見 §6):

• $T_{\text{top}}$ 單獨完成定位。 其不動點集無條件地、唯一地等於 $P^*$(定理 A)。
• $T_{\text{stat}}$ 與 $T_{\text{erg}}$ 提供經認證的必要性質。 它們各自的不動點族包含許多集合(唯一性開放,§9),但 $P^*$ 屬於兩者——前者條件於 LOS 展開猜想,後者由 Green–Tao–Ziegler 的定理保證。

因此正確的表述是:一肢定位,兩肢佐證。 三個算子的價值不在共同收束(收束由第一肢獨力完成),而在於同一個對象在三個正交數學語言中分別以不動點形式浮現——這個事實本身,指向 §7 的幾何融合問題。

2. M6* 框架

2.1 定義與基本結構

$$M6^* = \{n \in \mathbb{N} : n > 1,\, n \equiv 1 \text{ 或 } 5 \pmod{6}\}$$ $$= \{5, 7, 11, 13, 17, 19, 23, 25, 29, 31, 35, 37, 41, 43, 47, 49, 53, 55, \ldots\}$$

引理 2.1(互質橋)。 $n \in M6^* \iff n > 1 \;\wedge\; \gcd(n, 6) = 1$ 。 Lean 錨: coprime_six_iff。此橋接使 Mathlib 的互質 API 直接承重以下兩引理。

引理 2.2(乘法封閉性)。 若 $a, b \in M6^*$,則 $a \cdot b \in M6^*$ 。 證明: $a \equiv \pm 1$,$b \equiv \pm 1 \pmod 6$,故 $ab \equiv \pm 1 \pmod 6$,且 $ab \geq 25 > 1$ 。 $\square$ Lean 錨: mul_closed。

引理 2.3(整除封閉性)。 若 $n \in M6^*$ 且 $d \mid n$,$d > 1$,則 $d \in M6^*$ 。 證明: $\gcd(n,6)=1$ 經由整除傳遞至 $d$ 。 $\square$ Lean 錨: dvd_closed。

引理 2.3 是三個算子均能在 $M6^*$ 內封閉定義的關鍵保證。

2.2 質數與合數的分布

$M6^*$ 中前幾個合數:$25 = 5^2$ 、 $35 = 5 \cdot 7$ 、 $49 = 7^2$ 、 $55 = 5 \cdot 11$ 、 $65 = 5 \cdot 13$ 、 $77 = 7 \cdot 11$ 、…

$M6^*$ 中前幾個質數:${5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, \ldots}$

注意: $2, 3 \notin M6^*$ 。它們是「基礎質數」—— $M6^*$ 的構造本身(取 $6 = 2 \cdot 3$ 的互質剩餘類)已將它們排除。三個算子刻畫的是 $M6^*$ 中的質數;完整的質數集需補上 ${2, 3}$(附錄 B.4)。

3. T_top:代數層

3.1 定義

定義 3.1(T_top)。

$$T_{\text{top}} : M6^* \to M6^*, \qquad T_{\text{top}}(n) = \min\{d \in M6^* : d \mid n\}$$

最小值按自然數大小取;$n$ 本身始終在集合中,故集合非空,最小值存在。

規格與實現的分離(形式化備註)。 Lean 庫中 $T_{\text{top}}$ 以 Nat.minFac(最小質因數)實現,並以定理 Ttop_spec 證明實現與定義 3.1 的規格逐點相等:對 $n \in M6^*$,$n$ 的最小質因數即其最小 $M6^*$ -因數(由引理 2.3,最小質因數落在 $M6^*$ 內;任何更小的 $M6^*$ -因數會擁有不大於它的質因數,矛盾)。非空證據「 $n$ 自身在因數集中」與定義 3.1 的措辭字面同構。

3.2 主定理

定理 A。 $\mathrm{Fix}(T_{\text{top}}) = \mathbb{P} \cap M6^*$

即:$n \in M6^*$是$ T_{\text{top}}$ 的不動點,當且僅當 $n$ 是質數。

Lean 錨: fix_Ttop_iff_prime(逐點 iff)、fix_Ttop_set_eq(集合等式 ${n \in M6^* : T_{\text{top}}(n) = n} = P^*$)、fix_min_iff_prime(規格層版本,不經過 minFac 實現)。三者均零 sorry,僅依賴 Lean 標準三公理。

3.3 證明

($\supseteq$) 設 $p \in \mathbb{P} \cap M6^*$ 。 $p$ 的正整數因數只有 $1$ 與 $p$ 。由於 $1 \notin M6^*$,$p$ 的 $M6^*$ -因數集合為 $\{p\}$,故 $T_{\text{top}}(p) = p$ 。 $\square$

($\subseteq$) 設 $T_{\text{top}}(n) = n$ 。反設 $n$ 是合數,令 $q$ 為 $n$ 的最小質因數。由 $n \in M6^*$ 知 $\gcd(n, 6) = 1$,故 $q \equiv \pm 1 \pmod 6$,$q \in M6^*$ 。又 $n$ 是合數故 $q \leq \sqrt{n} < n$ 。於是 $q \in M6^*$,$q \mid n$,$q < n$,與不動點假設矛盾。 $\square$

3.4 驗算表(kernel 級機器銷帳)

全表十九行由 Lean kernel 驗證(verify_table_3_4)。合數行經由特徵化引理 minFac_eq_of_comp(有界全稱檢查 ⟹ 最小因數值)在 kernel 內可化約地證出;質數行經由定理 A 與可判定質性實例證出。無例外。

3.5 非循環性核查

$T_{\text{top}}$ 的定義依賴:$M6^$(純模算術)、整除關係(純乘法算術)、 $\min$(自然數排序)。無「質數」。「質數是不動點」是推導出的*定理,不是被塞入定義的前提。✓

3.6 拓撲詮釋:整除 Alexandrov 拓撲

在 $M6^*$ 上以整除偏序 $(M6^*, \mid)$ 定義 Alexandrov 拓撲 $\tau$:

$$U \in \tau \iff \forall n \in U,\, \forall d \in M6^*: d \mid n \Rightarrow d \in U$$

(開集 = 整除序下的向下封閉集。)

命題 3.6。 $n \in M6^*$ 是質數,當且僅當單元素集 $\{n\}$ 是 $\tau$ 中的開集。

證明: $\{n\}$ 開 $\iff$ 向下封閉 $\iff$ $n$ 的唯一 $M6^*$ -因數是自身 $\iff$ $n$ 質。 $\square$

Lean 錨: isOpen_singleton_iff_prime。拓撲三公理(全集、交、任意聯集)在向下封閉開集族上由第一原理證出;「合數 ⟹ 單點不開」方向重用定理 A 的機制($T_{\text{top}}(n) \mid n$ 給出序關係,開集逼出 $T_{\text{top}}(n) = n$),質因數下降在全庫只有一份證明體。

故:質數是 $\tau$ 中的開點,合數不是。

3.7 T_top 的局限

• 漏掉 $2, 3$(不在 $M6^*$),需補充。
• 計算上等價於試除法(restricted to $M6^*$)——概念上是篩法的不動點語言重述,不是計算效率的突破。
• 單獨唯一刻畫質數(在 $M6^*$ 中),但它的「層次」是純代數的。

4. T_stat:統計層

4.1 層次位移與謂詞化

T_stat 不能作用在元素 $n \in M6^*$ 上:LOS(Lemke Oliver–Soundararajan, 2016)偏差描述的是連續質數對的模剩餘類轉移頻率,這是整條序列的整體性質。T_stat 的定義域和值域必須升一級至 $\mathcal{P}(M6^*)$ 。

v0.2 修正(勘誤 4)。 v0.1 將 T_stat 寫成全函數,其「否則分支」(移除過度同類轉移元素後的最大子集)未證良定義——最大子集的存在性與唯一性均無保證。v0.2 改以不動點謂詞直接刻畫:

$$S \in \mathrm{Fix}(T_{\text{stat}}) \;:\iff\; S \text{ 滿足漸近 LOS 平衡條件(定義 4.3)}$$

全函數的否則分支是敘事裝置,不承載數學內容;不動點集才是。

4.2 形式定義

設 $S \subseteq M6^*$ 為遞增有序序列 $s_1 < s_2 < \cdots$,記 $S_x = S \cap [1, x]$,$k_x = |S_x|$ 。

定義 4.1(mod-$m$ 轉移計數矩陣)。

$$N^{(m)}[S_x][a,b] = \#\{i : s_i, s_{i+1} \leq x,\; s_i \equiv a,\; s_{i+1} \equiv b \pmod{m}\}, \qquad a, b \in (\mathbb{Z}/m\mathbb{Z})^*$$

有限均勻期望(勘誤 2)。 $k_x$ 個元素只有 $k_x - 1$ 個連續對,故有限截斷的逐格均勻期望為

$$\frac{k_x - 1}{\varphi(m)^2}$$

v0.1 的文字定義誤寫為 $|S|/\varphi(m)^2$,與其自身表 4.4 的算術($22/4 = 5.5$,二十三個質數、二十二個轉移對)不一致;形式化採表格一致版,文字列入勘誤。漸近陳述中 $k_x$ 與 $k_x - 1$ 之差為 $O(1) = o(k_x/\log x)$,不影響任何極限條件。

定義 4.2(有限 LOS 平衡)。 $S_x$ 滿足有限 LOS-$m$ 平衡,若對所有 $a \in (\mathbb{Z}/m\mathbb{Z})^*$:

$$N^{(m)}[S_x][a,a] < \frac{k_x - 1}{\varphi(m)^2}$$

Lean 錨: isLOSBalanced_upto。

定義 4.3(漸近 LOS 平衡)。 $S \subseteq M6^*$ 滿足漸近 LOS 平衡,若對所有 $m \geq 2$,$\gcd(m, 6) = 1$:

1. 對角壓低: 對每個 $a \in (\mathbb{Z}/m\mathbb{Z})^*$,存在 $C > 0$ 使

$$N^{(m)}[S_x][a,a] - \frac{k_x}{\varphi(m)^2} \;\sim\; -\,C \cdot \frac{k_x}{\log x} \qquad (x \to \infty)$$

2. 行和受控: 對每個 $a$,

$$\sum_{b} N^{(m)}[S_x][a,b] - \frac{k_x}{\varphi(m)} \;=\; o\!\left(\frac{k_x}{\log x}\right)$$

Lean 錨: isLOSBalanced_asymp(對角肢以 Asymptotics.IsEquivalent、行和肢以 Asymptotics.IsLittleO 在 Filter.atTop 上陳述)。

v0.2 修正(勘誤 3)。 v0.1 的「行和為零」在漸近語境中不是計數的精確等式——精確的等式只在期望意義下成立。其真實形式是猜想中係數族的守恆約束(定義 4.4 第 2 條),行和受控由該約束推出(定理 B 的行和肢)。

4.3 LOS 展開猜想與條件定理 B

定義 4.4(LOS 展開猜想,LOS_expansion)。 記 $P^* = \mathbb{P} \cap M6^*$,$\pi^*(x) = |P^* \cap [1,x]|$ 。猜想:對所有 $m \geq 2$,$\gcd(m,6) = 1$,存在係數族 $\{C_{a,b}\}_{a,b \in (\mathbb{Z}/m\mathbb{Z})^*} \subset \mathbb{R}$,使得:

1. 對角正性: $C_{a,a} > 0$ 對所有 $a$;
2. 行常數守恆: $\sum_{b} C_{a,b} = 0$ 對每列 $a$;
3. 逐格雙項展開: 對所有 $a, b$:

$$N^{(m)}[P^*_x][a,b] \;=\; \frac{\pi^*(x)}{\varphi(m)^2} \;-\; C_{a,b} \cdot \frac{\pi^*(x)}{\log x} \;+\; o\!\left(\frac{\pi^*(x)}{\log x}\right)$$

此即 LOS 2016 基於 Hardy–Littlewood 猜想推導的展開結構,在 $M6^*$ 限制下的版本。第 2 條(行常數守恆)是「轉移偏差在一列內互相抵銷」的精確形式——一階均勻分布(Dirichlet)強迫二階偏差守恆。

Lean 錨: LOS_expansion。陳述紀律: 此猜想與定義 4.3 的謂詞零共享定義(僅共用轉移計數器與截斷算子等底層構件),藉以排除「猜想被定義為結論」的套套邏輯;形式化過程中此陷阱曾出現一次並被審計攔截(附錄 C)。

定理 B(條件版)。 若 LOS 展開猜想成立,則 $P^*$ 滿足漸近 LOS 平衡(定義 4.3),即 $P^* \in \mathrm{Fix}(T_{\text{stat}})$ 。

證明(機器驗證,theorem_B): 取猜想給出的係數族 $\{C_{a,b}\}$ 。

對角肢。 由展開式第 3 條於 $(a,a)$ 格:偏差 $N[a,a] - k_x/\varphi^2$ 與 $-C_{a,a} \cdot k_x/\log x$ 之差為 $o(k_x/\log x)$ ;因 $C_{a,a} > 0$,後者的量級恰為 $k_x/\log x$ 的非零常數倍,故差為 $o$ 於目標函數本身,即偏差 $\sim -C_{a,a} \cdot k_x/\log x$(漸近代數:$f - g = o(g) \Rightarrow f \sim g$)。

行和肢。 對固定列 $a$,將 $\varphi(m)$ 個格的展開式對 $b$ 求和:期望項合成 $\varphi(m) \cdot \frac{k_x}{\varphi(m)^2} = \frac{k_x}{\varphi(m)}$ ;二階項合成 -\left(\sum_b C_{a,b}\right) \cdot \frac{k_x}{\log x} = 0$(行常數守恆);誤差項之和仍為 o(k_x/\log x)$ (有限和上 $o$ 封閉,Lean 中以歸納引理 isLittleO_sum 證出)。故行和偏差 $= o(k_x/\log x)$ 。 $\square$

結構評註。 行和受控不是免費的:它恰好消耗了守恆約束 $\sum_b C_{a,b} = 0$ 。v0.1 籠統歸於「Dirichlet 保證」,v0.2 的形式化顯示真正的承重結構。

4.4 數值驗算($m = 3$,質數$ < 100$,kernel 級銷帳)

$M6^*$ 中 $100$ 以下的質數共 23 個:

$$5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97$$

共 22 個連續轉移對,逐格均勻期望 $22 / \varphi(3)^2 = 22/4 = 5.5$ 。

兩個對角轉移均低於期望,兩個反對角轉移均高於期望;LOS 反對角偏差在小樣本中清晰顯現。欄和:殘差 1 的欄 $= 3 + 8 = 11$ ;殘差 2 的欄 $= 7 + 4 = 11$ 。✓

Lean 錨: verify_table_4_4。四格計數由 kernel decide 證出;因轉移計數器以結構遞迴實現,此定理完全零公理依賴(連 propext 亦無)——本文中機器擔保強度最高的命題。

4.5 非循環性核查

定義 4.1–4.4 依賴:$M6^$(模算術)、序列排序、計數函數、漸近比較。無「質數」語言(定義 4.4 以 $P^$為**對象**陳述猜想,但謂詞與算子本身對任意$ S$ 定義)。✓

4.6 唯一性失敗

$\mathrm{Fix}(T_{\text{stat}}) \supsetneq \{P^*\}$ 。其他具有相近統計性質的 $M6^*$ 子集也可滿足漸近 LOS 平衡(例如 $P^*$ 移除有限多個元素後仍滿足全部漸近條件),故 T_stat 單獨不足以唯一刻畫質數。T_stat 給出的是 $P^*$ 的必要不充分性質。

5. T_erg:遍歷層

5.1 層次再次位移

T_stat 在集合的轉移結構層操作。T_erg 必須再上一層:在集合的密度與擬隨機性層操作,捕捉質數序列作為測度論對象的整體性質。與 §4.1 同理,v0.2 以不動點謂詞刻畫(勘誤 4):「Gowers 一致分量」依賴的結構分解不保證唯一,否則分支不入定義。

5.2 有限 Gowers 構件

設 $f : \mathbb{N} \to \mathbb{R}$ 。乘法差分算子沿位移序列 $H = (h_1, \ldots, h_j)$ 遞迴定義:

$$\Delta_{\varnothing} f = f, \qquad \Delta_{(h :: H)} f(x) = \Delta_H f(x + h) \cdot \Delta_H f(x)$$

未正規化 Gowers $U^k$ 和:

$$G_k(f; N) = \sum_{h_1, \ldots, h_k \in [N]} \sum_{x \in [N]} \prod_{\omega \in \{0,1\}^k} f\!\left(x + \sum_i \omega_i h_i\right)$$

平凡界為 $|G_k(f;N)| \leq \|f\|_\infty^{2^k} \cdot N^{k+1}$ ;**正規化的 $U^k[N]$ 範數即 $\left(G_k(f;N)/N^{k+1}\right)^{1/2^k}$ **,故「 $U^k$ 範數趨零」等價於「 $G_k(f;N) = o(N^{k+1})$ 」。形式化直接以後者陳述,迴避實數開方。

對 $S \subseteq \mathbb{N}$,記平衡指示函數 $f_{S,N}(x) = \mathbf{1}_S(x) - \delta_S(N)$,其中 $\delta_S(N) = |S \cap [1,N]|/N$ 。

Lean 錨: gowersDiff、gowersSum、gowersNorm、charFn、density、balancedCharFn。

5.3 為什麼樸素定義不可用(勘誤 5)

v0.1 的 §5.2–5.3 將 W-trick 與對數正規化留在註記裡;形式化證明這不可省略,因為樸素謂詞在兩個方向上同時失效:

(i)平凡化。 命題:對任何自然密度為零的集合 $S$,均有 $G_k(f_{S,N}; N) = o(N^{k+1})$ 。證明梗概: 將乘積按指標子集 $T \subseteq \{0,1\}^k$ 展開。 $T = \varnothing$ 項為 $(-\delta)^{2^k} N^{k+1} = o(N^{k+1})$ ;$ T \neq \varnothing$ 項取定 $\omega_0 \in T$,整項被 $N^k \cdot |S \cap [(k+1)N]| = o(N^{k+1})$ 壓住。全程純計數。 $\square$ 平方數集、2 的冪集、任何稀疏集都「一致」——謂詞對 $P^*$ 的成立是計數平凡事實,與 Green–Tao–Ziegler 無關。以此版本陳述引用公理,等於把平凡事實掛在深刻定理名下。

(ii)重標定後為假。 若僅乘上 $\log N$ 重標定(補償對數密度),陳述翻為假:$M6^*$ 只清除了 mod 2、3 的偏差,質數對 mod 5、7、… 的剩餘類偏差仍在(質數避開 $0 \bmod q$ ),重標定後的平衡指示函數與相應週期相位有下界相關,$ U^2$ 條件不成立。這正是 W-trick 存在的理由。

5.4 定義(T_erg,v0.2)

定義 5.1(W-trick 模數)。 $W(w) = \prod_{p \leq w,\, p \in \mathbb{P}} p$ 。($W(0)=W(1)=1$,$W(2)=2$,$W(3)=6$,$W(5)=30$,…)

定義 5.2(Gowers 一致謂詞,W-trick 纖維化 + 對數重標定)。 $S \subseteq \mathbb{N}$ 滿足 Gowers 一致,若對所有 $k \geq 2$ 、所有 $w \in \mathbb{N}$ 、所有 $b < W(w)$ 且 $\gcd(b, W(w)) = 1$:

$$G_k\!\left(\,(\log N)\cdot f_{S_{w,b},\,N}\,;\; N\right) \;=\; o\!\left(N^{k+1}\right) \qquad (N \to \infty)$$

其中 $S_{w,b} = \{n \in \mathbb{N} : W(w)\,n + b \in S\}$ 為 $S$ 在互質纖維上的拉回。

$$S \in \mathrm{Fix}(T_{\text{erg}}) \;:\iff\; S \text{ 滿足定義 5.2}$$

Lean 錨: Wtrick、isGowersUniform。

非平凡性核查。 因 $(\log N)^{2^k}$ 因子,定義 5.2 要求 $G_k(f_{S_{w,b},N};N) = o\!\left(N^{k+1}/(\log N)^{2^k}\right)$ ——比 §5.3(i) 的計數平凡界($N^{k+1}/\log N$ 量級)強了 $(\log N)^{2^k - 1}$ 個量級。密度零不再免費過關。不為假核查。 纖維化在每個固定 $w$ 上殺掉了所有 $p \leq w$ 的剩餘類偏差;對所有 $w$ 的全稱量化即標準 W-trick 極限程序。

5.5 主定理(引用)

定理 C(Green–Tao 2008;Green–Tao–Ziegler 2012;介面式引用)。

$$P^* = \mathbb{P} \cap M6^* \in \mathrm{Fix}(T_{\text{erg}})$$

證明階層(文獻):

• $k=1$(Vinogradov 層): 質數在等差數列中均分布(Dirichlet + PNT in AP)。
• $k=2$(Weyl 層): 質數與線性相位的相關趨零,由 Vinogradov 型指數和估計給出。
• $k=3$(Green–Tao 2008): 質數中存在任意長等差數列的核心步驟,等價於 $U^3$ 一致性。
• $k \geq 4$(Green–Tao–Ziegler 2012): Gowers 逆定理 + 質數(Möbius 函數)與 nil-序列正交。 $\square$

引用校準(附錄 B.2)。 文獻原文以 von Mangoldt 加權的 W-trick 化函數陳述一致性;定義 5.2 採「對數重標定平衡指示函數」介面,兩者為調和分析中的標準等價表述。形式化中定理 C 以引用公理 GTZ_uniformity : isGowersUniform primesM6 進入,隔離於單一檔案(附錄 A.3),其依賴邊界在公理審計中可見。本工程簽署的是等價介面,非逐字原文。

5.6 密度均勻性驗算

$P^* \cap [5, 97]$ (23 個質數),按模 3 分類:殘差 1 共 11 個;殘差 2 共 12 個;比值 $\approx 1 : 1.09$,趨向 $1:1$ (Dirichlet 漸近均勻)。✓ 按模 6:$ \equiv 1$ 共 11 個、 $\equiv 5$ 共 12 個。✓ $U^k$ ($ k \geq 2$ )的數值驗算需 $N \geq 10^6$ 量級,在 Green–Tao–Ziegler 文獻中已完整建立。

5.7 T_erg 的局限

• 已證(引用): $P^* \in \mathrm{Fix}(T_{\text{erg}})$ 。
• 未證: 唯一性。Möbius 隨機性猜想的完整版本尚未對所有集合建立,不能排除其他 $M6^*$ 子集也滿足定義 5.2。擬隨機性不唯一。

6. 三算子合攏

6.1 主合攏定理(v0.2 修正型)

型別勘誤(勘誤 1)。 v0.1 的盒裝主定理

$$\mathrm{Fix}(T_{\text{top}}) \cap \mathrm{Fix}(T_{\text{stat}}) \cap \mathrm{Fix}(T_{\text{erg}}) = \mathbb{P} \cap M6^*$$

是型別錯誤:$\mathrm{Fix}(T_{\text{top}}) \subseteq M6^*$ 是元素的集合,而 $\mathrm{Fix}(T_{\text{stat}}), \mathrm{Fix}(T_{\text{erg}}) \subseteq \mathcal{P}(M6^*)$ 是集合的族,三者不可相交。紙面靠讀者善意通融;形式化不通融。修正陳述:

合攏定理′。 設 $P^* = \mathbb{P} \cap M6^*$ 。則:

$$\boxed{\;P^* = \mathrm{Fix}(T_{\text{top}}) \;\;\wedge\;\; P^* \in \mathrm{Fix}(T_{\text{stat}}) \;\;\wedge\;\; P^* \in \mathrm{Fix}(T_{\text{erg}})\;}$$

等價地,對任意 $S \subseteq M6^*$(條件於 LOS 展開猜想與定理 C):

$$S = P^* \iff S = \{n \in M6^* : T_{\text{top}}(n) = n\} \;\wedge\; S \in \mathrm{Fix}(T_{\text{stat}}) \;\wedge\; S \in \mathrm{Fix}(T_{\text{erg}})$$

證明: 右到左由第一肢與定理 A 的集合形式獨力給出($S = \mathrm{Fix}(T_{\text{top}}) = P^*$)。左到右:第一肢由定理 A;第二肢由定理 B(條件於 LOS 展開);第三肢由定理 C(引用)。$ \square$

Lean 錨: 雙版本——

• main_closure:以 LOS 展開與 $P^*$ 的 Gowers 一致性為顯式假設,證明本體零自訂公理(僅標準三公理);
• main_closure_cited:以引用公理 GTZ_uniformity 釋放 Gowers 假設,隔離於引用區檔案,其公理依賴集為標準三公理 $\cup\ \{$ GTZ_uniformity$\}$,污染邊界精確到此單一定理。

邏輯結構的誠實化。 形式化使以下事實不可迴避:右到左方向只用了第一肢。 $T_{\text{top}}$ 的不動點集已唯一鎖定 $P^*$ ;統計肢與遍歷肢在合攏定理中對定位邏輯上冗餘。v0.1 的「三角定位」是修辭;真實結構是一肢定位、兩肢佐證——後兩肢的價值在於它們是 $P^*$ 經機器錨定的、跨語言的必要性質(§1.3, §6.3)。

6.2 三層次對比(含形式化狀態)

6.3 三個算子的關係

三個算子不是三個競爭的候選方案,而是同一個對象在三個正交數學領域的三個面向:

• $T_{\text{top}}$ 回答:「這個數字在乘法結構上是不可分解的嗎?」
• $T_{\text{stat}}$ 回答:「這條序列在連續對上是否有質數特有的反重複傾向?」
• $T_{\text{erg}}$ 回答:「這條序列在(對數重標定、W-trick 纖維化後的)密度分布上是否無法被多項式相位函數捕捉?」

定位由第一問獨力完成;後兩問的同時「是」,是 $P^*$ 在統計與測度語言中的身分證明。三種語言各自以不動點形式指認同一對象——這個共指現象本身,是 §7 幾何融合問題的動機。

7. 代數幾何的視角

7.1 已經存在的那塊

三個算子在代數幾何中已有對應:

$T_{\text{top}}$ $\leftrightarrow$ $\mathrm{Spec}(\mathbb{Z})$ 的 Zariski 拓撲。 每個質數 $p$ 對應閉點 $(p)$,零理想 $(0)$ 是泛點。閉點正是 Zariski 拓撲中最「極小」的點—— $T_{\text{top}}$ 的不動點結構在幾何上對應「閉點是其自身閉包的最小元素」。(本文 §3.6 的 Alexandrov 拓撲是此對應的初等影子:質數 = 開點,方向相反是因為整除序與包含序的對偶。)

$T_{\text{erg}}$ $\leftrightarrow$ Weil 猜想(Deligne 1974 已證)。 對有限域上的代數曲線,$\mathbb{F}_{q^n}$ 上的點字面上是 Frobenius 的不動點;等分布性正是「Frobenius 特徵值絕對值為 $q^{1/2}$ 」的幾何表達——T_erg 的遍歷均分布在幾何語言中的版本。

$T_{\text{stat}}$ $\leftrightarrow$ étale 上同調與 L 函數。 連續質數的轉移偏差在解析數論中與 Dirichlet L 函數的精細結構相關;L 函數是算術概型 étale 上同調的「特徵多項式」,其零點結構控制質數在剩餘類中的分布偏差。

7.2 缺失的那塊

三個算子在代數幾何中「應該」融合成一個定理——但存在根本性障礙:$\mathrm{Spec}(\mathbb{Z})$ 的基底問題。 有限域上的曲線有明確基底 $\mathrm{Spec}(\mathbb{F}_q)$ ;$ \mathrm{Spec}(\mathbb{Z})$ 的「基底」應是某種 $\mathbb{F}_1$,而此對象在標準數學中不存在。這正是三個算子必須各說各的語言的根源:它們本應是同一幾何語言在 $\mathrm{Spec}(\mathbb{Z})$ 上的三個投影,但承載它們的幾何框架尚未完整建立。各種嘗試:Arakelov 幾何、 $\mathbb{F}_1$ 理論(Tits, Connes, Haran 等)、Mochizuki IUT。

7.3 缺口即黎曼假設

若 $\mathrm{Spec}(\mathbb{Z})$ 能真正成為代數幾何意義下的「曲線」,則

$$T_{\text{top}} + T_{\text{stat}} + T_{\text{erg}} \longrightarrow \text{一個幾何定理(Lefschetz 不動點公式的算術版本)}$$

這個融合等價於黎曼假設的幾何形式:「 $\zeta(s)$ 的零點在臨界線上」等同於「Frobenius 特徵值絕對值恰為 $q^{1/2}$ 」在 $\mathrm{Spec}(\mathbb{Z})$ 上的類比。本文三算子程式的直觀缺口,指向的正是黎曼假設的幾何形式所在的牆壁的另一面。

8. 認識論附記:升維的意義,與形式化作為認識工具

8.1 升維策略

第一維(代數): T_top 問個別元素的二元問題,依賴乘法結構。第二維(統計): T_stat 問序列的頻率問題,依賴轉移結構。第三維(遍歷): T_erg 問測度的極限問題,依賴擬隨機性。三個問題從三個數學語言出發指認同一對象——不是三個替代方案,而是三個必要條件的聯立,其中第一個已然充分。

小數點的位置。 T_top 全程整數,無小數點。T_stat 的有限期望 $(k_x-1)/\varphi(m)^2$ 是精確有理數;小數點在「除以總數」處出現(顯示選擇,非數學實質)。T_erg 的 Gowers 條件涉及極限與 $\log N$ 重標定,是真正的實數操作——小數點在「有限離散到無限連續」的接縫處出現,且 v0.2 顯示這道接縫上還站著 W-trick:離散的剩餘類偏差必須先被纖維化清除,連續的極限陳述才不為假。

8.2 形式化作為認識工具

v0.1 到 v0.2 的全部差異由機器驗證過程強迫產生,五處修正(附錄 C)各對應一種「看起來對」與「是對的」之間的距離:

1. 型別距離(勘誤 1):紙面記號允許不同層的對象假裝同層相交;型別系統不允許。
2. 算術距離(勘誤 2):定義文字與自身表格的算術可以不一致而無人察覺;kernel 驗算不行。
3. 承重距離(勘誤 3):「由 Dirichlet 保證」這類籠統歸因,在推導被迫逐步寫出時顯形為具體的守恆約束。
4. 良定義距離(勘誤 4):敘事裝置(否則分支)與數學內容(不動點謂詞)的邊界,在「必須能定義」的壓力下浮現。
5. 語義距離(勘誤 5):一個謂詞可以形式上無懈可擊而內容上平凡;引用一條文獻,等於替原作者簽名,簽之前必須確定那是他們寫過的句子。

形式化不曾證明任何 v0.1 沒有主張的東西;它做的是測量每一個主張與其精確形狀之間的距離,然後把距離燒掉。

9. 開放問題

1. T_stat 的唯一性: 是否存在非質數的 $M6^*$ 子集(具有對數密度),滿足所有 $m$ 的漸近 LOS 平衡?
2. T_erg 的唯一性: Möbius 隨機性猜想的完整版本是否蘊含「具有對數密度且(W-trick 意義下)Gowers 一致的 $M6^*$ 子集唯一等於質數集」?
3. 代數幾何融合: 在 $\mathrm{Spec}(\mathbb{Z})$ 的正確完備化下,三算子是否融合為單一幾何定理?此問題等價形式是黎曼假設。
4. M6* 以外: 三算子程式對 $M30^*$ 等更高模數互質剩餘類集合的推廣。形式化基礎設施(轉移計數器、Gowers 構件、W-trick)已對一般模數參數化,推廣的形式化成本為增量。
5. 認識論的二階: 本文的 T_stat 是「統計二階」(從元素到對),而非原始意義下的「認識論二階」(從描述到描述的描述)。後者是否對應 Gilbreath 三角的 meta-算子,待展開。
6. (v0.2 新增)LOS 展開的部分無條件化: 定理 B 的推導完全機器化後,焦點移至前提:LOS 展開猜想中是否存在可無條件證明的弱化(例如固定小模數、或將二階項放寬為單邊不等式),使統計肢獲得部分無條件地位?

附錄 A:機器驗證附錄

A.1 庫結構與工具鏈

形式化庫 EML-NT-2026-PFPT,Lean 4(leanprover/lean4:v4.30.0)+ Mathlib(pinned v4.30.0),全庫編譯 2062 作業、零錯誤零警告。模組:

EML/PFPT/
  Basic.lean          -- M6* 定義、互質橋、兩封閉引理、primesM6
  Ttop.lean           -- Ttop(minFac 實現)、Ttop_spec、定理 A 三形式、minFac_eq_of_comp
  Topology.lean       -- 整除偏序、Alexandrov 拓撲實例、命題 3.6
  Verification.lean   -- 表 3.4(19 行)、表 4.4(4 格)kernel 銷帳
  Stat/Defs.lean      -- 轉移計數器、互質剩餘類、有限/漸近 LOS 謂詞
  Stat/TheoremB.lean  -- LOS_expansion、isLittleO_sum、定理 B
  Erg/Gowers.lean     -- Gowers 構件、Wtrick、isGowersUniform(R11 版)
  Erg/Cited.lean      -- 引用隔離區:恰兩條宣告
  Main.lean           -- 合攏定理′(main_closure)

A.2 命題對照表

標準三公理 = propext, Classical.choice, Quot.sound(Lean 4 標準型別論公理)。擔保強度區分: verify_table_4_4 因計數器以結構遞迴實現,連標準公理亦不需,為全文機器擔保最強的命題;其餘 kernel 級命題依賴標準三公理。全庫零 sorry、零 admit、零 unsafe、零 native_decide。

A.3 公理污染邊界

全庫唯一自訂公理:

axiom GTZ_uniformity : isGowersUniform primesM6

隔離於 Erg/Cited.lean,該檔恰含兩條宣告(公理本身與釋放定理 main_closure_cited)。#print axioms 審計確認:污染邊界精確到 main_closure_cited 單一定理;main_closure 及其餘全部宣告不含自訂公理。引用區之外的任何檔案出現自訂公理即違反庫的 CI 紅線。

A.4 凍結陳述名冊

九條承重陳述(定理 A 三形式、命題 3.6、合攏定理′ 雙版本、LOS 展開、定理 B、Gowers 定義本體、引用公理)的正典 Lean 簽名凍結於 statement_roster.md v1.0,任何字符偏離須附裁決編號(PFPT-R 系列,本案共 12 道)。名冊前言規則:謂詞若被任何公理引用,凍結範圍自動從簽名擴展到定義本體——因為對公理載體而言,定義本體即陳述。

附錄 B:誠實邊界

B.1 定理 B 是條件命題。 形式化證明的是「LOS 展開猜想 ⟹ $P^*$ 漸近 LOS 平衡」這條蘊含,未證明 LOS 展開猜想本身(其依賴 Hardy–Littlewood 型猜想,屬數論深水區)。統計肢的地位是:推導已封閉,前提仍開放。

B.2 定理 C 是介面式引用。 Lean 謂詞 isGowersUniform 採「對數重標定平衡指示函數 + W-trick 纖維化」介面;Green–Tao 與 Green–Tao–Ziegler 原文以 von Mangoldt 加權形式陳述。兩者為標準等價表述,但本工程簽署的是等價介面,非逐字原文;引用公理的精確措辭經獨立審計比對文獻結構,並在庫中以單點隔離標示其信任邊界。

B.3 唯一性開放。 合攏定理′ 的定位由 $T_{\text{top}}$ 獨力承擔;$T_{\text{stat}}$與$ T_{\text{erg}}$ 各自的不動點族是否在適當密度條件下唯一收束於 $P^*$,數學上開放(§9 問題 1、2)。本文不主張統計或遍歷層的判別力。

B.4 模數排他性。 全部結果在 $M6^*$ (與 6 互質)內陳述;$2$ 與 $3$ 被框架構造排除,完整質數集為 $\mathrm{Fix}(T_{\text{top}}) \cup \{2, 3\}$ 。

附錄 C:v0.1 → v0.2 勘誤記錄

以下五處修正全部由 Lean 形式化過程強迫產生,各附審計來源:

1. §6.1 型別錯誤。 主合攏定理的 $\cap$ 將元素集合與集合族混層相交;修正為三肢合取(合攏定理′),並誠實化邏輯結構(一肢定位、兩肢佐證)。來源:型別審計,計畫階段攔截。
2. §4.2 期望正規化不一致。 文字定義 $|S|/\varphi(m)^2$ 與表 4.4 算術 $(|S|-1)/\varphi(m)^2 = 5.5$ 矛盾($k$ 個元素僅 $k-1$ 個轉移對);採表格一致版。來源:謂詞形式化時的算術核對。
3. §4.2「行和為零」語義。 非計數精確等式;真實形式為猜想係數族的守恆約束 $\sum_b C_{a,b} = 0$,行和受控由之推出。來源:定理 B 行和肢的推導被迫逐步寫出。
4. T_stat / T_erg 否則分支不良定義。「最大子集」「一致分量」的存在唯一性無保證;改以不動點謂詞刻畫,否則分支自定義中移除。來源:定義審計,進管線前裁決。
5. §5.2–5.3 W-trick 與對數正規化缺失。 樸素 Gowers 謂詞對一切密度零集合平凡成立(計數論證,§5.3(i)),僅加對數重標定則為假(小模數偏差,§5.3(ii));兩者必須寫進謂詞本體。來源:引用公理語義審計——本案唯一在交付後而非計畫階段攔截的缺陷,印證「公理寫錯比 sorry 更隱蔽」。

參考文獻

[LOS2016] R. J. Lemke Oliver and K. Soundararajan, Unexpected biases in the distribution of consecutive primes, Proc. Natl. Acad. Sci. USA 113 (2016), E4446–E4454. arXiv:1603.03720.

[GT2008] B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008), 481–547. arXiv:math/0404188.

[GTZ2012] B. Green, T. Tao, and T. Ziegler, An inverse theorem for the Gowers $U^{s+1}[N]$ -norm, Ann. of Math. 176 (2012), 1231–1372. arXiv:1009.3998.

[Deligne1974] P. Deligne, La conjecture de Weil, I, Inst. Hautes Études Sci. Publ. Math. 43 (1974), 273–307.

[Furstenberg1955] H. Furstenberg, On the infinitude of primes, Amer. Math. Monthly 62 (1955), 353.

[Odlyzko1993] A. M. Odlyzko, Iterated absolute values of differences of consecutive primes, Math. Comp. 61 (1993), no. 203, 373–380.

[Guy1994] R. K. Guy, Unsolved Problems in Number Theory, 2nd ed., §A10, Springer, 1994.

[Chase2020] Z. Chase, A random analogue of Gilbreath's conjecture, arXiv:2005.00530 (2020).

[Colonna2026] J.-F. Colonna (with J.-P. Delahaye), Proth–Gilbreath Conjecture, CMAP, École polytechnique, 2026.

[Plouffe2025] S. Plouffe, Verification of Gilbreath's conjecture up to $10^{14}$, arXiv:2510.06688 (2025).

[Lean4] L. de Moura and S. Ullrich, The Lean 4 Theorem Prover and Programming Language, CADE 2021. 工具鏈:leanprover/lean4:v4.30.0;Mathlib v4.30.0。

v0.1 完成於 2026 年 5 月 30 日;v0.2(機器驗證版)完成於 2026 年 6 月 12 日。 EveMissLab 版本號:EML-NT-2026-PFPT-v0.2。形式化庫:EML-NT-2026-PFPT(Lean 4),凍結名冊 v1.0,審計裁決 PFPT-R01–R12。