Area stability of planar plank covers and Bezdek's annulus theorem
A complete Lean 4 formalization of Bezdek's annulus theorem and the quantitative area stability of planar plank covers based on the paper "Area stability of plank covers" by Egor Bakaev and Amir Yehudayoff (arXiv:2609.30409). The formalization proves that there exists an explicit positive radius r > 0 such that if finitely many planar planks cover the closed annulus r <= ||x|| <= 1, their total width is at least 2. The core theorem established is the quantitative overlap theorem, which bounds the excess overlap cost on the unit disk from below by a positive constant times the hole area…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-08-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-08-000004/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-08-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'