{"id":"palomar/PALOMAR-2026-11-04-000002","url":"https://github.com/zzyzek/R2K2ZZN/tree/6567375a4c4574d26237756819e2ce4b027bf119/proof","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000002-v1.json","repo":"https://github.com/zzyzek/R2K2ZZN","tags":["cs.DM","math.CO","msc:05C38","msc:05C85","msc:68R10"],"score":0,"title":"Two-colour Zig-Zag Numberlink on rectangles","trust":"high","domain":"cs.DM","source":"palomar","authors":["Z. Zzyzek (github: zzyzek)"],"reviews":0,"subject":"cs.DM","summary":"A Lean 4 proof that two-colour Zig-Zag Numberlink on rectangular grids (the paired 2-disjoint path cover problem: two vertex-disjoint paths s0 → t0 and s1 → t1 that together visit every cell) is decided by an explicit procedure, and that an explicit construction finds a solution whenever one exists. For both sides at least 11, an instance is solvable exactly when it passes a finite catalogue of forbidden patterns; for a side at most 10, a plug dynamic program decides it. The finite cases of the characterization are 21 boxes of slice certificates and 59 window certificates, all checked by the…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true,"formalizes":[{"title":"Two-colour Zig-Zag Numberlink on rectangles","identifier":"","relationship":"formalizes"}]}