Unit subdivision of finite orthogonal routes

Main definitions

• Cslib.Orthogonal.walk: a finite sequence of repeated integer vector steps.
• Cslib.Orthogonal.segmentWalk, Cslib.Orthogonal.subdivide: unit subdivision of a segment or an entire polygonal route, listing a shared endpoint only once.
• Cslib.Orthogonal.subdivideWithin: finite enumeration capped by a per-segment step budget.

Main results

• Cslib.Orthogonal.walk_length, Cslib.Orthogonal.walk_head, Cslib.Orthogonal.walk_last: size and endpoint formulas.
• Cslib.Orthogonal.subdivide_head, Cslib.Orthogonal.subdivide_last: endpoint preservation.
• Cslib.Orthogonal.subdivide_length: exact point count from original Manhattan wire length.
• Cslib.Orthogonal.subdivide_unit: every subdivided segment has Manhattan length one.
• Cslib.Orthogonal.support_subdivide: equality of the complete continuous real supports.
• Cslib.Orthogonal.wireLength_subdivide: exact wire-length preservation.
• Cslib.Orthogonal.subdivide_nodup: continuously simple orthogonal routes subdivide without repeating lattice points.
• Cslib.Orthogonal.subdivideWithin_eq_of_wireLength_le: recover full subdivision from a sufficient total-wire budget.
• Cslib.Orthogonal.subdivideWithin_length_le: explicit bounded output size.

References

The unit-walk construction and bounded enumeration are original.

def Cslib.Orthogonal.walk (a d : Point) : ℕ → Route

The k+1 lattice points obtained by taking k copies of vector d from a.

@[simp]

theorem Cslib.Orthogonal.walk_length (a d : Point) (k : ℕ) : List.length (walk a d k) = k + 1

One more listed point than steps.

@[simp]

theorem Cslib.Orthogonal.walk_head (a d : Point) (k : ℕ) : List.head? (walk a d k) = some a

The walk always starts at its prescribed first point.

@[simp]

theorem Cslib.Orthogonal.walk_last (a d : Point) (k : ℕ) : List.getLast? (walk a d k) = some (a + k • d)

The walk ends after precisely k copies of the step vector.

def Cslib.Orthogonal.UnitVector (d : Point) : Prop

A step vector in one of the four cardinal unit directions.

theorem Cslib.Orthogonal.support_walk (a d : Point) (k : ℕ) (hd : UnitVector d) : support (walk a d k) = segment a (a + k • d)

Cardinal walks cover exactly the original continuous segment.

theorem Cslib.Orthogonal.walk_step {a d : Point} {k : ℕ} {e : Point × Point} (he : e ∈ List.consecutivePairs (walk a d k)) : e.2 = e.1 + d

Every consecutive pair in a repeated walk is exactly one prescribed step.

theorem Cslib.Orthogonal.length_add_unit (a d : Point) (hd : UnitVector d) : length a (a + d) = 1

Cardinal steps have Manhattan length one.

theorem Cslib.Orthogonal.walk_unit {a d : Point} {k : ℕ} (hd : UnitVector d) {e : Point × Point} (he : e ∈ List.consecutivePairs (walk a d k)) : length e.1 e.2 = 1

Every consecutive pair of a cardinal walk is unit-adjacent.

theorem Cslib.Orthogonal.wireLength_walk (a d : Point) (k : ℕ) (hd : UnitVector d) : wireLength (walk a d k) = k

A k-step cardinal walk has exactly k units of wire.

def Cslib.Orthogonal.direction (a b : Point) : Point

Cardinal direction from a toward b; equal points use an arbitrary unit direction.

theorem Cslib.Orthogonal.direction_unit (a b : Point) : UnitVector (direction a b)

The chosen direction is always a cardinal unit vector.

theorem Cslib.Orthogonal.add_length_direction {a b : Point} (h : a.1 = b.1 ∨ a.2 = b.2) : a + length a b • direction a b = b

