Jordan curve winding number ±1 in Lean: chord surgery with explicit arctan lifts

To prove a Jordan curve has winding number ±1 inside (not just ≠ 0), avoid Schoenflies and theta-curve arguments. Cut along a horizontal chord through an inside point z₀; the endpoints are the first hits of J to the left and right. This gives two Jordan curves C_L, C_R that both contain the chord. Work with lifts on intervals (IsLiftOn F θ (Icc a b)): uniqueness up to 2πℤ via a 'continuous with values in b + cℤ is constant' lemma, and additivity over adjacent intervals by restricting one lift. Then w_J = w_L + w_R at z± = z₀ ± iε is pure bookkeeping. On the chord, use explicit lifts arctan(x/ε) - π/2 and π/2 - arctan(x/ε) (check them with Real.sin_arctan/cos_arctan and Complex.ext). Elsewhere, dir(γ - z+)/dir(γ - z-) has positive real part, so arg is a lift and changes by less than π (Complex.abs_arg_lt_pi_div_two_iff, continuousAt_arg (Or.inl hre)). So the jump is an integer in (0, 3/2). The JCT for C_L and C_R ('0 outside, constant inside') plus omega finishes. To build closed curves from a map g on [0,2π] with g 0 = g 2π and InjOn on Ico: use AddCircle.liftIco (needs a local Fact (0 < 2π) instance) composed with AddCircle.homeomorphCircle'.symm. Injectivity comes from unfolding liftIco = domRestrict g ∘ equivIco. Gotchas: Circle's topology is not syntactically a subtype, so IsInducing.subtypeVal.continuousOn_iff fails, while Continuous.subtype_mk works. ContinuousWithinAt division in Circle is .div'. In this Mathlib, if_pos, push_neg, setOf_and and ContinuousOn.restrict are deprecated.