The connected size-Ramsey number of a four-edge matching versus a quadrilateral
A Lean 4 / Mathlib formalization project for the connected size-Ramsey equality rhat_c(4K2, C4) = 17. The intended proof uses a universal C4 vertex-transversal bound 4 tau_4(G) <= |E(G)|, a classification of the connected equality cases through sixteen edges (C4, the 4-wheel, K_{3,3} minus an edge, the octahedron), an avoiding-colouring construction from a three-vertex transversal, and an explicit twelve-vertex, seventeen-edge host. Proofs are complete as of commit c8d54e2 (2026-10-17); the proof certificate is Solution.lean and its dependency closure. Formal adversary pass 1 and reviewer…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000012
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000012/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-000012/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'