Optimal clique partitions under local perturbations
A Lean 4 / Mathlib formalization of the main results of the author's preprint "Optimal Clique Partitions under Local Perturbations" (Erdős #81 series, Paper VI). For a graph G on n vertices with a core P of size p = ⌊(n+1)/3⌋, h = Δ(G △ (K_P ∨ I_O)) and u, s, m the numbers of core, crossing and exterior edges: if p ≥ 18h + 1 then cp(G) = cp_{≤4}(G) = s − u − 2m = M(n) + C − A − 2m with M(n) = ⌊n(n+1)/6⌋ (Theorem A), and cp_{≤3}(G) − cp(G) = m (Theorem B); if p ≥ 63h, every assignment of the orders 4 or 5 to the exterior edges is realized by an optimal partition (Theorem C); for p ≥ 16 each…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-01-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-01-000006/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-11-01-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'