Fixed-distance cutting of dilated incidence routes

After dilation by k, every original proper integer segment has length at least k. Consequently a fixed radius < k can be removed from the initial segment of every route. The operation preserves the original list length, proper orthogonality, and continuous simplicity, shrinks the dilated support, and removes exactly radius units of wire.

Main definitions

• cutPoint: the point at a fixed distance along a dilated first segment.
• cutStart: dilate a route and remove a fixed initial distance.

Main results

• isOrthogonal_cutStart, isSimple_cutStart, support_cutStart_subset.
• length_cutStart, wireLength_cutStart.

References

The integer-grid endpoint refinement and proofs are original.

def Cslib.Orthogonal.cutPoint (k radius : ℕ) (a b : Point) : Point

A point at a fixed distance along a dilated segment's cardinal direction.

def Cslib.Orthogonal.cutStart (k radius : ℕ) : Route → Route

Dilate a route and cut a fixed length from its first segment. Degenerate input lists are merely dilated; geometric correctness is stated for proper routes of length at least two.

theorem Cslib.Orthogonal.length_pos_of_axisAligned {a b : Point} (hab : AxisAligned a b) : 0 < length a b

A proper integer segment has positive Manhattan length.

theorem Cslib.Orthogonal.length_add_nsmul_unit (a d : Point) (n : ℕ) (hd : UnitVector d) : length a (a + n • d) = n

Multiples along a cardinal ray have their expected Manhattan distances.

theorem Cslib.Orthogonal.nsmul_unit_injective (a d : Point) (hd : UnitVector d) : Function.Injective fun (n : ℕ) => a + n • d

Distinct natural distances specify distinct points along a cardinal ray.

theorem Cslib.Orthogonal.cutPoint_mem_segment {a b : Point} (hab : AxisAligned a b) {k radius : ℕ} (hr : radius < k) : realPoint (cutPoint k radius a b) ∈ segment (k • a) (k • b)

A cut shorter than the dilation factor lies on every dilated proper first segment.

theorem Cslib.Orthogonal.cutPoint_ne_endpoint {a b : Point} (hab : AxisAligned a b) {k radius : ℕ} (hr : radius < k) : cutPoint k radius a b ≠ k • b

A short cut never reaches the other endpoint of a proper dilated first segment.

theorem Cslib.Orthogonal.length_cutStart (k radius : ℕ) (r : Route) : List.length (cutStart k radius r) = List.length r

Cutting never changes the number of listed route points.

theorem Cslib.Orthogonal.consecutivePairs_length_cutStart (k radius : ℕ) (r : Route) : (List.consecutivePairs (cutStart k radius r)).length = (List.consecutivePairs r).length

Cutting never changes the number of listed segments.

theorem Cslib.Orthogonal.isOrthogonal_cutStart {r : Route} (ho : IsOrthogonal r) {k radius : ℕ} (hr : radius < k) : IsOrthogonal (cutStart k radius r)

The fixed cut preserves proper orthogonality.

theorem Cslib.Orthogonal.isSimple_cutStart {r : Route} (ho : IsOrthogonal r) (hs : IsSimple r) {k radius : ℕ} (hr : radius < k) : IsSimple (cutStart k radius r)

The fixed cut preserves continuous route simplicity.

theorem Cslib.Orthogonal.support_cutStart_subset {r : Route} (ho : IsOrthogonal r) {k radius : ℕ} (hr : radius < k) : support (cutStart k radius r) ⊆ support (dilateRoute k r)

Every point of the cut route still belongs to the original dilated route.

theorem Cslib.Orthogonal.length_cutPoint (k radius : ℕ) (a b : Point) : length (k • a) (cutPoint k radius a b) = radius

The removed initial segment has precisely the chosen radius.

theorem Cslib.Orthogonal.wireLength_cutStart {r : Route} (ho : IsOrthogonal r) (hlen : 2 ≤ List.length r) {k radius : ℕ} (hr : radius < k) : wireLength (cutStart k radius r) + radius = k * wireLength r

A proper route loses exactly the chosen radius from its dilated wire length.

def Cslib.Orthogonal.inPointBox (a : Point) (radius : ℕ) (p : ℝ × ℝ) : Prop

A closed real square centered on an integer grid point.

theorem Cslib.Orthogonal.near_of_scaled_box {a : Point} {q : ℝ × ℝ} {k radius : ℕ} (hr : radius < k) (hb : inPointBox (k • a) radius (↑k • q)) : nearGridPoint a q

A box smaller than the integer dilation factor lies within the original open unit box after dividing by that factor.

theorem Cslib.Orthogonal.cutStart_box_contact {a b : Point} {r : Route} (ho : IsOrthogonal (a :: b :: r)) (hs : IsSimple (a :: b :: r)) {k radius : ℕ} (hr : radius < k) {p : ℝ × ℝ} (hp : p ∈ support (cutStart k radius (a :: b :: r))) (hb : inPointBox (k • a) radius p) : p = realPoint (cutPoint k radius a b)

The trimmed exterior route meets the closed local clause box only at its designated cut port. This controls all real points of the route.

theorem Cslib.Orthogonal.eq_of_inPointBoxes {a b : Point} {k radius : ℕ} (hr : 2 * radius < k) {p : ℝ × ℝ} (ha : inPointBox (k • a) radius p) (hb : inPointBox (k • b) radius p) : a = b

Closed local boxes about distinct integer source vertices cannot meet when the dilation factor is larger than twice their radius.

theorem Cslib.Orthogonal.pointBoxes_disjoint {a b : Point} (hab : a ≠ b) {k radius : ℕ} (hr : 2 * radius < k) : Disjoint {p : ℝ × ℝ | inPointBox (k • a) radius p} {p : ℝ × ℝ | inPointBox (k • b) radius p}

Distinct source vertices have disjoint closed local boxes under a sufficiently large integer dilation.