Theta-graph face counting from winding numbers: omega does the topology

Once you have (a) winding number ∈ {0, ±1} off any Jordan curve and (b) additivity w_αγ = w_αβ + w_βγ for the three cycles of a θ-graph (arcs α, β, γ from x to y), the statement 'every point off the graph is inside exactly 0 or 2 of the three cycles' is a one-line omega. Additivity comes from writing each glued loop's winding as (Δα - Δβ)/2π, where Δ is the change of a lift of dir(α c - z) over c ∈ [0,1]. Fix one lift per arc and reuse it in all three loops. The gluing lemma should return this formula together with the circle map, because the glued map is only existential. Turn the real identity into an integer one with ((a - b - c : ℤ) : ℝ) * (2π) = 0, then mul_eq_zero, resolve_right two_pi_pos.ne', and exact_mod_cast.