Qualitative convexity and universal cross-sections
David Victor Feldman
math.MG
Aug 6, 2026 · v1
TL;DR
All results on cross-section paths, tails and nearly universal points of convex bodies are stated to be formally verified in Lean 4 with Mathlib.
Abstract
We study a family of questions in convexity in which 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 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 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 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.
Problem
Convex cross-sections of a body recorded only up to translation and scaling form a path in a compact space of aligned shapes. The question is which asymptotic behaviours (tails) and which paths can occur as the cutting hyperplane approaches the last supporting hyperplane.
Approach
The space of aligned shapes is given a Hausdorff-type metric and shown to be compact. The tail invariant is defined, and Lipschitz estimates on section support functions give regularity of cross-section paths. Realisation questions are handled with a convexity criterion based on concave section supports and an iterated stacking and grafting construction. All results are reported as formally verified in Lean 4, citing Mathlib.
Results
Tails are continua, and polyhedral and smooth positive-curvature points have point tails. Cross-section paths are locally rectifiable, but local rectifiability is not sufficient for exact realisation, whereas every continuum of shapes occurs exactly as a tail. Bodies can be built with nearly universal points, dense in the boundary, at which renormalised sections approximate every convex shape.
