A converse to the discrete four-vertex theorem
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'