Integer-grid isolation for local drawing replacements

An orthogonal segment with integer endpoints that enters the open box of radius 1 about an integer point must contain that integer point. In a simple route, only the initial segment can contain its initial vertex. These facts supply uniform local isolation without searching for a drawing-dependent real radius.

Main definitions

• nearGridPoint: the open box of radius 1 about an integer point, an open square of side 2.

Main results

• gridPoint_mem_segment_of_near, gridPoint_mem_support_of_near.
• segment_eq_first_of_head_mem, mem_first_segment_of_near_head.

References

These integer-grid separation observations and proofs are original.

def Cslib.Orthogonal.nearGridPoint (c : Point) (p : ℝ × ℝ) : Prop

The open box of radius 1 about an integer grid point: an open square of side 2.

theorem Cslib.Orthogonal.eq_of_nearGridPoint {a c : Point} (h : nearGridPoint c (realPoint a)) : a = c

Distinct grid points are not within the open box of radius 1 about one another.

theorem Cslib.Orthogonal.gridPoint_mem_segment_of_near {a b c : Point} (hab : a.1 = b.1 ∨ a.2 = b.2) {p : ℝ × ℝ} (hp : p ∈ segment a b) (hc : nearGridPoint c p) : realPoint c ∈ segment a b

Entering the open box of radius 1 about a grid point forces an integer orthogonal segment to contain that grid point. The statement concerns all real points of the segment.

theorem Cslib.Orthogonal.gridPoint_mem_support_of_near {r : Route} (hr : IsOrthogonal r) {c : Point} {p : ℝ × ℝ} (hp : p ∈ support r) (hc : nearGridPoint c p) : realPoint c ∈ support r

A nonincident integer vertex has a whole open box of radius 1 disjoint from an orthogonal route.

theorem Cslib.Orthogonal.segment_eq_first_of_head_mem {a b : Point} {r : Route} (hr : IsSimple (a :: b :: r)) {e : Point × Point} (he : e ∈ (a :: b :: r).consecutivePairs) (ha : realPoint a ∈ segment e.1 e.2) : e = (a, b)

In a simple route, the initial grid vertex lies on no segment other than the first.

theorem Cslib.Orthogonal.mem_first_segment_of_near_head {a b : Point} {r : Route} (ho : IsOrthogonal (a :: b :: r)) (hs : IsSimple (a :: b :: r)) {p : ℝ × ℝ} (hp : p ∈ support (a :: b :: r)) (ha : nearGridPoint a p) : p ∈ segment a b

The open box of radius 1 about the initial vertex of a simple orthogonal route meets only the route's first segment.

theorem Cslib.Orthogonal.not_near_head_tail {a b : Point} {r : Route} (ho : IsOrthogonal (a :: b :: r)) (hs : IsSimple (a :: b :: r)) {p : ℝ × ℝ} (hp : p ∈ support (b :: r)) : ¬nearGridPoint a p

The tail of a simple proper orthogonal route avoids the entire open box of radius 1 about the route's initial grid vertex.

theorem Cslib.Orthogonal.axisAligned_cut_first {a b c : Point} (hab : a.1 = b.1 ∨ a.2 = b.2) (hc : realPoint c ∈ segment a b) (hcb : c ≠ b) : AxisAligned c b

Cutting the first segment at one of its grid points preserves proper axis alignment provided the new segment has not collapsed.

theorem Cslib.Orthogonal.support_cut_first_subset {a b c : Point} {r : Route} (hc : realPoint c ∈ segment a b) : support (c :: b :: r) ⊆ support (a :: b :: r)

Removing an initial portion of the first segment only shrinks a route's real support.

theorem Cslib.Orthogonal.isOrthogonal_cut_first {a b c : Point} {r : Route} (hr : IsOrthogonal (a :: b :: r)) (hc : realPoint c ∈ segment a b) (hcb : c ≠ b) : IsOrthogonal (c :: b :: r)

Endpoint cutting preserves a route's orthogonality.

theorem Cslib.Orthogonal.isSimple_cut_first {a b c : Point} {r : Route} (hr : IsSimple (a :: b :: r)) (hc : realPoint c ∈ segment a b) (hcb : c ≠ b) : IsSimple (c :: b :: r)

Moving the initial endpoint forward within its first segment preserves continuous simplicity. No repeated point or contact with a later segment is introduced.

theorem Cslib.Orthogonal.length_add_cut_first {a b c : Point} (hab : a.1 = b.1 ∨ a.2 = b.2) (hc : realPoint c ∈ segment a b) : length a c + length c b = length a b

Manhattan length is additive when a grid point lies on an orthogonal segment.

theorem Cslib.Orthogonal.wireLength_cut_first {a b c : Point} {r : Route} (hab : a.1 = b.1 ∨ a.2 = b.2) (hc : realPoint c ∈ segment a b) : wireLength (c :: b :: r) + length a c = wireLength (a :: b :: r)

Endpoint cutting subtracts exactly the removed Manhattan length.