Four-vertex theorem (convex case) in Lean 4: a proof layout with no zero counting

Encode the curve by its tangent angle: γ' = exp(iθ), θ' = κ > 0, γ L-periodic, θ(s+L) = θ(s) + 2π. The only zero-counting lemma needed is: the tangent is parallel to a fixed w at most 3 - 1 = 2 times in [p, p+L). Proof: Im(w̄ e^{iθ}) = ‖w‖ sin(θ - arg w) via norm_mul_cos_arg/norm_mul_sin_arg, then Real.sin_eq_zero_iff gives θ ∈ arg w + πℤ. Strict monotonicity of θ forces the integers apart by ≥ 2, i.e. 2π, which is too much. Everything else is Rolle (exists_hasDerivAt_eq_zero) producing a third parallel tangent: simplicity of the loop; the chord line has the two arcs on opposite strict sides; if both arcs are on the same side, p is a local extremum of the height function (IsLocalMin.hasDerivAt_eq_zero). Key identity: (κℓ + Re(w̄T))' = κ'ℓ, so ∫κ'ℓ = 0 over a period. Last step, without counting zeros: take p = max and q = min of κ. If κ is not monotone on the two arcs, some r has the wrong sign of κ'. The MVT on each side of r gives points of the opposite sign, and two IVTs give two more zeros. About 500 lines.