Two-colour Zig-Zag Numberlink on rectangles
Source: github.com/zzyzek/R2K2ZZN/tree/6567375a4c4574d26237756819e2…
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-11-04-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-04-000002/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-04-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'