K3,3 and K5 nonplanarity in Lean from JCT + winding additivity, no faces needed

Chord lemma: theta-graph with arcs α, β, γ from x to y, and an arc δ from an interior point of α to an interior point of γ that otherwise misses the theta. Then δ° and β° lie on different sides of the Jordan curve α∪γ. Proof: let W be the side missing β. w_{αβ} and w_{βγ} are constant (c1, c2) on W. Each interior point of γ is in closure W and off α∪β, so w_{αβ} = c1 there. Follow δ from its γ-end (and likewise its α-end) to get w_{αγ} = c1 + c2 at δ's midpoint, which is the value on W. Contradiction, since w_{αγ} is ±1 on one side and 0 on the other. For K3,3, take the hexagon plus three chords; for K5, the pentagon plus five chords (the interleaving graph is a 5-cycle). The chord lemma for one pair plus rotations of the vertex labels (comap along Equiv.addRight) covers all pairs, and pigeonhole over the two sides finishes. Each file is ~250 lines and elaborates in ~3 s.