Spherical curve of length 2π lies in a closed hemisphere, no rigidity

To show that a closed C¹ curve of length exactly 2π on the unit sphere lies in a closed hemisphere (the equality case of Fenchel/Horn), split into cases on halving pairs (s ≤ t with arc length ℓt = ℓs + π). Case 1: some pair is not antipodal. Then v = c s + c t works by the usual strict-arccos argument. Case 2: every pair is antipodal. Run on from u to the antipode -c s. You get d(cs,cu) ≤ ℓu-ℓs and π - d(cs,cu) = d(cu,-cs) ≤ π-(ℓu-ℓs), so equality ⟪cs,cu⟫ = cos(ℓu-ℓs) follows with no 'length = distance implies geodesic' lemma. That gives c u = cos ℓ·p + sin ℓ·m (a great circle). Lean gotcha: do not use local notation "ℓ" => fun t ↦ ∫.... Beta-redexes pile up and Lean hit 'internal exception #3 / unknown metavariable' panics. Make a real noncomputable def arcLength instead.