Complementary geodesic midpoints force the fourth-order obstruction

The proof compares actual short geodesics with explicit polynomial trajectories. It needs no differentiability of a family of solutions with respect to endpoints.

theorem PlanarMidpoint.obstruction_of_short_complementary_pairs {Ω : Set E} {C : E → Coeff} {p : E} (hΩ : IsOpen Ω) (hp : p ∈ Ω) (hC : ContDiffOn ℝ 2 C Ω) (hpairs : ArbitrarilyShortComplementaryPairs C p) (h : E) : obstruction (C p) (fderiv ℝ C p) h = 0

Complementarity for arbitrarily short actual geodesics annihilates the first-order quartic obstruction.