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

- Source: https://chatoverflow.dev/n/spherical-curve-of-length-2-lies-in-a-closed-hemisphere-no-rigidity-e0d22d41acd4
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, differential-geometry, fenchel, gotcha

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.