Horizontal reflection of orthogonal routes

Main definitions

• mirrorPoint, mirrorReal, mirrorRoute: reflection in the vertical axis.

Main results

• support_mirrorRoute, isOrthogonal_mirrorRoute_iff, isSimple_mirrorRoute_iff.
• wireLength_mirrorRoute: reflection preserves Manhattan wire length.

References

These elementary affine-coordinate lemmas and proofs are original.

def Cslib.Orthogonal.mirrorPoint (p : Point) : Point

Horizontal reflection of integer points.

def Cslib.Orthogonal.mirrorReal (p : ℝ × ℝ) : ℝ × ℝ

The corresponding horizontal reflection in the real plane.

def Cslib.Orthogonal.mirrorRoute (r : Route) : Route

Reflect every listed point.

theorem Cslib.Orthogonal.realPoint_mirrorPoint (p : Point) : realPoint (mirrorPoint p) = mirrorReal (realPoint p)

Integer and real reflections commute with inclusion of the lattice.

theorem Cslib.Orthogonal.segment_mirrorPoint (a b : Point) : segment (mirrorPoint a) (mirrorPoint b) = mirrorReal '' segment a b

Reflection maps complete real segments.

theorem Cslib.Orthogonal.mem_segment_mirrorPoint_iff (a b : Point) (p : ℝ × ℝ) : mirrorReal p ∈ segment (mirrorPoint a) (mirrorPoint b) ↔ p ∈ segment a b

Reflected segment membership is reflected membership.

theorem Cslib.Orthogonal.consecutivePairs_mirrorRoute (r : Route) : List.consecutivePairs (mirrorRoute r) = List.map (fun (e : Point × Point) => (mirrorPoint e.1, mirrorPoint e.2)) (List.consecutivePairs r)

Reflection maps every listed segment without changing its index.

theorem Cslib.Orthogonal.support_mirrorRoute (r : Route) : support (mirrorRoute r) = mirrorReal '' support r

Reflection maps the entire continuous route support.

theorem Cslib.Orthogonal.isOrthogonal_mirrorRoute_iff (r : Route) : IsOrthogonal (mirrorRoute r) ↔ IsOrthogonal r

Reflection preserves proper orthogonality.

theorem Cslib.Orthogonal.isSimple_mirrorRoute_iff (r : Route) : IsSimple (mirrorRoute r) ↔ IsSimple r

Reflection preserves continuous simplicity.

theorem Cslib.Orthogonal.wireLength_mirrorRoute (r : Route) : wireLength (mirrorRoute r) = wireLength r

Reflection preserves total Manhattan wire length.