结果族 331：Reflexive midpoint convexity and diamond distortion · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
给向量”量长度”的规则（范数）本身就是一件可以设计的东西。这篇论文在一棵能无穷分叉的树上立规矩：任何一条从根出发的路径，沿途系数的累加和都必须夹在 @@M@@[-1,1]@@ 里。用这条规矩当尺子，造出一批新的无穷维空间。反直觉的结论是：这些尺子在”中点”意义下是凸的，可无论换成哪把功能等价的新尺子，都得不到更强的”渐近一致凸”——两种凸性被证明可以彻底分家，而且分家发生在最温和的自反空间里。
关键词卡片
看个具体例子
在有限高的树上，这套尺子有一本干净的账：向量 @@M@@x@@ 的长度 @@M@@L_n(x)=\inf\big(\|h\|_2+\|\mu\|_1\big)@@，即把 @@M@@x@@ 拆成”一个欧氏向量加若干条根路径”的最小总成本。中点凸性则有显式曲线：取 @@M@@t=0.8@@，中点模 @@M@@\widehat\delta(0.8)\ge\sqrt{1+0.8^2/4}-1\approx 0.077@@，也就是说中点至少往球内压这么多。
为什么值得关心
“弱凸性能否靠换尺子升级成强凸性”是 2016 年提出的公开问题，本文给出了包含自反反例在内的一族最干净答案，把两种凸性的分离推进到自反世界。
已 Lean 形式化
第一级台阶
导读里把范数比作”量长度的尺子”。落实到本文：对象是一棵能无穷分叉的树上各结点处的实数系数，一个向量就是给有限多个结点各配一个数；”量长度”的操作，是拿一族合法的加权方案去逐点乘上系数再求和，取能取到的最大值。合法性由树的结构说了算。
第二级台阶
合法加权方案要过两道关：一是沿任何一条从根出发的路径，系数的累加和（位势）必须夹在 −1 与 1 之间；二是系数还要满足某种平方和预算，比如同一层兄弟之间、每条有限反链上、或全局的平方和有界。所有合法方案的集合记作测试集 K，定义范数 ‖x‖K = sup{f∈K} Σ f_s x_s，取完备化得到 Banach 空间 X_K。凸性的强弱用渐近模度量：在有限余维子空间里取范数不小于 1 的远方向 y，看 x±ty 两端范数平均超出 1 多少，下确界记为 δ̂(t)；更强的单侧版本恒正即为渐近一致凸（AUC）。
第三级台阶
定理在可数分支树上陈述：按兄弟、含根兄弟、反链、全局四种二次约束各造一个测试集，得到四个实 Banach 空间。结论两半：其一，每个空间一致满足 δ̂(t) ≥ √(1+t²/4) − 1，即中点处平均必有增益——位势夹逼假设挡住的麻烦，是规范性测试的位势顶在边界时尾部无法自由扰动；其二，任何等价范数都无法让单侧模变正，因为路径向量组成一棵有界的弱零增量树，封死了再赋范的出路。再把成本换成欧氏组合或按起点计费的线段，得到两个自反空间，把这一分离现象推进到最规矩的空间类别。
本文用可数分支树上的有界位势（bounded tree potential）显式构造出多个 Banach 空间：它们的平均渐近中点模满足 @@M@@\widehat\delta(t)\ge\sqrt{1+t^2/4}-1@@，却都不容许任何等价的渐近一致凸范数；其中二次路径空间与线段起点空间还是自反的，把 Baudier 的 AMUC/AUC 分离现象推进到自反空间。
渐近中点一致凸（AMUC）是否在再赋范意义下等价于渐近一致凸（AUC），是 Dilworth–Kutzarova–Randrianarivony–Revalski–Zhivkov（2016）提出的公开问题。Baudier 等人 2017 年证明：对具无条件渐近结构的可分自反空间二者等价，于是”无结构假设的自反反例”长期悬置（Perreau 2021 年仍记录为开放）。Baudier 2026 年借 Kadets–Werner 的 Daugavet 例子给出一般否定回答，但那个例子具 Schur 性质、非自反。卡在何处：如何在自反空间里同时实现”中点有增益”与”一切等价范数都非 AUC”这两件方向相反的事。本文的切入点是把两种效应都归结为树上路径的标量约束：路径和有界既挡住单侧凸性，系数的二次预算又允许中点两侧配对增益。
设 @@M@@T=\mathbb N^{<\omega}@@ 为可数分支树，系数族 @@M@@f@@ 的位势为 @@M@@P_f(s)=\sum_{u\preceq s}f_u@@。取测试集 @@M@@K@@：要求 @@M@@|P_f(s)|\le1@@，再附加四种二次约束之一——兄弟组约束（@@M@@K_{\rm s},K_{\rm p}@@，后者含根坐标）、有限反链约束（@@M@@K_{\rm a}@@，antichain）或全局 @@M@@\ell_2@@ 约束（@@M@@K_{\rm g}@@）。范数取 @@M@@\|x\|_K=\sup_{f\in K}\sum f_sx_s@@，完备化得 @@M@@X_K@@。定理证明：四个空间都是可分无限维实 Banach 空间，且对 @@M@@0<t<1@@ 一致满足 @@M@@\widehat\delta(t)\ge\sqrt{1+t^2/4}-1\ (\ge t^2/16)@@，同时任何一个都不容许等价 AUC 范数。在有限高树 @@M@@T_n=\mathbb N^{\le n}@@ 上，全局约束模型满足精确恒等式 @@M@@L_n(x)=\inf_{x=h+B_n\mu}(\|h\|_2+\|\mu\|_1)@@——即”Hilbert 向量与根路径的最小可加成本”；高度一时恰为 Dilworth 等人的 @@M@@\ell_2@@ 反例。把成本换成欧氏组合得到二次路径空间 @@M@@X_{\rm q}@@，把根路径换成任意起点的线段并按起点计费得到线段起点空间 @@M@@X_S@@：二者都自反、每点半径处最大渐近中点模为正、且无等价 AUC 范数。
中点下界的核心是”成对向内测试”。难点在于：支撑在有限初始集 @@M@@D@@ 内的中心 @@M@@x@@ 的赋范测试 @@M@@f@@，其位势可能已经顶在区间 @@M@@[-1,1]@@ 的边界上，任意的尾部扰动 @@M@@g@@ 会把位势推出区间。解决办法是把尾部测试在每个 @@M@@T\setminus D@@ 分量上的相对位势 @@M@@R(s)@@ 按头部继承值 @@M@@c=P_f(r)@@ 的内侧拆成两个正部 @@M@@U,V@@：@@M@@U-V=R@@ 且都指向区间内部。取符号正部是 1-Lipschitz 的，故新系数逐点被 @@M@@|g_s|@@ 控制，二次约束自动保留；位势界为 2，除以 2 后仍是合法测试。关键一步是验证 @@M@@af+\theta u@@ 与 @@M@@af+\theta v@@（@@M@@a=\sqrt{1-\theta^2}@@）都属于 @@M@@K@@：头部与尾部支撑不相交，任一二次组的预算按勾股式合成 @@M@@a^2+\theta^2=1@@，而位势因”向内”而被夹在 @@M@@[-1,1]@@ 中。把这两个测试分别作用于 @@M@@x+ty@@ 与 @@M@@x-ty@@ 再相加，即得平均 @@M@@\ge a\|x\|_K+\frac{t\theta}{2}g(y)@@，对 @@M@@g@@ 取上确界后选 @@M@@\theta=t/\sqrt{4+t^2}@@ 便得 @@M@@\sqrt{1+t^2/4}@@。配对的好处是无需预先挑端点：对一侧不利的尾部位势恰好为另一侧提供向内测试。排除 AUC 再赋范用的是”有界弱零树”引理：若空间含有一致有界的树 @@M@@(p_s)@@（@@M@@m\le\|p_s\|\le M@@）且子增量 @@M@@d_{s,n}=p_{s^\frown n}-p_s@@ 弱零、范数 @@M@@\ge c@@，则任何等价范数的单侧模在 @@M@@t_0=\alpha c/(2\beta M)@@ 处为零——否则沿树逐层选子节点，凸性迫使范数每步乘 @@M@@(1+\gamma/2)@@，有限层后突破一致上界。四个模型里路径向量 @@M@@p_s=\sum_{u\preceq s}e_u@@ 由位势条件归一，兄弟 @@M@@\ell_2@@ 约束使子增量弱零且范数为 1，引理以 @@M@@m=M=c=1@@ 生效。自反模型 @@M@@X_{\rm q},X_S@@ 的范数等价于 Hilbert 范数故自反；其AMUC靠对偶空间的截断、停止与匹配论证（如尾部估计 @@M@@\|Q_Ay\|\le 8\sqrt{R^2-\|x\|^2}@@、线段空间中 @@M@@\|Q_Ey\|_{\rm I}\le(\sqrt2+\sqrt6)\sqrt{1-\|x\|_{\rm I}}@@），AUC 排除则复用同一弱零树机制。
论文声明主结果已有 Lean 形式化证明。作为结果族 331 的构造主干，它与本族另两篇互补：Daugavet 子空间一篇算出精确模曲线，独立乘积一篇给出 @@M@@L^1@@ 内的随机实现，本文则贡献显式树模型与自反反例，三者共同支撑”中点一致凸不迫使 AUC 可再赋范，即使在自反世界”。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇虽已形式化，文中诸多数值常数（如 @@M@@1/64@@、@@M@@495@@、@@M@@252@@）仍以原文与社区核验为准。
问 1：中点下界证明里最脆弱的一步是什么？
（答：是”向内拆分”。中心 x 支撑在有限头部 D 时，规范性测试 f 的位势可能已顶在 [−1,1] 端点，任意尾部扰动会越界。论文把尾部相对位势按头部继承值拆成两个指向区间内部的正部，利用正部算子 1-Lipschitz 保证新系数逐点被原系数控制、二次预算保留，再按勾股式 a²+θ²=1 合成测试 af+θu 与 af+θv 并验证均属于 K。这一步若 Lipschitz 论证或预算合成有误，整个下界坍塌；引言称四种约束共用同一证明而不逐一辨认范数，恰是核验时最需盯紧之处。）
| **问 2：位势约束 | P_f | ≤1 为什么不能去掉？** |
（答：它承担双重职责。一方面它把路径向量 p_s = Σ_{u≼s} e_u 归一成一致有界的树，是”有界弱零树”引理排除一切等价 AUC 范数的原料；另一方面它是中点测试合法性的边界条件。去掉它，测试集失去沿路径方向的控制，子增量的弱零与范数下界都无法保证，两条主线同时失效。）
问 3：与已有工作相比真正的新意是什么？
（答：Baudier 2026 用 Kadets–Werner 的 Daugavet 例子给出一般否定回答，但该例有 Schur 性质、非自反；Perreau 2021 明确记录无结构假设的自反情形仍开放。本文给出显式树模型，且二次路径空间 X_q 与线段起点空间 X_S 是自反的，模有显式曲线 δ̂(t) ≥ √(1+t²/4)−1，不只是存在性论证。）
问 4：这类 AI 生成证明最可能出错的模式是什么？
（答：一是数值常数：文中出现 495、252、1/64、(√2+√6)、8、7 等大量手工常数，集中在鞅能量估计与截断论证（如 thm:quadratic-tail、thm:segment-start-tail），逐项核验成本高；二是组合推理在四种约束变体（兄弟、含根、反链、全局）与含根坐标、线段缩短等边角情形下的逐一适配，容易漏case。论文声明主结果已 Lean 形式化，但能量估计等辅助章节是否被形式化覆盖，文中未逐一说明。）
问 5：恒等式 L_n(x) = inf(‖h‖₂ + ‖μ‖₁) 有什么下游价值？
（答：它把抽象位势范数翻译成”一个欧氏向量加若干条根路径的最小可加成本”，高度一时恰为 Dilworth 等人的 ℓ₂ 反例（命题 prop:linear-duality）。这既校准了模型，又给外层 Hilbert 和结构提供可直接引用的块，姊妹篇中 L¹ 随机实现正建立在这套块结构上。）
问 6：自反模型的范数等价于 Hilbert 范数，分离现象岂不是平淡无奇？
（答：不平淡。等价于 Hilbert 范数只保证自反性，但 Hilbert 型空间本可再赋范成一致凸；本文恰恰证明这两个空间在原范数下有正的渐近中点模，而任何等价范数下单侧模在某个 t₀ 处为零（引理 lem:bounded-tree 给出 t₀ = αc/(2βM)）。”本可很凸的空间里仍换不出 AUC”正是反例的锋利之处。）
总评
这项工作把 AMUC/AUC 再赋范分离问题在自反世界干净落地，构造显式、主线已形式化，分量扎实；最大风险在大量未逐一核验的数值常数与多约束变体的组合细节，可信度系于形式化覆盖的完整性。