AI 中文总结
研究紧致凸体在仿射和射影语言下的初等等价性，通过可定义紧致度量族等方法证明任意维度凸体在\(L_{\mathrm{aff}}\)中初等等价当且仅当仿射等价，还发展了\(L_B\)演算及得出相关结果并分类非紧致例子。
AI 中文摘要
一个紧致凸体\(K\subseteq\mathbb{R}^n\)是两种自然语言下的一阶结构：\(L_{\mathrm{aff}}\)，具有三元中间关系和凸组合运算；以及更稀疏的\(L_B\)，仅具有中间关系。同构在第一种语言中意味着仿射等价，在第二种语言中根据希夫曼定理意味着射影等价。我们研究何时初等等价已经能确定该凸体。主要定理：任意维度的两个紧致凸体，无正则性假设，在\(L_{\mathrm{aff}}\)中初等等价当且仅当它们仿射等价。证明基于一个可定义的紧致度量族：对于重心坐标固定的单纯形，通过反互补单纯形使体积有下界。对于\(L_B\)，我们发展了一种内部冯·施陶特演算，所有量词在凸体内取值，使调和共轭、有理交比比较和交比相等成为一阶的；仅需调和原语，通过单个内部透视实现尺度变化。结果：对于每个\(n\geq2\)，闭单位球在\(L_B\)中与\(\{\sum x_i^4\leq1\}\)分离；在平面上，对于凸多边形和具有实解析、正曲率、非圆锥边界的凸体，射影范畴性直接成立，后者通过一个新的有限射影不变量，即圆锥簇集：其每个边界弧包含六个共圆锥极点的点。一般约化分离出射影猜想的剩余部分：在至少三维中恢复边界坐标以及一个可定义的紧致度量，恰好被非紧致射影对称阻碍，如在二次曲面上。我们还对自然的非紧致例子进行了分类。
英文摘要
Convex subsets of R^n carry two first-order structures: barycentric (affine) structure, with operations C_l(p,q)=(1-l)p+lq for l in [0,1], and betweenness (projective) structure, with ternary relation B(a,x,b) meaning x lies in [a,b]. Isomorphism means affine equivalence in the first and, for n at least 2 and sets open or closed, projective equivalence in the second. We ask when elementary equivalence already determines the body. Main theorem: two compact convex bodies of any dimension, with no regularity hypotheses, are elementarily equivalent in the barycentric language if and only if they are affinely equivalent. The proof rests on a definable compact family of gauges: simplices stationary for barycentric coordinates, with volume bounded below via the anticomplementary simplex. For the betweenness language we develop an interior von Staudt calculus, all quantifiers ranging over the body, making harmonic conjugacy and rational cross-ratio comparisons first-order; a relativization scheme then propagates planar separations to R^n. Consequences: the closed unit ball is separated from sum x_i^4 <= 1 for every n at least 2; and in the plane, projective categoricity holds outright for convex polygons and for bodies with real-analytic, positively curved, non-conic boundary, the latter via a definable finite projective invariant, the conic-cluster set: the points whose every boundary arc contains six co-conic extreme points. A general reduction isolates what remains of the projective conjecture: recovery of boundary coordinates in dimension at least three, and a definable compact gauge, obstructed exactly by non-compact projective symmetry, as on the quadric. For closed noncompact bodies the asymptotic structure is itself elementary: the dimensions of the recession cone and of the lineality space are determined by the betweenness theory, separating the solid cylinder from the slab.
Comments42 pages. All numbered results are formalized in Lean 4 against Mathlib, with no sorry and only the standard axioms. The development is included as ancillary material and archived at https://doi.org/10.5281/zenodo.21997275; classical inputs not formalized appear there as explicit hypotheses, never as axioms
