Orientation independence of orthogonal incidence routes

Reversing a route preserves its full real support, proper orthogonality, continuous simplicity, Manhattan wire length, and segment count. This normalizes supplied incidence routes without changing their drawing.

Main results

• support_reverse, isOrthogonal_reverse_iff, isSimple_reverse_iff.
• wireLength_reverse, consecutivePairs_length_reverse.

References

These finite-route reversal lemmas and proofs are original.

theorem Cslib.Orthogonal.consecutivePairs_reverse (r : Route) : (List.reverse r).consecutivePairs = List.map Prod.swap (List.consecutivePairs r).reverse

Reversal reverses segment order and swaps each segment's endpoints.

theorem Cslib.Orthogonal.consecutivePairs_length_reverse (r : Route) : (List.reverse r).consecutivePairs.length = (List.consecutivePairs r).length

Reversal preserves the number of listed segments.

theorem Cslib.Orthogonal.support_reverse (r : Route) : support (List.reverse r) = support r

Reversal preserves the entire continuous support.

theorem Cslib.Orthogonal.isOrthogonal_reverse_iff (r : Route) : IsOrthogonal (List.reverse r) ↔ IsOrthogonal r

Reversal preserves proper orthogonality.

theorem Cslib.Orthogonal.isSimple_reverse_iff (r : Route) : IsSimple (List.reverse r) ↔ IsSimple r

Reversal preserves continuous simplicity.

theorem Cslib.Orthogonal.wireLength_reverse (r : Route) : wireLength (List.reverse r) = wireLength r

Reversal preserves total Manhattan wire length.