An axis-aligned displacement is its Manhattan length times its chosen unit direction.

def Cslib.Orthogonal.segmentWalk (a b : Point) : Route

Unit subdivision of one segment, including both endpoints.

@[simp]

theorem Cslib.Orthogonal.segmentWalk_length (a b : Point) : List.length (segmentWalk a b) = length a b + 1

Segment subdivision uses exactly one more point than its Manhattan length.

@[simp]

theorem Cslib.Orthogonal.segmentWalk_head (a b : Point) : List.head? (segmentWalk a b) = some a

Segment subdivision preserves the first endpoint.

theorem Cslib.Orthogonal.segmentWalk_last {a b : Point} (h : a.1 = b.1 ∨ a.2 = b.2) : List.getLast? (segmentWalk a b) = some b

Segment subdivision preserves the last endpoint of every axis-aligned segment.

theorem Cslib.Orthogonal.support_segmentWalk {a b : Point} (h : a.1 = b.1 ∨ a.2 = b.2) : support (segmentWalk a b) = segment a b

The subdivision covers the entire original real segment, without adding points.

theorem Cslib.Orthogonal.segmentWalk_unit (a b : Point) {e : Point × Point} (he : e ∈ List.consecutivePairs (segmentWalk a b)) : length e.1 e.2 = 1

Each subdivided segment has unit Manhattan length.

theorem Cslib.Orthogonal.wireLength_segmentWalk (a b : Point) : wireLength (segmentWalk a b) = length a b

Segment subdivision preserves wire length exactly.

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

Joining routes at a common endpoint, listing that endpoint once, concatenates their segment lists.

theorem Cslib.Orthogonal.support_join {q r : Route} {p : Point} (hq : List.getLast? q = some p) (hr : List.head? r = some p) : support (q ++ List.tail r) = support q ∪ support r

Joining routes at their common endpoint takes the union of their full real supports.

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

A route joined at a common endpoint has the last endpoint of the second route.

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

Joining at a common endpoint adds the two Manhattan wire lengths.

def Cslib.Orthogonal.subdivide : Route → Route

Replace each consecutive segment by its unit walk, retaining a shared endpoint once.

@[simp]

theorem Cslib.Orthogonal.subdivide_head (r : Route) : List.head? (subdivide r) = List.head? r

Subdivision preserves the first listed point, including the empty-route convention.

theorem Cslib.Orthogonal.subdivide_length (r : Route) : List.length (subdivide r) = wireLength r + if r = [] then 0 else 1

The exact point count is wire length plus one for a nonempty route.

theorem Cslib.Orthogonal.subdivide_last {r : Route} (hr : IsOrthogonal r) : List.getLast? (subdivide r) = List.getLast? r

Subdivision preserves the final endpoint of an orthogonal route.

theorem Cslib.Orthogonal.support_subdivide {r : Route} (hr : IsOrthogonal r) : support (subdivide r) = support r

Subdivision preserves the complete real support of every orthogonal route.

theorem Cslib.Orthogonal.subdivide_unit {r : Route} (hr : IsOrthogonal r) {e : Point × Point} (he : e ∈ List.consecutivePairs (subdivide r)) : length e.1 e.2 = 1

Every consecutive pair in the subdivided orthogonal route is a unit grid step.

theorem Cslib.Orthogonal.wireLength_subdivide {r : Route} (hr : IsOrthogonal r) : wireLength (subdivide r) = wireLength r

Unit subdivision preserves total Manhattan wire length exactly.

theorem Cslib.Orthogonal.subdivide_orthogonal {r : Route} (hr : IsOrthogonal r) : IsOrthogonal (subdivide r)

Unit subdivision is itself a proper orthogonal route.

theorem Cslib.Orthogonal.walk_eq_map_range (a d : Point) (k : ℕ) : walk a d k = List.map (fun (i : ℕ) => a + i • d) (List.range (k + 1))

The recursive walk is also an explicit range enumeration.

