{"id":"palomar/PALOMAR-2026-10-17-000012","url":"https://github.com/benkeene/size-ramsey/tree/3233dcdd4807cbc808f68582d913c4f463047de2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000012-v1.json","repo":"https://github.com/benkeene/size-ramsey","tags":["math.CO","msc:05C55","msc:05D10","msc:05C35","ramsey-theory","size-ramsey","graph-theory","lean-formalization"],"score":0,"title":"The connected size-Ramsey number of a four-edge matching versus a quadrilateral","trust":"high","domain":"math.CO","source":"palomar","authors":["Ben Keene"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true}