{"id":"palomar/PALOMAR-2026-08-19-000003","url":"https://github.com/WillWhistler/Regts-Sevenster/tree/bb0a60543d48afac3f36938104b5c85c7c0396c7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-19-000003-v2.json","repo":"https://github.com/WillWhistler/Regts-Sevenster","tags":["math.CO","math.CT","msc:05C31","msc:05C50","msc:18M05","msc:18M25","msc:20C30","msc:68V20","graph-invariants","category-theory"],"score":0,"title":"A proof of the Regts–Sevenster conjecture, formalized","trust":"high","domain":"math.CO","source":"palomar","authors":["William Whistler"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 proof of the Regts–Sevenster conjecture. A complex-valued graph parameter, normalized at the empty graph and invariant under isomorphism, has exponentially bounded edge-connection rank if and only if it is a mixed partition function. For a natural rank base R, a representing model can be chosen with k even and 2ℓ odd colours satisfying k + 2ℓ ≤ R. The development also proves the even connection-rank growth limit, minimum total colour dimension, minimal parity formulas and prescribed-dimension criterion. Schrijver's factorial argument supplies nilpotent-trace vanishing;…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-06","reactions":{},"formalized":true,"formalizes":[{"title":"Mixed partition functions are exactly the graph parameters of exponentially bounded edge-connection rank","identifier":"arXiv:2607.27198","relationship":"formalizes"},{"title":"Tannakian categories in positive characteristic","identifier":"arXiv:1812.02452 (Duke Math. J. 169 (2020), 3167-3219)","relationship":"adapts"},{"title":"Characterizing partition functions of the edge-coloring model by rank growth","identifier":"arXiv:1211.3561","relationship":"adapts"}]}