Continuous simplicity certificates for finite polygonal routes

Main definitions

• Cslib.Orthogonal.EndpointContacts: every continuous segment intersection is a common endpoint.
• Cslib.Orthogonal.IsSimple: no repeated listed points, and distinct consecutive segments have only common endpoint contacts. In conjunction with proper segments, this excludes retracing, self-crossings, and contacts between nonadjacent segments.

References

The finite-route simplicity certificate and elementary proofs are original.

def Cslib.Orthogonal.EndpointContacts (a b c d : Point) : Prop

Two continuous closed segments contact only at common endpoints.

theorem Cslib.Orthogonal.EndpointContacts.symm {a b c d : Point} (h : EndpointContacts a b c d) : EndpointContacts c d a b

Interchanging the two segments preserves the contact certificate.

theorem Cslib.Orthogonal.EndpointContacts.reverse_left {a b c d : Point} (h : EndpointContacts a b c d) : EndpointContacts b a c d

Reversing one segment preserves the contact certificate.

theorem Cslib.Orthogonal.EndpointContacts.reverse_right {a b c d : Point} (h : EndpointContacts a b c d) : EndpointContacts a b d c

Reversing one segment preserves the contact certificate.

theorem Cslib.Orthogonal.endpointContacts_of_disjoint {a b c d : Point} (h : Disjoint (segment a b) (segment c d)) : EndpointContacts a b c d

Disjoint segments have no non-endpoint contacts.

def Cslib.Orthogonal.IsSimple (r : Route) : Prop

A finite polygonal route with no repeated listed points and only common-endpoint contacts between distinct segments. All contacts are tested in the real plane.

theorem Cslib.Orthogonal.IsSimple.of_cons {a : Point} {r : Route} (h : IsSimple (a :: r)) : IsSimple r

Removing the initial listed point preserves continuous simplicity.