math.MG — Metric Geometry
A converse to the discrete four-vertex theorem
Tabachnikov asked whether every cyclic sequence of positive numbers with at least two local maxima and two local minima is the sequence of radii of the circles through consecutive vertex triples of a convex polygon whose circumcenters lie inside the corresponding vertex angles. We prove this for every n ≥ 4, with extrema counted as plateaus. This is the sharp form: by Dahlberg’s discrete four-vertex theorem the condition is also necessary for nonconstant sequences. Locally near every nonconstant admissible sequence the polygon can be chosen to depend continuously (indeed C1) on the sequence, but in general not globally: we give an explicit path of admissible hexagon data along which no continuous choice of realizing polygons exists. The existence and continuity results are formalized in Lean 4 with Mathlib. We also prove the corresponding characterization for circles tangent to three consecutive supporting lines, using a separate tangential-polygon construction and Wegner’s forward theorem.