Finite orthogonal polygonal routes

The data are lists of integer points. Their geometric interpretation uses Mathlib's closed real segments, including every real point between consecutive listed points, rather than only lattice points. A singleton route has singleton support; an empty route has empty support.

Main definitions

• Cslib.Orthogonal.Point, Cslib.Orthogonal.Route: finite integer-coordinate data.
• Cslib.Orthogonal.support: the continuous support of a polygonal route.
• Cslib.Orthogonal.IsOrthogonal: every consecutive segment is axis aligned and nondegenerate.
• Cslib.Orthogonal.wireLength: total Manhattan length.

Main results

• Cslib.Orthogonal.mem_horizontal, Cslib.Orthogonal.mem_vertical: real segment membership characterized by coordinate intervals.

References

The finite-route definitions and proofs are original.

@[reducible, inline]

abbrev Cslib.Orthogonal.Point : Type

An integer grid point.

@[reducible, inline]

abbrev Cslib.Orthogonal.Route : Type

Explicit finite polygonal route data.

def Cslib.Orthogonal.realPoint (p : Point) : ℝ × ℝ

Inclusion of the integer grid into the real plane.

theorem Cslib.Orthogonal.realPoint_injective : Function.Injective realPoint

The geometric inclusion does not identify distinct grid points.

def Cslib.Orthogonal.segment (a b : Point) : Set (ℝ × ℝ)

A closed real segment between two integer grid points.

def Cslib.Orthogonal.support (r : Route) : Set (ℝ × ℝ)

All real points on a finite polygonal route, including isolated listed points.

theorem Cslib.Orthogonal.support_cons_cons (a b : Point) (r : Route) : support (a :: b :: r) = segment a b ∪ support (b :: r)

Splitting off the first segment agrees with the continuous polygonal support.

def Cslib.Orthogonal.AxisAligned (a b : Point) : Prop

A proper axis-aligned segment; zero-length segments are excluded.

@[instance_reducible]

instance Cslib.Orthogonal.instDecidableAxisAligned (a b : Point) : Decidable (AxisAligned a b)

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

Every consecutive segment is proper and axis aligned.

@[instance_reducible]

instance Cslib.Orthogonal.instDecidablePredRouteIsOrthogonal : DecidablePred IsOrthogonal

Orthogonality is decidable by checking the finitely many consecutive segments.

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

Removing the initial listed point preserves proper orthogonality.

def Cslib.Orthogonal.length (a b : Point) : ℕ

Manhattan length of one segment.

theorem Cslib.Orthogonal.axisAligned_of_length_eq_one {a b : Point} (h : length a b = 1) : AxisAligned a b

A pair of lattice points one Manhattan unit apart forms a proper axis-aligned segment.

def Cslib.Orthogonal.wireLength (r : Route) : ℕ

Total Manhattan length of the consecutive segments.

theorem Cslib.Orthogonal.length_le_box {a b : Point} {w h : ℕ} (ha : 0 ≤ a.1 ∧ a.1 ≤ ↑w ∧ 0 ≤ a.2 ∧ a.2 ≤ ↑h) (hb : 0 ≤ b.1 ∧ b.1 ≤ ↑w ∧ 0 ≤ b.2 ∧ b.2 ≤ ↑h) : length a b ≤ w + h

A bounding rectangle controls the length of any one segment.

theorem Cslib.Orthogonal.wireLength_le_box {r : Route} {w h : ℕ} (hr : ∀ p ∈ r, 0 ≤ p.1 ∧ p.1 ≤ ↑w ∧ 0 ≤ p.2 ∧ p.2 ≤ ↑h) : wireLength r ≤ (List.consecutivePairs r).length * (w + h)

Bounding all listed points bounds the total wire length by the number of segments times the sum of the rectangle sides.

def Cslib.Orthogonal.Transverse (a b c d : Point) (p : ℝ × ℝ) : Prop

A strict transverse horizontal/vertical crossing at a real point. The strict inequalities exclude endpoints and bends.

theorem Cslib.Orthogonal.mem_segment_bounds {a b : Point} {p : ℝ × ℝ} (hp : p ∈ segment a b) : p.1 ∈ Set.uIcc ↑a.1 ↑b.1 ∧ p.2 ∈ Set.uIcc ↑a.2 ↑b.2

Every real segment lies in its coordinate bounding rectangle.

theorem Cslib.Orthogonal.mem_horizontal {a b y : ℝ} {p : ℝ × ℝ} : p ∈ _root_.segment ℝ (a, y) (b, y) ↔ p.2 = y ∧ p.1 ∈ Set.uIcc a b

Horizontal real segment membership is a one-dimensional interval test.

theorem Cslib.Orthogonal.mem_vertical {x a b : ℝ} {p : ℝ × ℝ} : p ∈ _root_.segment ℝ (x, a) (x, b) ↔ p.1 = x ∧ p.2 ∈ Set.uIcc a b

Vertical real segment membership is a one-dimensional interval test.

theorem Cslib.Orthogonal.realPoint_mem_segment_iff {a b p : Point} (h : a.1 = b.1 ∨ a.2 = b.2) : realPoint p ∈ segment a b ↔ min a.1 b.1 ≤ p.1 ∧ p.1 ≤ max a.1 b.1 ∧ min a.2 b.2 ≤ p.2 ∧ p.2 ≤ max a.2 b.2

Integer points on an axis-aligned segment can be checked using integer inequalities.

theorem Cslib.Orthogonal.realPoint_mem_support_iff {r : Route} (hr : IsOrthogonal r) (p : Point) : realPoint p ∈ support r ↔ p ∈ r ∨ ∃ e ∈ List.consecutivePairs r, min e.1.1 e.2.1 ≤ p.1 ∧ p.1 ≤ max e.1.1 e.2.1 ∧ min e.1.2 e.2.2 ≤ p.2 ∧ p.2 ≤ max e.1.2 e.2.2

Integer-point membership in an orthogonal route is an entirely integer-arithmetic test, while its meaning remains membership in the continuous real support.