In Zig-Zag Numberlink, pairs of endpoints in a grid must be joined by vertex-disjoint paths that together visit every cell. The problem is NP-complete when the number of pairs is un- bounded (Adcock et al.). For a single pair it is the Hamiltonian path problem in rectangular grid graphs, solved by Itai, Papadimitriou and Szwarcfiter. Two pairs on a rectangle form the paired 2-disjoint path cover problem. We settle the case of two pairs on rectangles with the endpoints anywhere in the grid. If both sides of the rectangle are at least 11, an instance is solvable if and only if no entry of a finite catalogue of forbidden patterns occurs. The catalogue consists of a parity condition, an alternation condition on the border, a handful of local corner and edge patterns, 65 listed corner configurations, and a rule that propagates forced routes out of the corners before testing alternation. If a side is at most 10, a frontier dynamic programming algorithm decides the instance in time linear in the long side. The characterization is construc- tive. Solutions are built by deleting empty lines, splitting the rectangle by straight cuts, and splicing the pieces back together, in time O((R+C) RC). Both directions of the characterization and the correctness of the dynamic programming algorithm are verified in Lean 4. The finite case analyses, which are window certificates for the corner configurations and a check of all irreducible instances with sides 11-22, are carried out by the Lean compiler via native decide. We describe the algorithm, the catalogue, the proof structure, the compromises made in the formalization, and implementations in Python, JavaScript and C that produce identical output.