Gluing local and exterior incidence routes

Two simple orthogonal routes can be joined at a common endpoint when their full real supports intersect only there. The joined route is again simple and orthogonal; existing subdivision lemmas identify its support, final endpoint, segment list, and Manhattan wire length.

Main results

• head_mem_segment_endpoint, last_mem_segment_endpoint: an endpoint of a simple route can occur on a segment only as a segment endpoint.
• isOrthogonal_join, isSimple_join: geometric correctness of endpoint gluing.

References

These finite polygonal-route gluing lemmas and proofs are original.

theorem Cslib.Orthogonal.head_mem_segment_endpoint {r : Route} (hs : IsSimple r) {p : Point} (hp : List.head? r = some p) {e : Point × Point} (he : e ∈ List.consecutivePairs r) (hm : realPoint p ∈ segment e.1 e.2) : p = e.1 ∨ p = e.2

A simple route's initial listed vertex can lie on one of its segments only as an endpoint.

theorem Cslib.Orthogonal.last_mem_segment_endpoint {r : Route} (hs : IsSimple r) {p : Point} (hp : List.getLast? r = some p) {e : Point × Point} (he : e ∈ List.consecutivePairs r) (hm : realPoint p ∈ segment e.1 e.2) : p = e.1 ∨ p = e.2

A simple route's final listed vertex can lie on one of its segments only as an endpoint.

theorem Cslib.Orthogonal.isOrthogonal_join {q r : Route} {p : Point} (hq : List.getLast? q = some p) (hr : List.head? r = some p) (hoq : IsOrthogonal q) (hor : IsOrthogonal r) : IsOrthogonal (q ++ List.tail r)

Joining properly orthogonal routes at their common listed endpoint remains orthogonal.

theorem Cslib.Orthogonal.isSimple_join {q r : Route} {p : Point} (hq : List.getLast? q = some p) (hr : List.head? r = some p) (hsq : IsSimple q) (hsr : IsSimple r) (hc : ∀ z ∈ support q, z ∈ support r → z = realPoint p) : IsSimple (q ++ List.tail r)

Joining simple routes whose only continuous intersection is their common endpoint introduces neither repeated listed points nor forbidden segment contacts.