# 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 級機器銷帳)

| $n$ | $T_{\text{top}}(n)$ | 不動點? | 質數? |
|---|:---:|:---:|:---:|
| 5, 7, 11, 13, 17, 19, 23 | 自身 | ✓ | ✓ |
| 25 = 5² | 5 | ✗ | ✗ |
| 29, 31 | 自身 | ✓ | ✓ |
| 35 = 5·7 | 5 | ✗ | ✗ |
| 37, 41, 43, 47 | 自身 | ✓ | ✓ |
| 49 = 7² | 7 | ✗ | ✗ |
| 55 = 5·11 | 5 | ✗ | ✗ |
| 65 = 5·13 | 5 | ✗ | ✗ |
| 77 = 7·11 | 7 | ✗ | ✗ |

全表十九行由 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$。

| 轉移 $(a,b) \bmod 3$ | 計數 | 期望 | 偏差 $\Delta$ | 方向 |
|:---:|:---:|:---:|:---:|:---:|
| (1,1) | 3 | 5.5 | $-2.5$ | ✓ 對角壓低 |
| (1,2) | 7 | 5.5 | $+1.5$ | ✓ 反對角抬升 |
| (2,1) | 8 | 5.5 | $+2.5$ | ✓ 反對角抬升 |
| (2,2) | 4 | 5.5 | $-1.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 三層次對比(含形式化狀態)

| 算子 | 操作層 | 操作對象 | 質數為不動點 | 唯一性 | 機器狀態 |
|:---:|:---:|:---:|:---:|:---:|:---:|
| $T_{\text{top}}$ | 代數 | 元素 $n \in M6^*$ | ✓ 無條件 | ✓ 完全 | kernel 級已證(零自訂公理) |
| $T_{\text{stat}}$ | 統計 | 子集 $S \subseteq M6^*$ | ✓ 條件於 LOS 展開 | ✗ 開放 | 條件推導 kernel 級已證 |
| $T_{\text{erg}}$ | 測度 | 密度/擬隨機性 | ✓(GT/GTZ) | ✗ 開放 | 介面式引用公理,單點隔離 |

### 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 命題對照表

| 論文項 | Lean 名 | 公理依賴 |
|---|---|---|
| 引理 2.1–2.3 | `coprime_six_iff` / `mul_closed` / `dvd_closed` | 標準三公理 |
| 定理 A(三形式) | `fix_Ttop_iff_prime` / `fix_Ttop_set_eq` / `fix_min_iff_prime` | 標準三公理 |
| 規格=實現 | `Ttop_spec` | 標準三公理 |
| 命題 3.6 | `isOpen_singleton_iff_prime` | 標準三公理 |
| 表 3.4 | `verify_table_3_4` | 標準三公理 |
| 表 4.4 | `verify_table_4_4` | **零公理** |
| 定義 4.2 / 4.3 | `isLOSBalanced_upto` / `isLOSBalanced_asymp` | 標準三公理 |
| 定義 4.4 | `LOS_expansion` | 標準三公理 |
| 定理 B | `theorem_B` | 標準三公理 |
| 定義 5.1 / 5.2 | `Wtrick` / `isGowersUniform` | 標準三公理 |
| 合攏定理′(假設版) | `main_closure` | 標準三公理 |
| 合攏定理′(引用版) | `main_closure_cited` | 標準三公理 + `GTZ_uniformity` |

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

### A.3 公理污染邊界

全庫唯一自訂公理:

```lean
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。*