OAI/Geometry/RCD/Harmonic/DefectSegment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An actual geodesic with controlled local defect

Positive endpoint sets are connected by the already constructed RCD bounded-compression plan. First-moment selection retains its endpoints, geodesicity, and whole-path containment. No segment or splitting input is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_defect_segment line 21