linhaowei1/sum-diff-proof

# 确定与和集与差集相关的最优指数 这是一个 Lean 4 / [mathlib](https://github.com/leanprover-community/mathlib4) 形式化项目，用于证明 配套论文 [**“确定与和集与差集相关的最优指数”**](paper/settling-the-optimal-exponent.pdf)。 对于满足 `|A| ≥ 2` 的有限整数集 `A`，定义**和/差增长指数** ``` C(A) = log(|A + A| / |A|) / log(|A − A| / |A|) ``` 其中 `A + A` 和 `A − A` 是逐点和集与差集。本仓库证明了： 1. **普遍严格上界。** 对于所有满足 `|A| ≥ 2` 的有限集 `A ⊆ ℤ`，`C(A) < 2`。 2. **上确界恰好为 `2`。** `Sup { C(A) : A ⊆ ℤ finite, |A| ≥ 2 } = 2`。 3. **上确界无法达到。** 没有任何满足条件的 `A` 能使 `C(A) = 2`。 4. **定量见证。** 存在一个显式的有限集合 `A`，满足 `2 − 10⁻⁹⁹⁹ < C(A) < 2`。 上界属于解析部分（通过加性 Plünnecke–Ruzsa / Ruzsa 三角不等式证明）；与之匹配的下界则通过一个显式的 39 进制“列”构造证明，其增长指数收敛于 `2`。 ## 核心定理 所有定理均位于命名空间 `SumDiffExponent` 中（构造引理位于 `Column39` 中）。 | 定理 | 文件 | 命题 | |---|---|---| | `growthExponent_lt_two` | `SumDiffExponent.lean` | `2 ≤ A.card → growthExponent A < 2` | | `tendsto_growthExponent_approximatingSet` | `SumDiffExponentMain.lean` | 显式集合的指数 `→ 2` | | `isLUB_admissibleExponents` | `SumDiffExponentMain.lean` | `IsLUB admissibleExponents 2` | | `sSup_admissibleExponents` | `SumDiffExponentMain.lean` | `sSup admissibleExponents = 2` | | `supremum_not_attained` | `SumDiffExponentMain.lean` | `2 ≤ B.card → growthExponent B ≠ 2` | | `quantitative_example` | `SumDiffExponentQuantitative.lean` | 对于显式集合有 `2 − 10⁻⁹⁹⁹ < C < 2` | 其中 `growthExponent A = Real.log (sigma A) / Real.log (delta A)`， `sigma A = |A + A| / |A|`，`delta A = |A − A| / |A|`（作为实数）。 ## 仓库结构 | 模块 | 作用 | |---|---| | `SumDiffExponent.lean` | 问题定义；普遍严格上界；12 进制自动机证书（对手稿的忠实记录，未被最终构造使用）。 | | `SumDiffExponentColumn.lean` | 对 kernel 友好的 39 进制块 `V`；有限证书 `V + V = range 39` 和 `|V − V| = 37`。 | | `SumDiffExponentConstruction.lean` | 显式的行/列集合 `A l` 及其和/差集势的界限。 | | `SumDiffExponentLimit.lean` | 渐近下界 `exponentLower l → 2`。 | | `SumDiffExponentMain.lean` | 收敛于 `2`，最小上界 / 上确界定理，以及不可达性。 | | `SumDiffExponentQuantitative.lean` | 显式的 `10⁻⁹⁹⁹` 见证。 | | `scripts/CheckAxioms.lean` | 打印核心定理的公理占用情况（见下文）。 | ## 环境要求 * [`elan`](https://github.com/leanprover/elan)（Lean 工具链管理器）。确切的 Lean 版本 —— **`leanprover/lean4:v4.32.1`** —— 固定在 `lean-toolchain` 中，并且会在首次使用时由 `elan` 自动安装。 * 需要互联网连接以下载 mathlib olean 缓存（几个 GB），而不是从源码编译 mathlib。 * 需要约 8 GB 的可用磁盘空间，用于构建目录 `.lake/`。 依赖项固定为 `lake-manifest.json` 中的确切提交（mathlib `v4.32.1`， 提交 `520045a…`），因此构建是可复现的。 ## 构建与复现 如果尚未安装 `elan`，请先安装： ``` curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y source "$HOME/.elan/env" ``` 然后，在仓库根目录下执行： ``` lake exe cache get # download the pinned mathlib oleans (fetches deps on first run) lake build # compile all six modules — this is the verification ``` 成功运行将以 `Build completed successfully` 结束。Lean 会对任何 `sorry` 发出警告；无警告的干净构建意味着代码中不存在 `sorry`。 ### 检查公理占用 ``` lake env lean scripts/CheckAxioms.lean ``` ## 验证状态 * `lake build` 成功完成（2212 个任务）；**没有 `sorry`** 且 **没有 `warning`**。 * 公理占用（`#print axioms`，由 `scripts/CheckAxioms.lean` 复现）： * `growthExponent_lt_two` 和 `supremum_not_attained` 仅依赖于三个 标准的 mathlib 公理 `propext`、`Classical.choice`、`Quot.sound` —— 解析 上界部分已完全通过 kernel 检查。 * `sSup_admissibleExponents`、`isLUB_admissibleExponents`、 `tendsto_growthExponent_approximatingSet` 和 `quantitative_example` 额外 依赖于**三个 `native_decide` 证书**： `V_card_certificate`、`V_sum_certificate`、`VDiff_card_certificate` （即针对 12 元素的 39 进制块 `V` 的事实 `|V| = 12`、`V + V = {0,…,38}`、`|V − V| = 37`）。 ### 信任基说明 `native_decide` 通过将目标编译为本地代码并运行它来证明目标， 这将 Lean 编译器和本地执行加入了可信计算基（这就是为什么这些定理 带有额外的生成公理，而不是完全由 kernel 独立闭环证明的原因）。在此项目中，它 仅用于上述列出的三个基本有限计算；每一个都是关于 12 元素集合的、 可独立检查的小事实。`SumDiffExponent.lean` 中的 12 进制自动机证书也使用了 `native_decide`，但**并没**有作为最终定理的支撑（它们不在上述的公理占用中）。 ## 来源与致谢 底层的有限集构造是在 [Hyra](https://hy.tencent.com/research/hyra) 的协助下开发的，Hyra 是来自腾讯混元 的 AI 研究智能体（基于 Hy3 模型）。 本仓库给出了该**尖锐**命题的机器可检验 Lean 4 / mathlib 证明 —— 即对于*每一个*符合条件的集合，其增长指数 `< 2`，其在所有此类集合上的上确界为 `2`，且永远无法达到 `2` —— 证明中使用了论文中 12 进制构造的一个对 kernel 友好的 39 进制变体（12 进制自动机保留在 `SumDiffExponent.lean` 中，作为 手稿的忠实记录，但不作为最终定理的承重部分）。 ## 引用 ``` @misc{lin2026settling, title = {Settling the Optimal Exponent Relating Sumsets and Difference Sets}, author = {Lin, Haowei and Li, Shanda}, year = {2026}, } ``` ## 许可证 根据 [Apache License, Version 2.0](LICENSE) 授权 —— 这是 mathlib 及 Lean 生态系统大部分内容所使用的 许可证。归属信息记录在 [`NOTICE`](NOTICE) 中。

标签：Lean 4, mathlib, 加性组合数学, 定理证明, 形式化验证, 数学证明