Exterior routes for clause-box replacement

An incidence edge is normalized from its second endpoint (the clause vertex) to its first endpoint (the variable vertex), independently of the supplied route orientation. Dilation and initial trimming provide an exterior route with a single contact with its clause box. The normalization changes neither route support nor geometric costs.

Main definitions

• sourceRoute, sourceDirection: the normalized source incidence and its exit direction.
• exteriorRoute, exteriorPort: the scaled, trimmed incidence and its designated box port.

Main results

• sourceRoute_endpoints, sourceRoute_regular: normalized source-route correctness.
• sourceDirection_ne: distinct incidences at a clause use distinct cardinal directions.
• exteriorRoute_box_contact: the exterior route meets its own closed box only at the port.
• exteriorRoute_avoids_box: nonincident source vertices have disjoint replacement boxes.

References

The source normalization and geometric assembly proofs are original.

def Cslib.Complexity.SAT.ExactOne.sourceStart (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Point

The clause endpoint of a listed incidence, with a fixed fallback for invalid indices.

def Cslib.Complexity.SAT.ExactOne.sourceFinish (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Point

The variable endpoint of a listed incidence, with a fixed fallback for invalid indices.

def Cslib.Complexity.SAT.ExactOne.sourceRoute (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Route

Normalize the supplied incidence route to begin at its clause endpoint.

theorem Cslib.Complexity.SAT.ExactOne.drawingPosition_injOn {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {v w : ℕ} (hv : v ∈ G.vertices) (hw : w ∈ G.vertices) (he : G.drawingPosition d v = G.drawingPosition d w) : v = w

Declared vertices with equal positions are equal in a valid drawing.

theorem Cslib.Complexity.SAT.ExactOne.support_sourceRoute (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.support (sourceRoute G d i) = Orthogonal.support (d.2.getD i [])

Normalization preserves the complete continuous support of each supplied route.

theorem Cslib.Complexity.SAT.ExactOne.length_sourceRoute (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : List.length (sourceRoute G d i) = List.length (d.2.getD i [])

Normalization preserves the number of route points.

theorem Cslib.Complexity.SAT.ExactOne.consecutivePairs_length_sourceRoute (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : (List.consecutivePairs (sourceRoute G d i)).length = (List.consecutivePairs (d.2.getD i [])).length

Normalization preserves the number of segments.

theorem Cslib.Complexity.SAT.ExactOne.wireLength_sourceRoute (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.wireLength (sourceRoute G d i) = Orthogonal.wireLength (d.2.getD i [])

Normalization preserves the total Manhattan wire cost.

theorem Cslib.Complexity.SAT.ExactOne.sourceRoute_endpoints {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) : List.head? (sourceRoute G d i) = some (sourceStart G d i) ∧ List.getLast? (sourceRoute G d i) = some (sourceFinish G d i)

The normalized route begins at the clause and ends at the variable.

theorem Cslib.Complexity.SAT.ExactOne.sourceStart_ne_finish {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) : sourceStart G d i ≠ sourceFinish G d i

The clause and variable endpoints occupy different points.

theorem Cslib.Complexity.SAT.ExactOne.sourceRoute_length_ge_two {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) : 2 ≤ List.length (sourceRoute G d i)

Every normalized valid incidence has at least two listed points.

theorem Cslib.Complexity.SAT.ExactOne.sourceRoute_regular {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) : Orthogonal.IsOrthogonal (sourceRoute G d i) ∧ Orthogonal.IsSimple (sourceRoute G d i)

Normalization preserves proper orthogonality and continuous simplicity.

theorem Cslib.Complexity.SAT.ExactOne.sourceRoute_shape {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) : ∃ (b : Orthogonal.Point) (r : List Orthogonal.Point), sourceRoute G d i = sourceStart G d i :: b :: r

A normalized incidence starts with its actual clause vertex and a proper next point.

def Cslib.Complexity.SAT.ExactOne.sourceDirection (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Point

The cardinal exit direction of a normalized source incidence.

theorem Cslib.Complexity.SAT.ExactOne.sourceDirection_ne {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) (hc : G.edges[i].2 = G.edges[j].2) : sourceDirection G d i ≠ sourceDirection G d j

Incidences at the same clause vertex leave in different cardinal directions.

def Cslib.Complexity.SAT.ExactOne.exteriorRoute (k radius : ℕ) (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Route

Scale and trim the clause end of a normalized source incidence.

def Cslib.Complexity.SAT.ExactOne.exteriorPort (k radius : ℕ) (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.Point

The designated contact with the boundary of the local clause box.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_regular {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) {k radius : ℕ} (hr : radius < k) : Orthogonal.IsOrthogonal (exteriorRoute k radius G d i) ∧ Orthogonal.IsSimple (exteriorRoute k radius G d i)

The trimmed exterior incidence is proper and continuously simple.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_endpoints {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) (k radius : ℕ) : List.head? (exteriorRoute k radius G d i) = some (exteriorPort k radius G d i) ∧ List.getLast? (exteriorRoute k radius G d i) = some (k • sourceFinish G d i)

The exterior incidence has its designated box port and the original scaled variable endpoint.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_wireLength {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) {k radius : ℕ} (hr : radius < k) : Orthogonal.wireLength (exteriorRoute k radius G d i) + radius = k * Orthogonal.wireLength (d.2.getD i [])

Cutting removes exactly the radius from the scaled Manhattan cost.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_segmentCount (k radius : ℕ) (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : (List.consecutivePairs (exteriorRoute k radius G d i)).length = (List.consecutivePairs (d.2.getD i [])).length

Exterior incidence routes keep the original number of listed segments.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_box_contact {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) {k radius : ℕ} (hr : radius < k) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (exteriorRoute k radius G d i)) (hb : Orthogonal.inPointBox (k • sourceStart G d i) radius p) : p = Orthogonal.realPoint (exteriorPort k radius G d i)

The exterior route meets its own closed clause box only at the designated port.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_avoids_box {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) {v : ℕ} (hv : v ∈ G.vertices) (hv₁ : v ≠ G.edges[i].1) (hv₂ : v ≠ G.edges[i].2) {k radius : ℕ} (hr : radius < k) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (exteriorRoute k radius G d i)) : ¬Orthogonal.inPointBox (k • G.drawingPosition d v) radius p

A nonincident declared vertex has a closed replacement box disjoint from an exterior route.

theorem Cslib.Complexity.SAT.ExactOne.sourceDirection_unit (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : Orthogonal.UnitVector (sourceDirection G d i)

The exit direction is one of the four cardinal unit vectors.

theorem Cslib.Complexity.SAT.ExactOne.exteriorPort_ne_center (k radius : ℕ) (hr : 0 < radius) (G : Graph) (d : Graph.OrthogonalDrawing) (i : ℕ) : exteriorPort k radius G d i ≠ k • sourceStart G d i

A positive-radius port is different from the removed source clause center.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_not_mem_center {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i : ℕ} (hi : i < G.edges.length) {k radius : ℕ} (hr₀ : 0 < radius) (hr : radius < k) : Orthogonal.realPoint (k • sourceStart G d i) ∉ Orthogonal.support (exteriorRoute k radius G d i)

A trimmed incidence no longer contains the scaled source clause vertex.

theorem Cslib.Complexity.SAT.ExactOne.exteriorRoute_contacts {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) {k radius : ℕ} (hr₀ : 0 < radius) (hr : radius < k) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (exteriorRoute k radius G d i)) (hq : p ∈ Orthogonal.support (exteriorRoute k radius G d j)) : G.edges[i].1 = G.edges[j].1 ∧ p = Orthogonal.realPoint (k • sourceFinish G d i)

Different exterior incidences can meet only at their shared scaled variable endpoint. The common source clause endpoint has been removed by the positive-radius cut.

theorem Cslib.Complexity.SAT.ExactOne.sourceVertex_not_mem_box {G : Graph} {d : Graph.OrthogonalDrawing} (hd : G.IsPlanarOrthogonalDrawing d) {v w : ℕ} (hv : v ∈ G.vertices) (hw : w ∈ G.vertices) (hvw : v ≠ w) {k radius : ℕ} (hr : radius < k) : ¬Orthogonal.inPointBox (k • G.drawingPosition d v) radius (Orthogonal.realPoint (k • G.drawingPosition d w))

A different source vertex center lies outside the closed local replacement box.