结果族 331：Reflexive midpoint convexity and diamond distortion · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
球的”圆度”可以打分：球面上两个离得远的点，它们的中点应该明显陷进球里。无穷维空间里可以耍赖——往某些方向看是平的，但你每次只能检查有限多个方向。这篇论文造出一个非常正派的空间（自反、可分）：扔掉任意有限多个方向后，它始终保有”中点版”的圆度；可是无论怎么更换等价范数，都换不出更强的”单向版”圆度。两种圆度被彻底分开，顺带否定了自反情形的菱形反问题。
关键词卡片
看个具体例子
两条定量结论，代入数字即可感受：平均中点模 @@M@@\widehat\delta_X(t)\ge\sqrt{1+t^2/12}-1@@（如 @@M@@t=1@@ 时约 @@M@@0.041@@）；深度 @@M@@k@@ 的可数分支菱形图嵌入 @@M@@X@@ 的失真下界 @@M@@\sqrt{1+k/12}@@——@@M@@k=12@@ 时 @@M@@\ge\sqrt2\approx1.41@@，@@M@@k=36@@ 时 @@M@@\ge2@@。菱形越深，在这个空间里越”塞不平”，没有一致有界的嵌入。
为什么值得关心
它回答了 Baudier–Lancien 书稿中的问题 39：即使加上自反性，中点凸性也不足以阻止菱形图被越嵌越歪。
主结果已 Lean 形式化
第一级台阶
导读用”球的圆度打分”区分两种圆：中点版（远两点的中点陷进球里）与单向版（单个方向就能看到凹陷）。无穷维的耍赖方式是”平的方向藏在你看不见的地方”，于是测试规则改为：先扔掉任意有限多个方向，再看剩下的几何。本文造出一个空间：这种”扔完再测”的中点圆度永远保有，可无论换哪套等价刻度，单向版圆度都造不出来。
第二级台阶
用本科术语说：Banach 空间 X 的（平均）中点模 δ̂_X(t) 度量单位球面上相距 t 的两点之中点到球心的最短距离，一致凸即该模处处为正；渐近版本要求只在某个有限余维子空间里检验，AMUC 指这个渐近中点模一致为正。渐近一致凸（AUC）则用单点 x 与远点 y 的中点衡量，是更强的单向条件。等价范数指与原范数互相控制的另一把尺子；图嵌入的失真是边长拉伸倍数在最优嵌入下的最小值。
第三级台阶
主定理的语境：X=J*，其中 J 是可数分支、高度有限但无界的树森林上有限支撑函数在”两两不交线段平方和”范数 ρ(u)=sup(Σu(S_i)²)^{1/2} 下的完备化。分量为 Hilbert 型结构保证 X 可分自反——自反性正是此前反例（Baudier 的不自反空间）缺失的资质。结论三合一：X 的天然范数是 AMUC，模有显式下界 √(1+t²/12)−1；X 不容许任何等价的 AUC 范数；深度 k 的可数分支菱形图嵌入 X 的失真至少 √(1+k/12)，故中点凸性即使配自反性也拦不住菱形被越嵌越歪。
构造出可分自反 Banach 空间 @@M@@X=J^*@@：其天然范数渐近中点一致凸（模 @@M@@\ge\sqrt{1+t^2/12}-1@@），却无任何等价的渐近一致凸范数；深度 @@M@@k@@ 的可数分支菱形图嵌入 @@M@@X@@ 失真必 @@M@@\ge\sqrt{1+k/12}@@，否定自反情形的菱形反问题。
渐近凸性 (asymptotic convexity) 度量”扔掉有限多个方向后还剩多少凸性”。Dilworth–Kutzarova–Randrianarivony–Revalski–Zhivkov（2016）引入渐近中点一致凸性 (asymptotic midpoint uniform convexity, AMUC)，在 @@M@@\ell_2@@ 上造出 AMUC 而非 AUC 的范数，并问：AMUC 能否通过重赋范 (renorming) 得到渐近一致凸 (asymptotically uniformly convex, AUC) 的等价范数？Baudier（2026）用 Kadets–Werner 修正的 Bourgain–Rosenthal 空间给出否定回答，但该空间不自反。另一条线索是度量嵌入：Baudier 等（2017）证明 AMUC 范数排除可数分支菱形图 (countably branching diamonds) 的一致嵌入，并在”自反＋无条件渐近结构”假设下证明非 AUC 可重赋范反而蕴涵菱形一致嵌入。无条件结构这一假设能否去掉（Baudier–Lancien 书稿中记录的问题 39），正是本文要回答的：不能。
取可数分支、高度有限但无界的树之森林 @@M@@\mathcal F=\coprod_{h\ge1}(\{h\}\times\mathbb N^{\le h})@@，对有限支撑实函数用 James 的不相交线段平方和范数 @@M@@\rho(u)=\sup(\sum_i u(S_i)^2)^{1/2}@@（上确界取遍两两不交线段 (segment) 的有限族），完备化得 @@M@@J@@，令 @@M@@X=J^*@@。主定理：@@M@@X@@ 无穷维、可分、自反 (reflexive)，且不容许任何等价 AUC 范数；其原始范数满足平均中点模 @@M@@\widehat\delta_X(t)\ge\sqrt{1+t^2/12}-1@@，故为 AMUC；并且对每个整数 @@M@@k\ge0@@，深度 @@M@@k@@ 的可数分支菱形 @@M@@D_k@@ 到 @@M@@X@@ 的任何嵌入的失真 (distortion) 至少为 @@M@@\sqrt{1+k/12}@@。换言之：即便加上自反性，中点一致凸也不强迫菱形图有一致有界嵌入。
论证分四步。先建坐标结构：高 @@M@@h@@ 的分量上是 Hilbert 型的（@@M@@\|u\|_2\le\rho(u)\le\sqrt{h+1}\|u\|_2@@），故 @@M@@J@@ 是各分量的 @@M@@\ell_2@@ 直和，其对偶仍是 @@M@@\ell_2@@ 直和，两次运用即得 @@M@@X@@ 自反；对有限祖先集 (ancestral set) @@M@@H@@ 的坐标投影 @@M@@P_H@@ 是压缩的，而 @@M@@H@@ 之外的余部分按”门”（gate，即 @@M@@H@@ 外的极小顶点）分解为 @@M@@\ell_2@@ 直和。再证无 AUC 重赋范：沿根路径求和的泛函 @@M@@p_v@@ 范数恰为 1，其子增量 @@M@@e^*_{v^\frown j}@@ 是弱零 (weakly null) 的单位向量（因 @@M@@X^*=J@@ 而 @@M@@J@@ 中坐标平方可和）。假设某等价范数 @@M@@N@@ 的单侧渐近模在某半径为正，则借助有限维商空间逼近，可把有限余维子空间中的增益转移到某个真实子方向上，使范数沿路径每步至少乘以 @@M@@1+\gamma/2@@；取足够高的树逐层迭代便突破范数的上界，矛盾——故每个等价范数的模在 @@M@@\alpha/(2\beta)@@ 处为零。第三步是核心的成对扩张引理：设 @@M@@x=P_Hx@@、@@M@@y=Q_Hy@@，先取头部与尾部各自近乎赋范的线段测试 @@M@@f,k@@，朴素的 @@M@@f\pm sk@@ 会在跨越 @@M@@H@@ 边界的线段上产生失控的正交叉项；作者改为在首出口顶点（门）处添加同一个修正向量 @@M@@c@@，其符号与过大的头部后缀和相反，使得修正后两个测试都满足 @@M@@\rho^2\le1+12s^2@@，而两个端点的赋值取平均时 @@M@@c@@ 的贡献恰好相消，由此得 @@M@@(\|x+y\|+\|x-y\|)/2\ge\sqrt{\|x\|^2+\|y\|^2/12}@@，对参数 @@M@@s@@ 调优即得模下界。最后处理菱形：先由有限维紧性把无穷多个两两分离的近似中点配出一对投影任意接近者，其半差经交叉凸组合仍留在同一透镜 (lens) 中且尾部不小，代入成对引理得 @@M@@R^2-\|x\|^2\ge\varepsilon^2/48@@；对每层定义斜率上确界 @@M@@L_m@@，每次边替换至少损失 @@M@@1/12@@，即 @@M@@L_m^2\le L_{m+1}^2-1/12@@，逐层求和得 @@M@@D^2\ge L_0^2+k/12\ge1+k/12@@。
主结果已 Lean 形式化（家族文档 lean/docs/331.md）。本族三篇互相支撑：本文自成体系地给出 @@M@@X@@ 上常数 @@M@@1/12@@；姊妹篇《Midpoint lenses in segment spaces》证明更一般的透镜尾估计并把结论推广到无穷高模型；《Distortion of countably branching diamonds…》用该尾估计把 @@M@@X@@ 上的下界改进为 @@M@@\sqrt{1+k/4}@@。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇主结果已形式化，数值常数以论文陈述为准。
问 1：证明中最关键、最脆弱的一步是什么？
（答：第 4 节（paired）的成对扩张引理是全文支点：对 x=P_Hx、y=Q_Hy，要证 (‖x+y‖+‖x−y‖)/2≥√(‖x‖²+‖y‖²/12)。朴素测试 f±sk 在跨越 H 边界的线段上产生失控交叉项；改为在首出口顶点（门）处加同一个修正向量 c，符号与过大的头部后缀和相反，使两测试 ρ²≤1+12s²，端点取平均时 c 相消。常数 12 与符号配合是下界 1/12 的出生地、审稿首查处。）
问 2：自反性这个升级为何要紧？此前不是已有否定回答吗？
（答：Baudier 2026 已用 Kadets–Werner 修正的 Bourgain–Rosenthal 空间回答过 DKRRZ 的重赋范问题，但该空间不自反；而 Baudier 等 2017 的菱形定理在”自反＋无条件渐近结构”下有正面结论，Baudier–Lancien 书稿问题 39 正是问自反性够不够。J* 可分自反且无条件结构不成立，落实了”无条件”假设的必要性——新否定而非旧结果搬运。）
问 3：没有 AUC 等价范数的障碍论证怎么运作？
（答：第 3 节（obstruction）用路径泛函：沿根路径求和的 p_v 范数恰为 1，子增量 e*_{v⌢j} 是弱零单位向量。若等价范数 N 的单侧渐近模在 α/(2β) 处为正，经有限维商逼近把增益转移到真实子方向，范数沿路径每步至少乘 1+γ/2，树够高即突破等价上界——矛盾。故一切等价范数的模在该半径为零。）
问 4：AMUC 却非 AUC 可重赋范，两种凸性的差距在哪现形？
（答：现形于单向与双向之差：中点模要求 x±y 同时提供信息（成对引理把 ‖x+y‖ 与 ‖x−y‖ 加在一起用），AUC 只要一个方向。J* 的几何对成对的对称测试慷慨（Hilbert 型分量提供 ℓ₂ 结构）、对单向渐近测试吝啬（路径泛函提供逐层摊平的方向），这个不对称正是反例的灵魂。）
问 5：这类 AI 生成的构造性证明最可能的出错模式？
（答：最危险的是修正向量 c 的一石二鸟：它要同时救活两个测试的范数估计，又在端点平均时相消——符号判断依赖”头部后缀和过大”的择一情形，情形划分漏了状态即破。其次是菱形节的配对紧性：无穷多近似中点配出投影任意近的一对，半差交叉凸组合留在同一透镜且尾部不小，易与可分性细节打架。主结果已 Lean 形式化，可据此核对 1/12 这类常数。）
问 6：菱形失真的逐层斜率论证为何恰好给出 1/12？
（答：第 6 节（diamonds）对每层定义斜率上确界 L_m，每次边替换经成对引理得 R²−‖x‖²≥ε²/48 型估计、折算为 L_m²≤L_{m+1}²−1/12，逐层求和 D²≥L_0²+k/12≥1+k/12。1/12 正是成对引理里 12 的倒数——下界精度完全由该引理的常数决定，姊妹篇后用更强尾估计改进到 1/4。）
问 7：谁会关心这个反例？
（答：非线性几何与粗嵌入理论：菱形是粗嵌入/一致嵌入的经典障碍图，本例给出”自反＋AMUC 仍拦不住菱形失真增长”的精确边界，用中点凸性排除坏嵌入须补 AUC 重赋范才行；重赋范理论里它也是 AMUC 与 AUC 在自反类中分离的第一个样例，直接回应 Baudier–Lancien 问题 39。）
总评
在最好的空间类（自反）里钉死”中点圆”与”单向圆”的分离，顺带终结菱形反问题的自反版本，主结果有 Lean 背书；最大风险在成对引理的修正机制与常数链条，形式化已覆盖其主干。