结果族 167：Planar distinct distances and unit-distance bounds · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
想象操场上站着 @@M@@n@@ 个同学，每人环顾四周，报出”我到大家的距离有多少种不同取值”。这篇论文证明：几乎每个人的答案都大得惊人——距离取值至少有 @@M@@n^{1-\varepsilon}@@ 种，想要多接近 @@M@@n@@ 都行；只能看到很少种距离的”宅点”，占比必然趋于零。这就是 Erdős 1957 年提出、悬置近七十年的钉点不同距离猜想的弱形式，而且结论对一切点集一致成立，不设任何分离性或一般位置假设。
关键词卡片
@@M@@n@@ 个点两两之间能数出多少种互不相同的距离长度@@M@@o(n)@@，即随 @@M@@n@@ 增大占比趋近于零看个具体例子
最天然的例外点是圆心：
定理代入数字：@@M@@n=10^6@@、@@M@@\varepsilon=0.01@@ 时，@@M@@n^{1-\varepsilon}\approx 8.7\times10^5@@——除占比趋零的点外，每个点都各自张出至少约 87 万种互异距离。
为什么值得关心
全局版不同距离问题已被 Guth–Katz 解决，而逐点的钉点版本此前最好结果只有 @@M@@n^{0.864}@@；本文一举推到 @@M@@n^{1-\varepsilon}@@；其工具箱（复坐标分解、数域乘积公式、实闭域转移）与姊妹篇单位距离上界共享，互相印证，且主结果已通过机器核验。
已 Lean 形式化
第一级台阶
入门导读把点集想成操场上的同学，每人报出”我到大家的距离有几种取值”。现在把比喻剥掉一层：对象是平面上有限个点构成的集合，操作是任选其中一个点作观察者，把它到其余各点的距离收集起来、去掉重复、数出不同取值的个数。圆心之所以只报一个数，是因为它与一大批点等距——许多点共享同一个距离值，这种”扎堆”现象正是整个问题的敌人与主角。
第二级台阶
用本科语言精确化：对有限点集 @@M@@P@@ 中的点 @@M@@x@@，距离集 @@M@@D_x(P)@@ 是 @@M@@x@@ 到其余各点欧氏距离的全体取值；与某个点 @@M@@y@@ 同 @@M@@x@@ 等距的点构成一条距离纤维，其规模记作 @@M@@k_P(x,y)@@。论文实际研究的量是 @@M@@F_n(s)@@：在一切 @@M@@n@@ 点集上，随机抽取有序点对时落在规模不小于 @@M@@n^s@@ 的纤维中的比例的最大值——它度量”距离值被多少个点重复使用”。
第三级台阶
主定理断言：固定 @@M@@s>0@@，当 @@M@@n@@ 趋于无穷时 @@M@@F_n(s)@@ 趋于零，且对一切构形一致成立，不设任何分离性或一般位置假设。”固定 @@M@@s@@“挡住了纤维规模随 @@M@@n@@ 增长的病态情形，”一致”挡住了对特殊构形逐一处理的取巧。结论翻译过来：巨大的距离纤维在全体点对中只占消失比例，例外点占比必然趋于零；除这些例外点外，每个点看到的距离取值至少有 @@M@@n^{1-\varepsilon}@@ 个——这正是弱钉点 Erdős 猜想的完整陈述。
证明了弱钉点 Erdős 不同距离猜想：对任何固定 @@M@@\varepsilon>0@@，任何 @@M@@n@@ 点平面点集中除 @@M@@o(n)@@ 个例外点外，每个点都与其余点张出至少 @@M@@n^{1-\varepsilon}@@ 个互异距离——Erdős 1957 年提出的这一公开问题得到肯定解决。
1946 年 Erdős 开创了平面不同距离问题（distinct distances）：@@M@@n@@ 个点的平面点集最少确定多少个互异距离？平方格点集给出约 @@M@@n/\sqrt{\log n}@@ 个距离的构形，Guth 与 Katz 证明了 @@M@@n/\log n@@ 的下界，全局版本基本解决。但”钉点”（pinned）版本要求这些距离共享同一个源点：对 @@M@@x\in P@@ 记 @@M@@D_x(P)=\{\|y-x\|_2:y\in P\setminus\{x\}\}@@，问是否必有点使 @@M@@|D_x(P)|@@ 很大。Erdős 1957 年明确提出了这一弱问题。此前最好结果是 Solymosi–Tóth 的 @@M@@n^{6/7}@@，Tardos 与 Katz–Tardos 借助熵不等式把指数推到 @@M@@0.864137\ldots@@，与完整猜想的目标 @@M@@n/\sqrt{\log n}@@ 相距甚远。卡点在于：Guth–Katz 的全局估计对所有源点取并，无法锁定单个钉点；而”圆周加圆心”的构形中圆心只看到一个距离，说明例外点集天然存在，须证明它只占 @@M@@o(n)@@。
论文核心定理控制”距离纤维”（distance fiber）的规模：对相异 @@M@@x,y\in P@@，令 @@M@@k_P(x,y)@@ 为与 @@M@@y@@ 到 @@M@@x@@ 等距的点数（含 @@M@@y@@ 本身），@@M@@F_n(s)@@ 定义为在一切 @@M@@n@@ 点集上、满足 @@M@@k_P(x,y)\ge n^s@@ 的有序对所占比例的上确界。定理断言：对每个固定 @@M@@s>0@@，@@M@@F_n(s)\to 0@@，且对一切构形一致成立，不设分离性或一般位置假设。由它直接推出推论：对每个固定 @@M@@\varepsilon>0@@，满足 @@M@@|D_x(P)|<n^{1-\varepsilon}@@ 的钉点占比趋于 @@M@@0@@；特别地，每个足够大的 @@M@@n@@ 点平面集必存在一个钉点，张出至少 @@M@@n^{1-\varepsilon}@@ 个互异非零距离。这正是弱钉点 Erdős 猜想的完整陈述。
证明用反证法，分四步推进。
先做极值归约。假设 @@M@@F_n(s)\not\to 0@@，沿近极值序列抽出边密度趋于正数 @@M@@\theta@@ 的有向图，边按（源点、平方距离）分成纤维（fiber），每条纤维大小 @@M@@\ge n^{s-o(1)}@@，并附带一条子集估计：小集合抓不住多少纤维质量。再用实闭域的转移原理（transfer for real closed fields）把坐标替换为实代数数，一切距离等式与不等式原样保留。
再搭建算术引擎。取包含全部坐标的数域 @@M@@K@@，令 @@M@@Z_1=u+\mathrm{i}v@@、@@M@@Z_2=u-\mathrm{i}v@@，则平方距离分解为 @@M@@\|x-y\|_2^2=(Z_1(y)-Z_1(x))(Z_2(y)-Z_2(x))@@，于是在一条等距纤维上第二坐标是第一坐标的分式线性函数。归一化乘积公式（product formula）@@M@@\sum_v\sigma_v\log|z|_v=0@@ 表明两个坐标的对数深度在所有绝对值上加权平衡。为把它变成有限恒等式，在每个位上构造嵌套分割（nested partitions）：有限位由超度量不等式免费给出；复嵌入处用随机平移、随机旋转的嵌套方格网（Arora 式随机剖分），其共享深度与真实深度之误差与点对无关且指数衰减。把质量超过 @@M@@n/2@@ 的巨胞（giant）换成补集后积分，得到加性重叠恒等式 @@M@@L^*(x,y)=b_*+S^*(x)+S^*(y)@@——凡总质量与两边际之和皆为零的符号测度，对 @@M@@L^*@@ 的积分严格为零。
接着做方差估计。构造符号测度 @@M@@P_B-2R_B+\pi@@，它恰好零总质量、零边际和，代入上述恒等式并对胞概率展开，得到纤维质量 @@M@@p@@ 与均匀质量 @@M@@a@@ 之差的平方 @@M@@(p-a)^2@@ 加上显式的有限总体修正。关键在于全程只采样相异点对：单点胞上的三项概率严格相消，无穷的单点层尾从不被积分。结论是纤维律与入边条件律都逼近均匀律到 @@M@@o(W+1)@@，其中 @@M@@W@@ 为总重叠尺度。
最后按 @@M@@W@@ 二分排除。若 @@M@@W\to\infty@@，保留质量与补质量都有下界的胞并组织成加权有根树；纤维方程把一棵树中源到目标的距离折算成另一棵树中只依赖目标的根到目标距离，树上传输（transport on trees）再把到达同一目标的两源替换为独立均匀点，于是两距离之差的期望可忽略，与树上距离的初等几何下界矛盾。若 @@M@@W@@ 有界，则选取方差最小的复嵌入并归一化坐标，使均匀坐标律收敛到非原子极限 @@M@@\beta_1,\beta_2@@；纤维方程逼出一族 Möbius 变换把 @@M@@\beta_1@@ 映为 @@M@@\beta_2@@，而第一个源坐标与整个目标对独立，令其逼近目标坐标，对数距离差在概率中塌缩，但像点的对数目标距离律即使允许加性常数也有正散布——矛盾。两种情形皆不可能，定理得证。
本文主定理及推论已有 Lean 形式化证明，验证等级在同族中最高。姊妹篇《A power saving for planar unit distances》从单位距离上界一侧使用同一套”复坐标分解＋数域乘积公式＋实闭域转移”工具箱，两文互相印证技术路线；但该姊妹篇本身尚未形式化。按 OpenAI 官方声明，未经形式化的结果可能有问题，而本文主结果已通过机器核验。
问 1：整个证明最要害、也最脆弱的一步在哪里？
（答：是”加性重叠恒等式”。论文把数域乘积公式在每个位上经嵌套分割——有限位用超度量、复嵌入处用 Arora 式随机方格网——变成有限恒等式 @@M@@L^*(x,y)=b_*+S^*(x)+S^*(y)@@，引言明确称之为”算术在证明中的主要用途”。它之所以成立，全靠随机网格的误差是”与点对无关的均值加性误差”这一特殊性质；若误差依赖点对，乘积公式的消去立刻失效。）
问 2：例外集 @@M@@o(n)@@ 能不能去掉？
（答：不能，论文自己给出反例：圆周加圆心的构形中，圆心只看到一个非零距离，故任何一致结论必有例外。但要注意引言明言定理”不提供显式衰减率”——@@M@@o(n)@@ 与 @@M@@F_n(s)\to0@@ 都是定性陈述，距离定量应用还有一步之遥。）
问 3：比起 Katz–Tardos 的指数 @@M@@0.864@@，真正的新意是什么？
（答：不止把指数从 @@M@@0.864@@ 推到 @@M@@1-\varepsilon@@。以往结果（Solymosi–Tóth、Tardos、Katz–Tardos）只保证”存在一个好钉点”，本文定理控制的是每个钉点处的距离重数（@@M@@F_n(s)\to0@@），从而得出”几乎每个点都是好钉点”的推论。方法上也换了赛道：不再沿关联几何加熵不等式推进，而用实闭域转移加数域乘积公式。）
问 4：这个证明最可能以什么模式出错？
（答：最脆弱处在转移原理之后的随机网格误差分析与”只用相异点对”的处理：引言强调单点胞会穿过无穷多层水平，”即使很小的对角误差也无法被积分”，无穷尾估计恰是 AI 生成证明最容易悄悄出错的地方。缓解因素是主定理已有 Lean 形式化，机器核验覆盖了这条主链。）
问 5：不设分离性、一般位置假设，是省事还是困难？
（答：恰是困难所在，也是定理的强度。结论对所有构形一致，意味着证明必须对格点、圆周、聚簇等病态构形一视同仁——这正是需要把坐标转移到实代数数、借助算术而非几何特殊性的原因之一；转移动理保留全部距离等式与不等式。）
问 6：谁会用到它，下一步是什么？
（答：直接推论是每个足够大的点集必有钉点张出至少 @@M@@n^{1-\varepsilon}@@ 个距离；更值钱的是工具箱——同一套复坐标分解、乘积公式、实闭域转移在姊妹篇单位距离上界中复用，两文互相印证。完整钉点猜想（@@M@@n/\sqrt{\log n}@@ 量级）仍开放，本文是弱形式。）
总评
这是把 Erdős 1957 年弱钉点猜想一次推到近乎最优、且主结果经机器核验的工作；最大风险不在主定理本身，而在技术细节向尚未形式化的姊妹篇传播时的可信度。