Exact transfers between opposite connection coefficients.

theorem PlanarMidpoint.neg_coeff_taylor_remainder (C : E → Coeff) (p d : E) (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) : ‖(-C) (p + d) - -c - (-J) d - (1 / 2) • ((-H) d) d‖ = ‖C (p + d) - c - J d - (1 / 2) • (H d) d‖

Negating the coefficient field and both derivatives preserves the Taylor-error norm.

theorem PlanarMidpoint.norm_neg_coeff_sub (C : E → Coeff) (p q : E) : ‖(-C) p - (-C) q‖ = ‖C p - C q‖

theorem PlanarMidpoint.isGeodesicSegment_neg (C : E → Coeff) (γ v : ℝ → E) : IsGeodesicSegment C (-1) γ v ↔ IsGeodesicSegment (-C) 1 γ v

Negating the field exchanges the plus and minus geodesic equations.

theorem PlanarMidpoint.isShortGeodesic_neg (C : E → Coeff) (p : E) (r : ℝ) (P Q : E) (γ v : ℝ → E) : IsShortGeodesic C (-1) p r P Q γ v ↔ IsShortGeodesic (-C) 1 p r P Q γ v

The shortness and endpoint requirements are unchanged by the sign transfer.