结果族 331：Reflexive midpoint convexity and diamond distortion · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
把一张越编越细的钻石网塞进一间屋子，网眼不可避免被拉扯，拉扯的最小倍数叫失真。这篇论文证明：深度 @@M@@k@@ 的钻石图塞进两类”家谱树”空间，无论怎么塞，失真的平方至少是 @@M@@1+k/4@@——网越深，越塞不平。它从两条彼此独立的路线（借透镜的尾部账本、直接计算树的能量）得到同一个常数，比姊妹篇的 @@M@@1/12@@ 更好。
关键词卡片
@@M@@k@@ 次得到的图。@@M@@D\gtrsim\sqrt{k}@@。看个具体例子
主定理的数字版：任何失真 @@M@@D@@ 嵌入满足 @@M@@D^2\ge1+\dfrac{k}{4}@@，代入三个深度：
@@M@@Dk=4\Rightarrow D\ge\sqrt2\approx1.41,\qquad k=16\Rightarrow D\ge\sqrt5\approx2.24,\qquad k=100\Rightarrow D\ge\sqrt{26}\approx5.10@@
对比姊妹篇常数 @@M@@1/12@@：同样 @@M@@k=16@@ 只能推出 @@M@@D\ge\sqrt{7/3}\approx1.53@@，新常数把下界抬了一大截。论文还对一批树范数各给门槛：线性路径费用范数上从 @@M@@D^2\ge1+k/484@@ 经弱零配对改进到 @@M@@D^2\ge1+k/16@@，二次路径费用 @@M@@D^2\ge1+k/49@@，起点费用 @@M@@D^2\ge1+k/64@@，不可比线段范数上甚至是指数式障碍——这些范数下整族菱形都无法一致有界地嵌入。
为什么值得关心
它精确标定了”中点凸性能阻止多大的度量嵌入”，是 Ribe 纲领把线性几何翻译成图论量词的定量样本。
主结果已 Lean 形式化
第一级台阶
导读把菱形失真比作”把越编越细的钻石网塞进屋子，网眼被拉扯的最小倍数”。拧紧一点：对象是一族迭代生成的图——从一条单位边出发，每步把每条边换成可数条总长不变的两边路径——以及两类由家谱树造出的线性空间；操作是把图嵌入空间并结算边长被拉伸与压缩之比。要证的是：网越深，最优塞法也躲不开按幂律增长的拉扯。
第二级台阶
| 用本科术语说：归一化菱形 D_k 的每条替换边的长度取父边之半，d_k 为其最短路度量；映射 f 失真至多 D 指存在尺度 s>0 使 s·d_k(u,v)≤‖f(u)−f(v)‖≤Ds·d_k(u,v)。目标空间 X=J* 是有限高森林上不相交线段平方和范数 ρ(a)=sup(Σ | Σ_{S_j}a_s | ²)^{1/2} 的完备化的对偶；B∞ 是无穷树上坐标泛函闭张成的预对偶。对称透镜 {z:‖x±z‖≤R} 收集以 x 为中点、两端在球内的位移。 |
第三级台阶
主定理的语境：对每个整数 k≥0，任何失真 D 的嵌入进入 X 或 B∞ 都被检验——假设只有”边替换处两半边中点彼此远离”这一图结构本身，空间侧的全部几何浓缩在姊妹篇的尾不等式（‖p±y‖≤R 且 p=P_Hp 蕴含 ‖Q_Hy‖≤2√(R²−‖p‖²)，对一切位移 y）里。结论：D²≥1+k/4，系数 1/4 来自完整保留二次预算；配套的直接路线绕开中点模，用树能量自建账本，另对路径费用、起点费用、递归树范数等一批刻度给出幂型乃至指数式障碍。
从透镜尾估计与直接树能量两条路线给出可数分支菱形图的定量失真下界：深度 @@M@@k@@ 的菱形嵌入线段森林对偶或无穷高坐标预对偶均满足 @@M@@D^2\ge1+k/4@@；对路径费用、起点费用与递归树范数也得到幂型障碍。
菱形图 (diamond graph) @@M@@\mathcal D_k@@：从一条单位边出发，每一步把每条边替换为可数条总长不变的两边路径。一个 Banach 空间能否以一致有界的失真 (distortion) 嵌入整族 @@M@@\mathcal D_k@@，是度量嵌入与范数凸性之间的接口：Lee–Naor 与 Johnson–Schechtman 对（有限）二元菱形分别建立了凸性损失求和与模自改进方法；Baudier 等（2017）证明渐近中点一致凸 (AMUC) 范数排除可数分支菱形的一致嵌入，并给出”中点模 @@M@@\gtrsim t^p@@ ⇒ 失真 @@M@@\gtrsim k^{1/p}@@“的定量传递。本文系统追问：每次边替换中究竟哪个量在减少，所得失真下界又如何依赖于证明所用的几何量——并给出不经过中点模的直接能量证明。
主定理：对每个整数 @@M@@k\ge0@@，@@M@@\mathcal D_k@@ 到 @@M@@X=J^*@@（有限高线段森林的对偶，James 不相交线段范数）或 @@M@@B_\infty@@（无穷高坐标预对偶）的任何失真 @@M@@D@@ 嵌入满足 @@M@@D^2\ge1+k/4@@。此外对一批树范数得到幂型下界：线性路径费用范数 @@M@@X_{\rm lin}@@ 上 @@M@@D^2\ge1+k/484@@，用弱零 (weakly null) 配对可改进到 @@M@@D^2\ge1+k/16@@；二次路径费用范数 @@M@@D^2\ge1+k/49@@；线段起点费用范数 @@M@@D^2\ge1+k/64@@；不可比线段范数上 @@M@@k\le(\sqrt2+\sqrt6)^2D(D-1)@@ 且指数式 @@M@@D^{-1}\le\rho^k@@；递归上数组范数 @@M@@X_{\mathrm v}@@（子聚合指数 @@M@@p_h=1+1/h@@）上 @@M@@c_6k/8\le D^6-D^4@@ 与 @@M@@c_3k/(2\sqrt2)\le D^3-D@@；联合根范数 @@M@@D^{-1}\le(1-\eta(2/D))^k@@，固定零根范数 @@M@@k\le4608D^3(1-D^{-1})@@。这些结论各自排除相应范数下的一致有界失真嵌入。
迁移路线的骨架是”配对—透镜—求和”。输入是姊妹篇的尾估计：头部中心 @@M@@p=P_Hp@@、@@M@@\|p\pm y\|\le R@@ 时 @@M@@\|Q_Hy\|\le2\sqrt{R^2-\|p\|^2}@@，对任意位移 @@M@@y@@ 成立。先做有限维配对：有界序列 @@M@@(P_Hz_i)@@ 在有限维中全有界，故存在两个偏差的投影任意接近；其半差 @@M@@w=(z_i-z_j)/2@@ 经交叉凸组合仍留在同一透镜 (lens) 内且尾部不小，代入尾估计后令误差 @@M@@\eta\downarrow0@@，得透镜引理 @@M@@\|x\|^2+\varepsilon^2/16\le R^2@@。再令 @@M@@R_j@@ 为第 @@M@@j@@ 层边斜率范数的上确界：每条父边的斜率都是一个 2-分离透镜的中心，故 @@M@@R_j^2+1/4\le R_{j+1}^2@@；结合 @@M@@R_0\ge1@@、@@M@@R_k\le D@@ 逐层求和即得 @@M@@D^2\ge1+k/4@@——系数 @@M@@1/4@@ 来自完整保留二次预算。直接路线则绕开中点模：其一在头部之外的”新根”处放置修正，以每步至多 16 的平方测试代价换取 @@M@@1/(4D)@@ 的赋值增量，累计 @@M@@k@@ 步后与范数至多 @@M@@4\sqrt k@@ 的最终测试比较得 @@M@@k\le256D^2@@；其二按二进尺寸分箱平衡前缀和，随机下降中期望赋值每步至少增 @@M@@1/16@@ 而总测试范数不超过 @@M@@9\sqrt k@@，故 @@M@@D>\sqrt k/144@@；其三把选定的斜率做成公平二进鞅 (martingale)，终点由不相交线段原子精确表示，其系数的条件期望在 @@M@@L^2@@ 中正交、总预测能量不超过 1，把 @@M@@k@@ 层划分为区间后，用线段端点或线段起点计数找到预测能量无法支撑全部新坐标层的区间，导出矛盾。其余范数上的应用则是把配套论文（有界树位势、递归位势）的内蕴估计经幂型与收缩传递规则转成图论结论。
主结果已 Lean 形式化。本篇的 @@M@@1/4@@ 常数依赖姊妹篇《Midpoint lenses in segment spaces》的联合预算定理，并把另一姊妹篇（自反树空间）在 @@M@@X@@ 上的 @@M@@\sqrt{1+k/12}@@ 改进为 @@M@@\sqrt{1+k/4}@@；其余范数的输入引自配套的树位势与递归位势论文。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇主结果已形式化，各常数以论文陈述为准。
问 1：证明最关键、最脆弱的一步是什么？
（答：迁移路线的”配对—透镜—求和”链条：投影 (P_Hz_i) 在有限维中全有界，两偏差投影可任意接近，半差经交叉凸组合留在同一透镜且尾部不小，代入尾估计令 η→0 得透镜引理 ‖x‖²+ε²/16≤R²；令 R_j 为第 j 层边斜率上确界，每条父边斜率都是 2-分离透镜的中心，得 R_j²+1/4≤R_{j+1}²。最脆是配对：无穷多中点像必须正确配对，配错则 ε²/16 无从谈起。）
问 2：1/4 这个系数从哪来？为什么比姊妹篇的 1/12 好？
（答：引言明言系数 1/4 来自”完整保留二次预算”：尾不等式本身是平方账（2√(R²−‖p‖²)），透镜引理把它转成 R² 的逐层亏损 ε²/16 折算 1/4。自反树空间姊妹篇的成对引理损耗大只得 1/12；本文借更强的联合预算尾估计捡回三倍余量。）
问 3：可数分支相对二元菱形多买了什么？
（答：Lee–Naor 与 Johnson–Schechtman 的二元菱形靠凸性求和与模迭代；可数分支让”无穷多中点像先投影到固定有限维再配对”成为可能——二元每层只有两个候选。引言称之为 further selection，透镜引理依赖它，也是定量改进的结构来源。）
问 4：直接路线为什么值得另起炉灶？风险有何不同？
（答：直接证明不调用姊妹篇的中点不等式，自建能量账本：新根修正以每步 ≤16 的平方测试代价换 1/(4D) 赋值增量，累计 k 步与范数 ≤4√k 的最终测试比较得 k≤256D²；或按二进尺寸分箱、随机下降期望每步增 1/16；或把选定斜率做成公平二进鞅，用 L² 正交预测能量导出矛盾。风险：各证明带显式常数（16、9√k、144 等），系数膨胀即吃掉幂指数，应逐条核算。）
问 5：这类 AI 生成的多路线证明最可能的出错模式？
（答：一是常数口径不一——中点模 max 版与平均版（DKRRZ 等用 max、Baudier–Lancien 用平均）混用，会让”平均⇒max”的方向用反；二是配对紧性与交叉凸组合的次序，凸组合系数若破坏透镜成员资格，尾估计前提失效。主定理已 Lean 形式化；其余范数上的应用是经幂型传递规则组合配套论文的产物，核验范围需逐项确认。）
问 6：附带范数上的结果各自说明什么？
（答：线性路径费用范数从 D²≥1+k/484 经弱零配对改进到 1+k/16，可见配对技术有余量；二次路径费用 1+k/49、起点费用 1+k/64；不可比线段范数上更强，得指数式障碍 D⁻¹≤ρ^k；递归上数组范数得 c₆k/8≤D⁶−D⁴ 等。结论统一：这些范数下整族菱形无一致有界失真嵌入。）
问 7：谁会用到这些下界？
（答：Ribe 纲领的定量侧：菱形失真是把线性凸性翻译成图论量词的标准汇率，本文给出该汇率在两类 James 型空间上的精确牌价 D≳√k；做粗嵌入、度量紧性与非线性几何分类的人可直接引用；弱零配对改进也是可复用技巧。）
总评
把族内透镜尾估计兑现成全族最好的菱形失真常数，并以独立直接路线交叉印证同一幂律，定量功底扎实且有 Lean 背书；最大风险在多组显式常数与两种中点模口径的穿梭使用——那部分属人工核验地带。