Documentation

Complexity.Foundations.Geometry.Orthogonal.Scale

Integer dilation of orthogonal drawings #

Positive integer dilation preserves continuous route supports, proper orthogonality, and simplicity, multiplies Manhattan wire length, and preserves the number of listed segments.

Main definitions #

Main results #

References #

These elementary affine-coordinate lemmas and proofs are original.

source
def Cslib.Orthogonal.dilateRoute (k : ℕ) (r : Route) :
Route

Dilate each listed integer point by the same natural factor.

Instances For
    source
    theorem Cslib.Orthogonal.realPoint_nsmul (k : ℕ) (p : Point) :
    realPoint (k • p) = ↑k • realPoint p

    Integer dilation commutes with inclusion into the real plane.

    source
    theorem Cslib.Orthogonal.nsmul_point_injective {k : ℕ} (hk : k ≠ 0) :
    Function.Injective fun (p : Point) => k • p

    Positive integer dilation is injective on grid points.

    source
    theorem Cslib.Orthogonal.segment_nsmul (k : ℕ) (a b : Point) :
    segment (k • a) (k • b) = (fun (p : ℝ × ℝ) => ↑k • p) '' segment a b

    The segment between dilated endpoints is the dilation of the original real segment.

    source
    theorem Cslib.Orthogonal.mem_segment_nsmul_iff {k : ℕ} (hk : k ≠ 0) (a b : Point) (p : ℝ × ℝ) :
    ↑k • p ∈ segment (k • a) (k • b) ↔ p ∈ segment a b

    Membership in a dilated segment is exactly dilated membership.

    source
    theorem Cslib.Orthogonal.consecutivePairs_dilateRoute (k : ℕ) (r : Route) :
    List.consecutivePairs (dilateRoute k r) = List.map (fun (e : Point × Point) => (k • e.1, k • e.2)) (List.consecutivePairs r)

    Dilation maps the consecutive segments in their unchanged order.

    source
    theorem Cslib.Orthogonal.consecutivePairs_length_dilateRoute (k : ℕ) (r : Route) :
    (List.consecutivePairs (dilateRoute k r)).length = (List.consecutivePairs r).length

    Dilation leaves the number of listed segments unchanged.

    source
    theorem Cslib.Orthogonal.support_dilateRoute (k : ℕ) (r : Route) :
    support (dilateRoute k r) = (fun (p : ℝ × ℝ) => ↑k • p) '' support r

    Dilation maps the entire real polygonal support, including singleton routes.

    source
    theorem Cslib.Orthogonal.axisAligned_nsmul_iff {k : ℕ} (hk : k ≠ 0) (a b : Point) :
    AxisAligned (k • a) (k • b) ↔ AxisAligned a b

    Proper axis alignment is invariant under positive integer dilation.

    source
    theorem Cslib.Orthogonal.isOrthogonal_dilateRoute_iff {k : ℕ} (hk : k ≠ 0) (r : Route) :
    IsOrthogonal (dilateRoute k r) ↔ IsOrthogonal r

    Proper orthogonality is invariant under positive integer dilation.

    source
    theorem Cslib.Orthogonal.length_nsmul (k : ℕ) (a b : Point) :
    length (k • a) (k • b) = k * length a b

    Every Manhattan segment length is multiplied by the dilation factor.

    source
    theorem Cslib.Orthogonal.wireLength_dilateRoute (k : ℕ) (r : Route) :
    wireLength (dilateRoute k r) = k * wireLength r

    Total Manhattan wire length is multiplied by the dilation factor.

    source
    theorem Cslib.Orthogonal.endpointContacts_nsmul_iff {k : ℕ} (hk : k ≠ 0) (a b c d : Point) :
    EndpointContacts (k • a) (k • b) (k • c) (k • d) ↔ EndpointContacts a b c d

    Endpoint-only segment contacts are invariant under positive integer dilation.

    source
    theorem Cslib.Orthogonal.isSimple_dilateRoute_iff {k : ℕ} (hk : k ≠ 0) (r : Route) :
    IsSimple (dilateRoute k r) ↔ IsSimple r

    Continuous simplicity is invariant under positive integer dilation.