Existence and restriction of canonical local midpoint maps

The small geodesic branch is constructed by the boundary-value contraction. Consequently canonical complementarity supplies complementary curves of arbitrarily small position and velocity size, without endpoint regularity as an additional hypothesis.

theorem PlanarMidpoint.exists_arbitrarily_short_geodesic {C : E → Coeff} {p : E} (hC : ContDiffAt ℝ 1 C p) (σ r : ℝ) (hr : 0 < r) : ∃ δ > 0, ∀ (P Q : E), P ∈ Metric.ball p δ → Q ∈ Metric.ball p δ → ∃ (γ : ℝ → E) (v : ℝ → E), IsShortGeodesic C σ p r P Q γ v

theorem PlanarMidpoint.localMidpointInvariance_arbitrarilyShort {Ω : Set E} {C : E → Coeff} {p : E} (hΩ : IsOpen Ω) (hp : p ∈ Ω) (hC : ContDiffOn ℝ 2 C Ω) (hlocal : LocalMidpointInvariance Ω C) : ArbitrarilyShortComplementaryPairs C p

theorem PlanarMidpoint.exists_canonical_local_midpoint {Ω : Set E} {C : E → Coeff} {p : E} (hΩ : IsOpen Ω) (hp : p ∈ Ω) (hC : ContDiffAt ℝ 1 C p) (σ : ℝ) : ∃ (r : ℝ) (W : Set (E × E)) (A : E → E → E), IsCanonicalLocalMidpoint Ω C σ p r W A

Smooth coefficient fields genuinely have canonical local midpoint maps; the defining predicate is witnessed by the constructed short BVP branch.

theorem PlanarMidpoint.canonical_midpoint_germs_agree {Ω₁ Ω₂ : Set E} {C : E → Coeff} {σ : ℝ} {p : E} {r₁ r₂ : ℝ} {W₁ W₂ : Set (E × E)} {A₁ A₂ : E → E → E} (hC : ContDiffAt ℝ 1 C p) (hA₁ : IsCanonicalLocalMidpoint Ω₁ C σ p r₁ W₁ A₁) (hA₂ : IsCanonicalLocalMidpoint Ω₂ C σ p r₂ W₂ A₂) : ∃ (W : Set (E × E)), IsOpen W ∧ (p, p) ∈ W ∧ W ⊆ W₁ ∩ W₂ ∧ ∀ (P Q : E), (P, Q) ∈ W → A₁ P Q = A₂ P Q

Any two canonical midpoint constructions for the same local connection agree after restriction to a common open neighborhood of the diagonal point. The comparison uses actual geodesics shorter than both defining radii.