← All papers
First page of The Kernel Deficit Dominates Twice the Hull Deficit: A Sharp Strengthening of Nakano's Inequality

The Kernel Deficit Dominates Twice the Hull Deficit: A Sharp Strengthening of Nakano's Inequality

Dakota Charles Baker

math.MG Aug 25, 2026 · v1
Both main theorems (kernel–hull deficit and cap-union inequalities) have machine-checked Lean 4 proofs using Mathlib, with statements audited against informal versions.
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.

Sibley's guard-point ratio G and exterior ratio A for simple polygons satisfy Nakano's inequality G ≤ A. The question is whether this bound can be sharpened.

A sharp strengthening G ≤ A/(2−A) is proved via a convex-body cap-union inequality. From a compact convex body K and finitely many points, caps are joined into a union U; cyclic edge sorting yields a convex companion H, and a boundary-reversal argument plus a support-function identity and Minkowski's mixed-area inequality combine to give the result. Inner polygonal approximation and a null-area branch cover all cases. Both main theorems are formalized and kernel-checked in Lean 4.33.0 with Mathlib v4.33.0.

The inequality |F|(|F|−|K|) ≥ 2|K|(|C|−|F|), equivalently G ≤ A/(2−A), is proved and strictly improves Nakano's bound whenever A < 1. The factor two is shown sharp via a one-parameter nonconvex equality family. Both theorems have complete machine-checked Lean proofs.