核亏空主导两倍的凸包亏空：中野不等式的严格强化
The Kernel Deficit Dominates Twice the Hull Deficit: A Sharp Strengthening of Nakano's Inequality
浏览论文内容
中文总结 AI 辅助
该研究强化了中野不等式，证明多边形核亏空主导两倍凸包亏空，通过凸体帽并集等方法推导，结果有Lean 4机器验证。
中文摘要 AI 辅助
若多边形内一点能看到整个多边形，则该点位于多边形的核中。因此，核衡量单个守卫可覆盖多边形的程度，而凸包则衡量多边形偏离凸性的程度。我们证明这两种亏空存在严格的两倍因子关联：多边形与其核之间损失的面积，主导了多边形凸包中缺失的核加权面积的两倍。以Sibley的守卫点比率G和外比率E（记为A）表示，结果为G ≤ A/(2-A)，当A < 1时，该结果改进了中野不等式G ≤ A。证明通过凸体帽并集展开：从紧致凸体K及其凸包包含它的有限个点，将每个点与K连接，取所得帽的并集U。对多边形U的有向边界边进行循环排序，得到凸伴随体H。边界反转论证给出|H| + |U| ≥ 2|conv U|，而支撑函数恒等式与Minkowski混合面积不等式给出|U|² ≥ |K||H|。内部多边形逼近处理所有正面积的紧致凸K，单独的零面积分支覆盖点、线段及所有其他低维情况。两个主定理均有机器验证的Lean 4证明，其最终陈述经内核检查后与非正式陈述核对。
英文摘要
A point lies in the kernel of a polygon if it can see the entire polygon. Thus the kernel measures how much of the polygon is available to a single guard, while the convex hull measures how far the polygon is from being convex. We prove that these two losses are linked by a sharp factor of two: the area lost between a polygon and its kernel dominates twice the kernel-weighted area missing from the polygon's convex hull. In terms of Sibley's guard-point ratio $G$ and exterior ratio $E$, which we denote by $A$, the result is $G \leq A/(2-A)$, which improves Nakano's inequality $G \leq A$ whenever $A < 1$. The proof passes through a convex-body cap union. From a compact convex body $K$ and finitely many points whose convex hull contains it, we join every point to $K$ and take the union $U$ of the resulting caps. Cyclically sorting the directed boundary edges of a polygonal $U$ produces a convex companion $H$. A boundary-reversal argument gives $|H| + |U| \geq 2|\mathrm{conv}\, U|$, while a support-function identity and Minkowski's mixed-area inequality give $|U|^2 \geq |K||H|$. Inner polygonal approximation handles every positive-area compact convex $K$, while a separate null-area branch covers points, segments, and all other lower-dimensional cases. Both main theorems have machine-checked Lean 4 proofs whose final statements were audited against the informal statements after kernel checking.
