结果族 331：Reflexive midpoint convexity and diamond distortion · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
两枚同样大的硬币交叠，公共部分是一枚”透镜”。在无穷维空间里，透镜收集的是所有”以 @@M@@x@@ 为中点、两端都不越出半径 @@M@@R@@“的位移。这篇论文对两棵无穷大的家谱树造出的空间证明了一条干净的几何事实：中心 @@M@@x@@ 越贴近球面，透镜在扔掉任意有限多个坐标之后剩下的”尾巴”就越薄，按平方根的速度收缩。这条尾巴不等式是整个结果族的发动机。
关键词卡片
@@M@@\{y:\|x+y\|\le R,\ \|x-y\|\le R\}@@，两个球相交的公共部分。@@M@@H@@ 后，剩余部分 @@M@@Q_Hy@@ 的大小上界。看个具体例子
主不等式 @@M@@\|Q_Hy\|\le2\sqrt{R^2-\|x\|^2}@@，取 @@M@@R=1@@ 代入具体数字：@@M@@\|x\|=0.8@@ 时尾部 @@M@@\le2\sqrt{0.36}=1.2@@；@@M@@\|x\|=0.99@@ 时尾部 @@M@@\le2\sqrt{1-0.9801}\approx0.28@@；@@M@@\|x\|\to1@@ 时尾部趋于 @@M@@0@@。中心只差百分之一贴到球面，尾巴就被压掉四分之三以上——无论位移 @@M@@y@@ 怎么选、扔掉的坐标集 @@M@@H@@ 怎么选都成立。
为什么值得关心
这条尾部不等式正是姊妹篇把菱形失真下界改进到 @@M@@\sqrt{1+k/4}@@ 的直接输入；AMUC 与 AUC 的分界线又被精确地画深了一笔。
主结果已 Lean 形式化
第一级台阶
导读用”两枚硬币交叠出透镜”讲对称透镜：收集一切以 x 为中点、两端不越出半径 R 的位移。拧紧一点：对象是两棵无穷大家谱树造出的线性空间；操作是把有限多个”头部坐标”投影扔掉，再看透镜里位移还剩多长的”尾巴”。要证的直觉是：中心 x 越贴近球面，凸性把透镜远方压得越薄，且按平方根速度收缩。
第二级台阶
用本科术语说：对称透镜 L(x,R)={y:‖x+y‖≤R, ‖x−y‖≤R}，即两个 R-球的交集沿中点 x 的切片；P_H 与 Q_H 分别是向有限祖先集 H 的坐标投影及其余投影。两个模型空间：高度有限但无界的树森林在线段范数 ρ(u)=sup(Σu(Sᵢ)²)^{1/2}（sup 取遍两两不交线段）下的对偶 X=J*，以及无穷树上闭坐标张成的预对偶 B∞。渐近中点一致凸（AMUC）指扔掉任意有限维方向后中点版圆度仍在。
第三级台阶
主定理（联合预算）的语境：Y 取 X 或 B∞ 之一，假设仅是 x=P_Hx（中心有限支撑）与 y∈L(x,R)——”同一个头部 H 控制透镜中一切位移”正是单个中心面对无穷多候选中点时需要的强度。结论：‖Q_Hy‖≤2√(R²−‖x‖²)。推论三件套：两个给定范数的显式平均渐近中点模下界，故皆 AMUC；两个空间都换不出等价的 AUC 范数（根路径泛函提供逐层摊平的方向）；有限高森林对偶 X 自反。
对有限高线段森林对偶 @@M@@X=J^*@@ 与无穷高坐标预对偶 @@M@@B_\infty@@ 两个 James 树型空间，证明对称透镜中任意位移的尾部满足 @@M@@\|Q_Hy\|\le2\sqrt{R^2-\|x\|^2}@@；两个范数均渐近中点一致凸，却都无等价渐近一致凸范数。
对范数空间 @@M@@Y@@、向量 @@M@@x@@ 与半径 @@M@@R@@，对称透镜 (symmetric lens) @@M@@\mathcal L(x,R)=\{y:\|x+y\|\le R,\ \|x-y\|\le R\}@@ 收集以 @@M@@x@@ 为中点、两端点都在 @@M@@R@@-球内的一切偏差。当 @@M@@\|x\|@@ 接近 @@M@@R@@ 时凸性会压缩透镜；在无穷维空间里可以问：投影掉有限多个坐标后透镜还剩多大。Dilworth–Kutzarova–Randrianarivony–Revalski–Zhivkov（2016）正是用近似中点透镜的非紧性刻画渐近中点一致凸性 (asymptotic midpoint uniform convexity, AMUC)。Perreau（2021）进一步提问：可数分支 James 树空间的典则预对偶是否 AMUC？本文研究两个模型——高度有限但无界的树森林在线段范数下的对偶 @@M@@X=J^*@@（自反）与无穷树 @@M@@T_\infty=\mathbb N^{<\omega}@@ 上的闭坐标张成 @@M@@B_\infty\subset J_\infty^*@@（Ghoussoub–Maurey–Schachermayer 式坐标预对偶）——并对两者证明统一的尾部估计。作为对照，Girardi 曾证明经典二元 James 树空间的预对偶与全对偶都是 AUC 的；本文改用可数分支与有限而无界的分量高度，呈现出截然不同的行为，且局部相消估计均为本文就所给范数直接证明，而非从二元树结果移植。
主定理（联合预算）：设 @@M@@Y@@ 为 @@M@@X=J^*@@ 或 @@M@@B_\infty@@ 之一，@@M@@H@@ 为有限祖先集 (ancestral set)，@@M@@x=P_Hx@@，且 @@M@@\|x\pm y\|\le R@@，则
@@M@@D\|Q_Hy\|\le2\sqrt{R^2-\|x\|^2}.@@
关键是同一个头部 @@M@@H@@ 控制透镜中的一切位移——这正是单个中心拥有无穷多个可能中点时所需要的性质。推论由此给出两个模型的显式平均渐近中点模，故两个给定范数都 AMUC；同时两个空间都无可重赋范 (renormable) 的等价 AUC（渐近一致凸, asymptotically uniformly convex）范数；且有限高森林对偶 @@M@@X@@ 自反。
先建原子表示：有限头部 @@M@@P_HB_\infty@@ 的单位球恰是”表示原子”@@M@@\sum_i a_id_{S_i}@@（@@M@@d_S@@ 为不相交线段 (segment) 上的示性泛函、@@M@@\sum_i a_i^2\le1@@）的凸包，Carathéodory 定理保证至多 @@M@@|H|+1@@ 个原子的有限表示；@@M@@H@@ 之外则按门 (gate) 分解为 @@M@@\ell_2@@ 直和。证明核心是联合预算论证：把两个端点 @@M@@x\pm y@@ 表示为原子的凸组合，再以等概率随机符号 @@M@@\sigma@@ 混合成一个随机原子 @@M@@A@@，使 @@M@@\mathbb EA=x@@、@@M@@\mathbb E(\sigma A)=y@@；然后用近乎赋范头部的测试 @@M@@p@@（@@M@@x(p)=r=\|x\|@@）预测每个原子系数，即把 @@M@@a_i@@ 换成 @@M@@b_i=rp(S_i)@@。这一替换产生两笔非负误差：系数误差 @@M@@V=\sum_i(a_i-b_i)^2@@ 与未用尽的头部测试能量 @@M@@L=r^2-\sum_ib_i^2@@，而二者期望之和恰好被平方半径亏损控制：@@M@@\mathbb EV+\mathbb EL\le R^2-r^2@@。真正的难点在相消：两个原子若从头部同一顶点离开且带相反符号的和，则它们的头线段必然嵌套，把较长者切开会增大其平方线段测试，于是反号乘积被测试”未满一”的差额吸收；由此得到门口质量估计 @@M@@\|m\|_2\le\sqrt{\eta+2\theta}@@（其中 @@M@@m(g)=\mathbb E|b(g)|@@，@@M@@\eta=\mathbb EV@@、@@M@@\theta=\mathbb EL@@）。最后每个锥上的项范数不超过 @@M@@m(g)@@，锥的 @@M@@\ell_2@@ 分解给出 @@M@@\|Q_Hy\|\le\sqrt\eta+\sqrt{\eta+2\theta}\le2\sqrt{R^2-r^2}@@。至于 AUC 障碍，则利用空间的另一特征：根路径泛函 @@M@@d_{[o,v]}@@ 范数为 1，而子增量 @@M@@e^*_{v^\frown n}@@ 是弱零 (weakly null) 单位向量；正的单侧渐近模会迫使范数沿路径几何式增长，与路径范数的一致有界矛盾。无穷树上还有不需要迭代的版本：取全体路径范数的上确界 @@M@@M@@，同样的增益论证给出 @@M@@M\ge(1+\gamma)M@@，自相矛盾。
主结果已 Lean 形式化。本篇是族内枢纽：其尾估计正是姊妹篇《Distortion of countably branching diamonds…》推出 @@M@@D^2\ge1+k/4@@ 的直接输入；另一姊妹篇（自反树空间）在 @@M@@X@@ 上用自身的成对引理得常数 @@M@@1/12@@，本篇的联合预算机制更强。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇主结果已形式化，具体常数以论文陈述为准。
问 1：证明中最关键、最脆弱的一步是什么？
（答：第 5 节（joint-budget）的联合预算论证：把端点 x±y 写成原子 Σaᵢd_{Sᵢ} 的凸组合，以等概率符号 σ 混合出随机原子 A 使 EA=x、E(σA)=y，再用近乎赋范头部的测试 p 把系数 aᵢ 预测成 bᵢ=rp(Sᵢ)，得非负误差 V 与 L，期望之和恰被 EV+EL≤R²−r² 控制。预算恒等式若差一个交叉项，全部下游估计即塌。）
问 2：门口质量估计里的”相消”为什么最难啃？
| （答：两个原子若从头部同一顶点离开且带相反符号的和，朴素乘积会失控；难点在证明头线段必然嵌套、切开较长者会增大其平方测试，反号乘积被”未满一”差额吸收，得 ‖m‖₂≤√(η+2θ)（m(g)=E | b(g) | ）。这步全靠线段范数的嵌套几何，任何一对”同门反号”原子漏检都会让门口质量失控，尾部上界就废了。） |
问 3：为什么必须”同一个 H 控制透镜中一切位移”？逐个 y 换 H 不行吗？
（答：不行。下游（姊妹篇的 D²≥1+k/4）需在同一透镜里同时处理无穷多候选中点位移；若 H 可随 y 变化，透镜非紧性无法统一量化，而 DKRRZ 的 AMUC 刻画正要求一致估计。定理陈述里 x=P_Hx 固定头部、y 任意，正是为”一次预算、全体付款”的强度设计。）
问 4：与 Girardi 的经典 James 树结果为何行为相反？新意是什么？
（答：Girardi 证明二元 James 树空间的预对偶与全对偶都是 AUC；本文改用可数分支与”有限而无界”的分量高度，得到 AMUC 却非 AUC 可重赋范的相反行为，且相消估计就所给范数直接证明而非移植。新意有二：统一的透镜尾不等式（两个模型同时成立）；肯定回答 Perreau 2021 之问。）
问 5：AUC 障碍论证怎么运作？两个空间有何不同？
（答：共同机制是根路径泛函 d_[o,v] 范数为 1 而子增量 e*_{v⌢n} 弱零：若某等价范数的单侧渐近模在正半径有增益 γ，范数沿路径几何式增长，与路径范数一致有界矛盾。无穷树 B∞ 上还有免迭代的版本——取全体路径范数上确界 M，同样增益给出 M≥(1+γ)M，自相矛盾（第 8 节，infinite-obstruction）。）
问 6：这类 AI 证明最可能的出错模式？
| （答：最险的是随机符号混合与 Carathéodory 表示的配合：原子个数至多 | H | +1、期望恒等式 EA=x 与 E(σA)=y 的符号翻转要在凸组合系数下严格成立；其次是”切开增大平方测试”的单调性：线段族若不满两两不交，测试即不控范数。主结果已 Lean 形式化，常数有机器背书，但 20 个小节里支撑性的变体命题仍需人工过目。） |
问 7：谁会用到这条尾不等式？
（答：它就是结果族的发动机：姊妹篇《Diamond distortion》把它当直接输入推出 D²≥1+k/4（把自反树空间篇的 1/12 改进三倍）；更广地，用透镜非紧性刻画渐近凸性、或用菱形/树图失真检验粗嵌入的工作都可引用这条显式平方根收缩；AMUC 与 AUC 的分界线由此多了一块精确参照物。）
总评
把全族最难的技术核做成干净自足定理，覆盖两个模型并回应 Perreau 之问，主结果有 Lean 形式化；最大风险在相消引理的嵌套几何细节——全文唯一无法靠”预算记账”直觉复核的部分。