The Kernel Deficit Dominates Twice the Hull Deficit

For a simple polygon F in the plane, the kernel K(F) is the set of points that see all of F, and the convex hull C(F) measures how far F is from being convex. We prove that the two associated losses are linked by a sharp factor of two: area(F)(area(F) − area(K)) ≥ 2·area(K)(area(C) − area(F)) In terms of Sibley's guard-point ratio G and exterior area ratio A, this reads G ≤ A/(2−A), which strictly improves Nakano's inequality G ≤ A for every non-convex polygon. The coefficient two cannot be increased: a one-parameter family of non-convex equality examples is exhibited. The proof passes through a convex-body cap union. Cyclically sorting the directed boundary edges of a polygonal cap union U produces a convex companion H; a boundary-reversal argument gives area(H) + area(U) ≥ 2·area(conv U), while a support-function identity and Minkowski's mixed-area inequality give area(U)² ≥ area(K)·area(H). Inner polygonal approximation extends the result to every positive-area compact convex body, and a separate branch covers the degenerate cases. Both main theorems have machine-checked Lean 4 proofs whose final statements were audited against the informal statements after kernel checking. The accompanying formalization is at https://github.com/SilverAsh7/p5-kernel-deficit-lean (commit 64e81a503ee4d78875cb9cededdda18995f30007). A final section separates rigorous bounds, exact finite computations, and conjectures for Nakano's still-open perimeter optimum α*, and makes no claim to determine it. The manuscript includes a declaration of generative AI assistance.