# DeepSeek V4 Flash 工作轨迹：有界素数间隔问题的独立验证与探索

> 公开说明：这是本次 DeepSeek V4 Flash 数学研究任务的技术工作记录，保留了执行过程中的任务拆解、算法设计、调试与阶段性判断，供读者参考。它不是供应商导出的原始 API JSON 或逐 token 日志；代码、证书和最终仓库状态应以项目仓库为准。
>
> 版本说明：本文主体记录的是执行过程中的阶段性状态，因此其中关于 H(45)、H(50) 的“运行中”、定理数量和文件布局可能早于当前仓库。最新的 `lean_cert/` 证书与最终状态请以 [项目仓库](https://github.com/guoshaoyang-pku/twin-prime-admissible) 为准。

> 本文档是 AI 执行 agent（fork 子进程）在"孪生素数猜想 / 有界素数间隔"问题上全部工作的详细技术记录。
> 目的：供数学专业读者审阅。所有结论都区分了【严格证明】【可复现计算】【启发式证据】三个等级。

---

## 0. 任务缘起与目标

原始任务（来自用户）："解决孪生素数猜想，或者把现有的值（246）缩短。"
Agent 在任务开始时即声明：这两件事在当前数学框架下均不可行——孪生素数猜想被 Selberg 奇偶性障碍阻挡；246 是 Polymath8b（2014）大规模变分优化的压线结果。随后的工作转向两条可行路线：(A) 对可容许 k 元组最小直径 H(k) 做**完全自足的穷举证明**（不依赖任何外部数据）；(B) 探索文献中从未发布的 k<50 的 Maynard 筛泛函值 M_{k,ε}（"超越 246"的唯一潜在路径）。

---

## 1. 数学背景：246 纪录的完整逻辑链

### 1.1 判据（Polymath8b, arXiv:1407.4897）

无条件（Bombieri–Vinogradov，θ = 1/2）下，若

$$M_{k,\varepsilon} > 4 \qquad (m=1, \theta=1/2)$$

则 DHL[k,2] 成立，即存在无穷多 n 使 n + h₁, …, n + h_k 中至少两个为素数（h 为任意可容许 k 元组），从而

$$H_1 \le H(k) := \min\{\max h - \min h : h \text{ 可容许 } k\text{-tuple}\}$$

其中 M_{k,ε} = sup_F [Σᵢ J_{i,1−ε}(F) / I(F)]，F 支撑在 ε-扩大单纯形 (1+ε)R_k 上（定理 3.12，ε-扩大单纯形版本）。

**可容许**：k 个互异整数，对每个素数 p ≤ k，模 p 的剩余类不覆盖全部 p 个类（p > k 自动满足）。

### 1.2 纪录链

| 年份 | 纪录 | 关键进展 |
|---|---|---|
| 2013 | 70,000,000 | 张益唐：新素数分布定理（光滑模 MPZ 型）→ k₀ = 3,500,000 |
| 2013 | 4,680 | Polymath8：分布常数改进 → k₀ = 632 |
| 2013 | 600 | Maynard–Tao 多维筛：k₀ 暴降到 105 |
| 2014 | **246** | Polymath8b：M 泛函变分优化 + ε-扩大单纯形 → k₀ = 50；H(50) = 246 |

关键数值（Polymath8b 严格计算）：M_{50,1/25} > **4.0043**——k=50 首次压线过 4（裕量 0.1%）。**k < 50 的 M_{k,ε} 数值从未被发布**（我们的文献核实确认了这一空白）。

---

## 2. 元组侧：H(k) 的完全自足证明

### 2.1 搜索算法（自研，C 实现）

对固定 (k, d) 判定 [0,d] 内是否存在可容许 k 元组：

- **归约**：平移不变性 ⟹ WLOG 含 0；最小直径 ⟹ WLOG 含 d；模 2 ⟹ 全偶。候选 = {0, d} ∪ 偶数。
- **DFS + 频数剪枝**：维护每个素数 p ≤ k 的已覆盖剩余类位掩码；剪枝条件为"已覆盖类位置数 + 频次最高的 budget 个新类位置数 ≥ 还需选择的个数"（budget = p−1−已覆盖类数）。这是本项目少数需要从第一性原理推导的组件（初版剪枝有数学错误，经手算反例修正）。
- **完备性**：对每个偶数 d < H(k) 逐点证明 UNSAT（搜索彻底性由剪枝的数学正确性保证）；在 d = H(k) 处给出显式见证元组。

### 2.2 已完成的自足证明（严格、可复现、不依赖 OEIS/Clark–Jarvis）

| 定理 | 状态 | 证据 |
|---|---|---|
| H(43) = 200 | ✅ 完整 | 全部 d<200 UNSAT + 显式见证 |
| H(44) = 210 | ✅ 完整 | 全部 d<210 UNSAT（含 d=204/206/208）+ 见证 |
| H(46) = 216 | ✅ 完整 | 全部 d<216 UNSAT（13 个偶数边界点）+ 见证 |
| H(45) = 212 | 🔄 收尾 | d≤208 UNSAT 已证；d=210 运行中 |
| H(50) = 246 | 🔄 收尾 | d≤220 UNSAT 已证；d=222..244 并行运行中；d=246 见证已找到 |
| H(2)..H(42) | ✅ 全表 | 与 OEIS A008407 逐项零失配（43 项对照） |

**重要澄清**：这些 H(k) 值本身是已知的（Clark–Jarvis 2001；OEIS A008407；Polymath8b 论文 Section 10）。本工作的增量是**完备性**——对关键 k 值给出第一个（据我们所知）不依赖外部程序的穷举证明链；但我们**无法声称"首次"**（Polymath 项目用 SAT 求解器做过类似验证，其代码与数据公开）。此点已向审阅者如实说明。

### 2.3 k=46 下行见证（H(46)=216 的证明支撑）

对 d = 246, 244, 242, …, 216 的每一个偶数，均给出显式可容许 46 元组（全部通过独立验证器：直接枚举模 p 剩余类覆盖——与搜索程序算法完全不同的第二实现）。

k=50 纪录元组（d=246）已被独立复现：{0, 2, 6, 8, 12, 18, 20, 26, 30, 32, 36, 42, 48, 50, 56, 62, 68, 72, 78, 86, 90, 96, 98, 102, 110, 116, 120, 128, 132, 138, 140, 146, 152, 156, 158, 162, 168, 176, 182, 186, 188, 198, 200, 210, 212, 216, 230, 240, 242, 246}。

---

## 3. Lean 4 形式化（机器验证）

文件 `TwinPrimeAdmissible.lean`：**89 个定理，仅 import Init（Lean 核心库，无 mathlib），零 sorry/axiom，编译 EXIT 0**。

覆盖：
- k = 43..50 六个关键见证的可容许性 + 直径 + 存在性定理（如 `H46_le_216 : ∃ t, t.length = 46 ∧ admissible 46 t ∧ diameter t = 216`）；
- k = 46 的 14 个下行见证（d = 246→216）；
- H(2)..H(12) 的**精确最小性定理**（形式：存在性 + ∀ d < H(k) 穷举不可行，含 0 ⇒ 全偶剪枝后 native_decide 机器验证，k=12 用时 17s）；
- **手写结构定理**（非计算）：平移不变性 `admissible_translate`（模 p 加法消去 + 剩余类双射）；存在性 `exists_admissible`（primorial 构造 [0, M, 2M, …, (k−1)M]，M = ∏_{p≤k} p，对任意 k ≥ 1）；单调性 `admissible_tail`。

难点（核心库缺失理论的手工补充）：eraseDups 理论、模消去、++ 结合性、List 归纳参数顺序。

---

## 4. M_{k,ε} 泛函：严格判定工具链（本项目方法论上最重要的部分）

### 4.1 符号积分框架（自研，精确有理数）

函数族：$F(t) = (1+\varepsilon-\sum t)^r \cdot g(p_1,\dots,p_m)$，$p_a = \sum_i t_i^a$ 为幂和，g 为幂和单项式 $\prod p_a^{m_a}$ 的线性组合（基 = 度数 ≤ D 的幂和多重集，大小 p(0)+…+p(D)）。

所有积分闭式化（Dirichlet 型），关键恒等式：

$$\int_{(1+\varepsilon)R_k} (1+\varepsilon-\textstyle\sum t)^s\, p_\gamma\, dt = (1+\varepsilon)^{k+|\gamma|+s}\,\frac{s!\, H_k(\gamma)}{(k+s+|\gamma|)!}$$

其中 $H_k(\gamma)$ = 槽位（带标签）划分为坐标组的组合计数 $\sum_{\text{partitions}} \frac{k!}{(k-g)!}\prod_{\text{groups}}(\text{group sum})!$，用 DP 精确计算。J₁ 侧同理（Beta 函数 + 1−ε 缩放的 Dirichlet）。

**已发现的数学现象**：k 个变量上，part 数 > k 的幂和基线性相关（Newton/基本对称多项式恒等式）——例如 5 变量上 p₁⁶ 可由 ≤5-part 的幂和多项式表出。这曾一度被误判为 bug，实为正确的代数事实（精确核向量验证）。

### 4.2 严格判定：LDLᵀ 惯性定理（无近似）

**判定命题**：M_{k,ε} > 4 ⟺ J₁ − (4/k)·I 存在正特征值 ⟺ 其精确有理数 LDLᵀ 分解的枢轴含正号（对称矩阵惯性定理）。所有运算为 Fraction（任意精度整数），**无浮点近似**。

过程中发现并修复的关键 bug：矩阵构建中 `int/int` 混入 float 污染（曾导致假"正特征值"判定）；修复后 J₁ 全 Fraction、对称差精确为 0。

### 4.3 严格结果（族内，D=8）

有理数二分（LDLᵀ 惯性 + 二分）给出族内 λ_max 的**严格区间**（宽度 < 10⁻¹⁰）：

| k | ε | 族内 M（D=8，严格） | 参考：真实值（外部） |
|---|---|---|---|
| 46 | 1/25 | **3.6518799** | ≈ 3.96（渐近标定） |
| 49 | 1/25 | **3.6970517** | ≈ 3.99–4.00（渐近标定） |
| 50 | 1/25 | **3.7111478** | 4.0043（Polymath8b） |

- D=8、D=10 的 LDLᵀ 判定均严格证明"族内 M < 4"（k=46/49/50）。
- D=10 的族内严格值（二分）与 D=12 的判定在更大规模上运行中（大整数运算，单点数小时）。
- 坐标下降给出的精确下界（3.21–3.24）劣于二分（说明优化器非瓶颈，二分是完备的）。

**局限（必须声明）**：有限多项式族（度数 ≤ D）内 M < 4 不能推出全空间 M_{k,ε} < 4（真实 sup 更大；k=50 的族内 3.71 vs 真实 4.0043 即为例证）。若某 D 处族内 > 4 出现，则**自动成为真实 M > 4 的完整证明**（下界单调）；但我们的证据表明真实值 < 4，故该路径大概率不会触发。

### 4.4 解析上界（论文方法的数值优化）

Polymath8b 的 Prop（mkeps）与 Remark：

$$M_{k,\varepsilon} \le \frac{k}{k-1}\log(2k-1)$$

$$M_{k,\varepsilon} \le \frac{k}{a(k-1)}\log\left(k + \frac{(a(1+\varepsilon)-1)(k-1)}{1-a(1-\varepsilon)}\right),\quad \frac{1}{1+\varepsilon}<a<\frac{1}{1-\varepsilon}$$

对 a 数值最优：

- **k=44, ε=1/50：上界 3.948 < 4 ✅（完整证明该点）**
- **k=46, ε=1/50：上界 3.991 < 4 ✅（完整证明该点）**
- k=46, ε=1/25：上界 4.070 > 4（**缺口 1.75%**）——全空间"∀ε 排除"未闭合

我们尝试过双参数/三参数权重族（G_i = c/(u+v·t_i)、c/(u+v·s′+w·t_i) 型）改进上界，数值结果不佳或推导待完善——**1.75% 缺口仍是开放问题**（需要新数学或 Polymath 级区间算术工程）。

### 4.5 启发式证据（非严格，但方向一致）

- **渐近标定**：以论文实测 M₅₄ ≥ 4.00238 标定 M_k ≈ log k − 2loglog k + 2.7805，加 ε 增益（由 M₅₀,₁/₂₅ = 4.0043 标定 ≈ 0.04）——交叉点精确复现在 **k = 50**；M_{46,1/25} ≈ 3.96，M_{49,1/25} ≈ 3.995。
- 若真实 M₅₄ 略高于 4.00238（下界），k=49 的真实值可能非常接近 4——**这是本项目唯一未能排除的"超越"场景**（但族内收敛趋势不支持）。

---

## 5. 文献核实（Web 调研）

- **246 仍是无条件纪录**（2024–2026 无权威来源显示被超越；无 arXiv/MathOverflow/专家博客证据）。
- 一篇 ResearchGate 预印本《A Weighted Distribution of Primes and a New Unconditional Bound on Gaps Between Primes》（2025）无法核实内容（无 arXiv 版本、页面反爬）——不构成可信证据。
- **k<50 的 M_{k,ε} 数值空白确认**：Polymath8b 只发布了 k=50 的计算；Polymath 维基与论文未见 k=46..49 的 M 值记录。

---

## 6. 方法与历史纪录方法的对比（重要）

- **历史纪录**（70,000,000 → 246）的每一步：解析数论新定理定 k₀（张益唐分布定理 → Maynard 筛 → Polymath 变分优化），元组搜索只是**最后一步的"存在性上界"**（当时张益唐甚至用朴素构造，未用最小元组）。
- **本项目的元组工作**：穷举证明**最小性下界**（H(k) 确切值）——比纪录所需更强，但**方向相反**：它不能产生新的更小上界。
- **核心结论**：元组侧已到底（H(46)=216、H(50)=246 均最小）；任何更小的纪录 d 都要求解析侧突破（M_{46,ε}>4 或 M_{49,ε}>4，即 k₀ 从 50 降到 46/49），而所有严格与启发式证据都指向 M_{k<50,ε} < 4。

---

## 7. 诚实评估（致数学读者）

1. **数学新结果：无**。H(k) 值、M₅₀ 值、判据、方法均为已知；本工作是对已知结果的独立完备验证与工具沉淀。
2. **可能的新产物**：
   - Lean 4 形式化库（89 定理）——据我们未完全核实的了解，mathlib 社区无此内容；**首创性未确认**。
   - LDLᵀ 惯性判据 + 有理数二分作为"变分 Rayleigh 商 vs 阈值"的通用严格判定方法——方法论上有一定通用性。
   - k<50 的 M 值族内严格数据（文献空白处的第一笔数据，虽然是下界）。
3. **未完成/开放**：
   - "246 不可超越"的全空间严格证明：1.75% 解析缺口（k=46, ε=1/25 处）。
   - H(45)=212、H(50)=246 的收尾 UNSAT（计算进行中，预期与已知值一致）。
   - 孪生素数猜想本体：未触及（奇偶性障碍）。

---

## 8. 复现指引

```bash
# 元组最小性（C）
gcc -O3 -o admissible admissible.c -lm; ./admissible 2 50
./admissible_d 46 216          # 单点 SAT/UNSAT 判定

# M 泛函严格判定（Python，仅标准库）
python3 mk_probe_strict.py 46 1 25 8 8 6   # LDLᵀ 惯性判定
python3 mk_bisect.py 46 1 25 8 8 6 50      # 严格区间二分

# Lean 4（v4.33.0，仅核心库）
lean TwinPrimeAdmissible.lean              # EXIT 0，89 定理
```

所有代码与结果：`/data3/guoshaoyang/workdir/math/`（本地 git 仓库，提交 db87837；含 results/ 全部 UNSAT 与严格判定日志）。