Documentation

Complexity.Foundations.Geometry.Orthogonal.Isolation

Integer-grid isolation for local drawing replacements #

An orthogonal segment with integer endpoints that enters the open unit box 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 #

Main results #

References #

These integer-grid separation observations and proofs are original.

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

The open unit square centered on an integer grid point.

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

    Distinct grid points are not within the open unit box about one another.

    source
    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 unit box about a grid point forces an integer orthogonal segment to contain that grid point. The statement concerns all real points of the segment.

    source
    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 unit box disjoint from a route.

    source
    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.

    source
    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 unit box about a route's initial vertex meets only its first segment.

    source
    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 unit box about the route's initial grid vertex.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.