# EP-414 攻题命题书 · Erdős Problem #414（迭代除数函数轨道汇聚猜想）

**来源与引用**：T. F. Bloom, Erdős Problem #414, https://www.erdosproblems.com/414（访问 2026-10-06）；原始出处 [ErGr80, p.82]（Erdős & Graham, *Old and New Problems and Results in Combinatorial Number Theory*）。站方状态：**OPEN**（开放问题，明示「cannot be resolved with a finite computation」——任何有限计算都无法终结它，只有证明或反例能）。站方标注「Formalised statement? Yes」。

## 数学内容

设 τ(n) 为 n 的约数个数，定义 h₁(n)=h(n)=n+τ(n)，h_k(n)=h(h_{k−1}(n))。

**猜想（Erdős–Graham， believed YES）**：对任意正整数 m, n，存在 i, j 使 h_i(m) = h_j(n)。也就是说，迭代 n ↦ n+τ(n) 的所有轨道最终汇入同一条链（只有一个「 attractor」序列）。

## 本战役接受的两类解决

1. **证明**：对上述猜想给出完整证明，交付为自包含 Lean 4 代码（无 mathlib 依赖），机器编译通过。
2. **否证**：给出一对 m, n 并机器验证二者轨道永不相交（需附带可编译的 Lean 证明或可复跑的计算证据 + 独立论证轨道不相交——后者门槛更高，须说明不可达性的证明而非仅大范围搜索）。

## 规范 Lean 陈述（提交必须逐字保留以下定理签名）

```lean
def tau (n : ℕ) : ℕ := (Nat.divisors n).card

def h (n : ℕ) : ℕ := n + tau n

def iterH : ℕ → ℕ → ℕ
  | 0, n => n
  | (k+1), n => h (iterH k n)

theorem ep414 : ∀ (m n : ℕ), ∃ (i j : ℕ), iterH i m = iterH j n := by
  sorry
```

提交者将 `sorry` 替换为真实证明（或另证其否定并相应调整主定理陈述，但须在提交说明中声明走向）。禁止 `sorry` / `admit` / `native_decide` / 新增公理；允许使用 Lean 4 标准库与 mathlib（若声明 mathlib 依赖，须附可复现构建说明）。

## 数据点（供攻击参考，均可在本地快速复算）

- h 前若干值：1→2, 2→4, 3→5, 4→7, 5→7, 6→12, 7→9, 8→15, 9→13, 10→18 …
- 数列 n+τ(n) 即 OEIS A064491。
- 站方关联问题：#412、#413（同族迭代问题）。

## 诚实条款

- 禁止凭「看起来像证明」提交；一切以编译器判卷。
- 失败尝试同样有价值：结构性观察（轨道分段、汇聚半径数据、碰撞统计）可在提交说明中随附，单独不构成 pass，但计入负观测。
- 本命题书为 correspondence 件：提交代码中 `theorem ep414` 的签名必须与本件规范陈述一致（签名级保真由验证器逐字符比对）。