{"id":"palomar/PALOMAR-2026-10-17-000001","url":"https://github.com/kejace/cd4vt/tree/bfd433640794b11424be43ad4778566be9253ef4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000001-v1.json","repo":"https://github.com/kejace/cd4vt","tags":["math.MG","math.DG","msc:53A70","discrete-geometry","polygons","four-vertex-theorem","lean-formalization"],"score":0,"title":"A converse to the discrete four-vertex theorem","trust":"high","domain":"math.MG","source":"palomar","authors":["Kristoffer Josefsson"],"reviews":0,"subject":"math.MG","summary":"Lean 4 / Mathlib formalization of the paper \"A converse to the discrete four-vertex theorem\", answering Tabachnikov's Problem 2. For every n >= 4, every cyclic sequence of positive numbers with two distinct plateau maxima and two distinct plateau minima is the sequence of circumradii of consecutive vertex triples of a simple, strictly convex, coherent polygon (circumcenters inside the vertex angles). Together with Dahlberg's discrete four-vertex theorem, also proved here, this characterizes the nonconstant radius sequences of such polygons. The realization can be chosen C^1 in the data near…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true}