theorem Cslib.Orthogonal.walk_dropLast_eq_map_range (a d : Point) (k : ℕ) : List.dropLast (walk a d k) = List.map (fun (i : ℕ) => a + i • d) (List.range k)

Omitting the final endpoint gives exactly the strict prefix of the range enumeration.

theorem Cslib.Orthogonal.subdivide_eq_flatMap {r : Route} (hr : IsOrthogonal r) : subdivide r = List.flatMap (fun (e : Point × Point) => List.dropLast (segmentWalk e.1 e.2)) (List.consecutivePairs r) ++ (List.getLast? r).toList

A flat enumeration of the unit subdivision: emit each segment without its last point, then emit the route's final endpoint. This form supports bounded polynomial-time implementations.

def Cslib.Orthogonal.subdivideWithin (budget : ℕ) (r : Route) : Route

Enumerate at most budget strict unit-prefix points per listed segment, then the last endpoint. The result agrees with subdivide when every segment fits in the budget.

theorem Cslib.Orthogonal.subdivideWithin_eq_subdivide {r : Route} (hr : IsOrthogonal r) {budget : ℕ} (hbudget : ∀ e ∈ List.consecutivePairs r, length e.1 e.2 ≤ budget) : subdivideWithin budget r = subdivide r

A sufficient per-segment budget recovers the complete geometric subdivision.

theorem Cslib.Orthogonal.subdivideWithin_length_le (budget : ℕ) (r : Route) : List.length (subdivideWithin budget r) ≤ budget * (List.consecutivePairs r).length + 1

Bounded enumeration emits at most budget points per segment, plus the last endpoint.

theorem Cslib.Orthogonal.length_le_wireLength {r : Route} {e : Point × Point} (he : e ∈ List.consecutivePairs r) : length e.1 e.2 ≤ wireLength r

Each listed segment's length is bounded by the route's total wire length.

theorem Cslib.Orthogonal.subdivideWithin_eq_of_wireLength_le {r : Route} (hr : IsOrthogonal r) {budget : ℕ} (hbudget : wireLength r ≤ budget) : subdivideWithin budget r = subdivide r

A bound for the whole route's wire length is a sufficient subdivision budget.

theorem Cslib.Orthogonal.walk_nodup (a d : Point) (k : ℕ) (hd : UnitVector d) : List.Nodup (walk a d k)

A cardinal walk never repeats a lattice point.

theorem Cslib.Orthogonal.segmentWalk_nodup (a b : Point) : List.Nodup (segmentWalk a b)

The unit walk along one segment has no repeated listed point.

theorem Cslib.Orthogonal.mem_support_segment {r : Route} (hlen : 2 ≤ List.length r) {p : ℝ × ℝ} (hp : p ∈ support r) : ∃ e ∈ List.consecutivePairs r, p ∈ segment e.1 e.2

Every supported point of a route with at least two listed points belongs to one of its consecutive segments. In this case separate degenerate pieces for listed points are redundant.

theorem Cslib.Orthogonal.first_segment_tail_contact {a b : Point} {r : Route} (hs : IsSimple (a :: b :: r)) {p : ℝ × ℝ} (hp : p ∈ segment a b) (hq : p ∈ support (b :: r)) : p = realPoint b

The first segment of a continuously simple route meets its tail only at their common listed endpoint.

theorem Cslib.Orthogonal.subdivide_nodup {r : Route} (hr : IsOrthogonal r) (hs : IsSimple r) : List.Nodup (subdivide r)

Unit subdivision of a continuously simple orthogonal route has no repeated lattice points. The proof uses the original segments' endpoint-contact certificates, not support equality alone.

theorem Cslib.Orthogonal.subdivideWithin_nodup {r : Route} (hr : IsOrthogonal r) (hs : IsSimple r) {budget : ℕ} (hbudget : wireLength r ≤ budget) : List.Nodup (subdivideWithin budget r)

A sufficient-budget native enumeration also has no repeated points on a simple route.