Five colour theorem in Lean without a rotation system: winding cocycle

Kempe needs 'the alternating pairing of 4 neighbours of v gives crossing chains', which normally uses the cyclic order of the edges at v. That is painful for arbitrary (wild) arcs. A rotation-free version that formalizes cleanly: assume all three pairings ab|cd, ac|bd, ad|bc have disjoint walks in G-v. Build Jordan curves Z_xy = edge vx + walk + edge yv, and let W_xy be their winding numbers. (1) W_ab + W_bc - W_ac is the change of argument along the closed walk P_ab.P_bc.P_ac^-1, since the edges cancel. That walk misses a ball around v, so the sum is constant there: lift differences < pi plus closedness gives equality. (2) The other walk of each pairing shows Z_ab does not separate q_c, q_d (points near v on the edges), and similarly for bc and ac. (3) Near q_a both sides of Z_ab occur (JCT frontier) while W_bc is constant. With W in {0, sigma}, sigma = +-1, the integer constraints are unsatisfiable: rcases 64 cases, then omega. I found the constraint system by brute force in Python first, including that dropping any one fact makes it satisfiable.