Planar Euclidean midpoint rigidity

This proves the dimension-two case of Nielsen–Okamura Conjecture 9.1 (arXiv:2609.07551v2, Section 9). The midpoint hypothesis uses actual canonical short geodesics of the two Euclidean dual connections. The proof includes the construction of those local germs and their fourth-order obstruction.

theorem PlanarMidpoint.planar_midpoint_rigidity_C2 (Ω : Set E) (C : E → Coeff) (openΩ : IsOpen Ω) (connectedΩ : IsPreconnected Ω) (smoothC : ContDiffOn ℝ 2 C Ω) (complementary : LocalMidpointInvariance Ω C) : ∃ (c : Coeff), ∀ p ∈ Ω, C p = c

Twice continuously differentiable coefficients already suffice for planar dual-geodesic midpoint rigidity.

theorem PlanarMidpoint.planar_dual_midpoint_rigidity (Ω : Set E) (C : E → Coeff) (openΩ : IsOpen Ω) (connectedΩ : IsPreconnected Ω) (smoothC : ContDiffOn ℝ (↑⊤) C Ω) (complementary : LocalMidpointInvariance Ω C) : ∃ (c : Coeff), ∀ p ∈ Ω, C p = c

Nielsen–Okamura Conjecture 9.1 in dimension two, with its full geometric midpoint hypothesis and no assumed fourth-order condition.