发表机构
University of New Hampshire（新罕布什尔大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究凸截面在平移和缩放下的渐近行为，定义尾部不变量，证明其连续统性质，并构造具有近泛点的凸体，所有结果经Lean 4验证。
AI 中文摘要
我们研究凸性中的一类问题，其中“大小无关紧要”：一个凸截面仅记录到平移和缩放，因此与凸体$B$和方向$\rho$相关的数据是紧度量空间$\A_{n-1}$（即“对齐形状”的空间）中的一条路径。我们关注的对象是当切割超平面接近最后一个支撑超平面时该路径的渐近行为，由我们称为“尾部”的不变量$T(B,\rho)$编码。我们证明尾部总是连续统，多面体和光滑支撑点是“平凡的”（尾部是一个点），而非平凡行为迫使接触退化。我们证明截面路径是局部可求长的，每条局部可求长路径可近似实现，且一个稠密类可精确实现，但精确实现在一般情况下失败：一个有界转向类型的二阶障碍产生一条不是截面路径的可求长路径。相比之下，对于尾部，没有这样的限制存在：每个形状连续统都作为尾部出现，而且是精确出现而非近似出现。我们构造具有“近泛”点的凸体，在这些点上重整化截面任意好地逼近每个平面（更一般地，$(n-1)$维）凸形状；这样的点可以在边界中稠密，且在嫁接点处具有任意指定的尾部。以下每个结果都已在Lean~4中正式验证。最后我们提出几个优化问题和一个高余维变体。
英文摘要
We study a family of questions in convexity in which \emph{size does not matter}: one records a convex cross-section only up to translation and scaling, so that the data attached to a convex body $B$ and a direction $ρ$ is a path in the compact metric space $\A_{n-1}$ of \emph{aligned shapes}. The object of interest is the asymptotic behaviour of this path as the cutting hyperplane approaches the last supporting hyperplane, encoded by an invariant $T(B,ρ)$ that we call the \emph{tail}. We show that tails are always continua, that polyhedral and smooth support points are ``boring'' (the tail is a point), and that non-boring behaviour forces degenerate contact. We show that cross-section paths are locally rectifiable, that every locally rectifiable path is realisable approximately and a dense class exactly, and that exact realisation fails in general: a second-order obstruction of bounded-turning type produces a rectifiable path that is not a cross-section path. For tails, by contrast, no such restriction survives: every continuum of shapes occurs as a tail, on the nose rather than up to approximation. We construct bodies possessing \emph{nearly universal} points, at which the renormalised cross-sections approximate every planar (more generally $(n-1)$-dimensional) convex shape arbitrarily well; such points can be made dense in the boundary, with arbitrary prescribed tails at the grafting sites. Every result below has been formally verified in Lean~4. We close with several optimisation questions and a higher-codimension variant.
Comments17 pages, LEAN 4 verified
