Canonical unit paths and their local occupancy

The finite path list uses the canonical incidence ports and the explicit linear per-route wire budget. Correctness statements refer to the existing graph's edge occurrences by their indices.

Main definitions

• Cslib.Complexity.Graph.unitPaths: canonical finite unit paths in edge-list order.
• Cslib.Complexity.Graph.unitPath: indexed access, with the empty path outside the edge range.

Main results

• Cslib.Complexity.Graph.unitPath_endpoints, .unitPath_nodup, .unitPath_unit: endpoint, uniqueness and unit-adjacency certificates.
• Cslib.Complexity.Graph.unitPath_first_neighbor, .unitPath_last_neighbor: exact canonical port neighbors at both ends, with .endpointNeighbor_ne for different incident edges.
• Cslib.Complexity.Graph.unitPath_support, .unitPath_bounds: continuous support and grid bounds.
• Cslib.Complexity.Graph.unitPath_declared_center_iff: no nonincident source-center contacts.
• Cslib.Complexity.Graph.unitPath_contact, .unitPath_atMostTwo: actual crossing classification and at most two paths at nonvertex points.
• Cslib.Complexity.Graph.unitPath_crossing_neighbors: opposite horizontal/vertical unit neighbors.
• Cslib.Complexity.Graph.BridgeStemCrossing.not_listed: crossings avoid all original bends.
• Cslib.Complexity.Graph.unitPath_neighbor_lengths, .unitPath_neighbors_distinct: the two distinct unit neighbors at every ordinary nonvertex occupied cell.

def Cslib.Complexity.Graph.unitPaths (G : Graph) : List Orthogonal.Route

Canonical unit paths, with the checked linear per-edge wire budget.

def Cslib.Complexity.Graph.unitPath (G : Graph) (i : ℕ) : Orthogonal.Route

Access one finite canonical unit path, defaulting to the empty path outside the edge range.

@[simp]

theorem Cslib.Complexity.Graph.unitPaths_length (G : Graph) : G.unitPaths.length = G.edges.length

One unit path is emitted for every listed edge occurrence.

theorem Cslib.Complexity.Graph.unitPath_eq_subdivide (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) : G.unitPath i = Orthogonal.subdivide (G.orthogonalRoutes G.canonicalPorts)[i]

The budgeted compiler produces the full subdivision at every existing edge.

theorem Cslib.Complexity.Graph.unitPath_endpoints (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) : List.head? (G.unitPath i) = some (Orthogonal.Layout.center (List.idxOf (G.edgeEndpoint i false) G.vertices)) ∧ List.getLast? (G.unitPath i) = some (Orthogonal.Layout.center (List.idxOf (G.edgeEndpoint i true) G.vertices))

Canonical unit paths preserve both original indexed edge endpoints.

theorem Cslib.Complexity.Graph.unitPath_nodup (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) : List.Nodup (G.unitPath i)

Canonical unit paths never repeat a listed lattice point.

theorem Cslib.Complexity.Graph.unitPath_first_neighbor (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) (d : Orthogonal.Point) : List.getD (G.unitPath i) 1 d = Orthogonal.Layout.center (List.idxOf (G.edgeEndpoint i false) G.vertices) + Orthogonal.Layout.portStep (portAt G.canonicalPorts i false)

The first unit neighbor is the source center plus its actual canonical port direction.

theorem Cslib.Complexity.Graph.unitPath_last_neighbor (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) (d : Orthogonal.Point) : List.getD (G.unitPath i) (List.length (G.unitPath i) - 2) d = Orthogonal.Layout.center (List.idxOf (G.edgeEndpoint i true) G.vertices) + Orthogonal.Layout.portStep (portAt G.canonicalPorts i true)

The penultimate unit point is the target center plus its canonical port direction.

def Cslib.Complexity.Graph.endpointNeighbor (G : Graph) (i : ℕ) (side : Bool) : Orthogonal.Point

The immediate unit neighbor at a chosen end of an indexed canonical path.

theorem Cslib.Complexity.Graph.endpointNeighbor_eq (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) (side : Bool) : G.endpointNeighbor i side = Orthogonal.Layout.center (List.idxOf (G.edgeEndpoint i side) G.vertices) + Orthogonal.Layout.portStep (portAt G.canonicalPorts i side)

Side-indexed exact endpoint-neighbor formula.

theorem Cslib.Complexity.Graph.endpointNeighbor_ne (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) (left right : Bool) (hc : List.idxOf (G.edgeEndpoint i left) G.vertices = List.idxOf (G.edgeEndpoint j right) G.vertices) : G.endpointNeighbor i left ≠ G.endpointNeighbor j right

Different edge occurrences at the same source center use different unit neighbors.

theorem Cslib.Complexity.Graph.unitPath_unit (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) {e : Orthogonal.Point × Orthogonal.Point} (he : e ∈ List.consecutivePairs (G.unitPath i)) : Orthogonal.length e.1 e.2 = 1

Every consecutive pair in a canonical unit path is exactly one Manhattan unit apart.

theorem Cslib.Complexity.Graph.unitPath_support (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) : Orthogonal.support (G.unitPath i) = Orthogonal.support (G.orthogonalRoutes G.canonicalPorts)[i]

Unit paths retain the whole continuous real support of their original polygonal routes.

theorem Cslib.Complexity.Graph.mem_unitPath_iff_support (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) (p : Orthogonal.Point) : p ∈ G.unitPath i ↔ Orthogonal.realPoint p ∈ Orthogonal.support (G.orthogonalRoutes G.canonicalPorts)[i]

An integer point lies on a unit path exactly when it lies on the original real route.

theorem Cslib.Complexity.Graph.unitPath_bounds (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) {p : Orthogonal.Point} (hp : p ∈ G.unitPath i) : 0 ≤ p.1 ∧ p.1 ≤ 8 * ↑G.vertices.length ∧ 0 ≤ p.2 ∧ p.2 ≤ 8 * ↑G.vertices.length + 2 * ↑G.edges.length

Every listed unit point lies in the original explicit linear rectangle.

theorem Cslib.Complexity.Graph.unitPath_ne_nil (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) : G.unitPath i ≠ []

Every canonical edge path is nonempty.

theorem Cslib.Complexity.Graph.unitPath_center_iff (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i w : ℕ} (hi : i < G.edges.length) (hw : w < G.vertices.length) : Orthogonal.Layout.center w ∈ G.unitPath i ↔ w = List.idxOf G.edges[i].1 G.vertices ∨ w = List.idxOf G.edges[i].2 G.vertices

A source grid center lies on a canonical unit path exactly when its position index is one of that graph edge's two endpoint indices.

theorem Cslib.Complexity.Graph.unitPath_declared_center_iff (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i v : ℕ} (hi : i < G.edges.length) (hv : v ∈ G.vertices) : Orthogonal.Layout.center (List.idxOf v G.vertices) ∈ G.unitPath i ↔ v = G.edges[i].1 ∨ v = G.edges[i].2

No source vertex center lies on a nonincident path, stated using the graph's actual labels.

theorem Cslib.Complexity.Graph.unitPath_not_endpoints (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i : ℕ} (hi : i < G.edges.length) {p : Orthogonal.Point} (hcenter : p ∉ G.orthogonalPositions) : List.head? (G.unitPath i) ≠ some p ∧ List.getLast? (G.unitPath i) ≠ some p

Nonvertex occupied cells are neither end of a canonical path.

theorem Cslib.Complexity.Graph.unitPath_interior_index (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i k : ℕ} (hi : i < G.edges.length) (hk : k < List.length (G.unitPath i)) {p : Orthogonal.Point} (heq : (G.unitPath i)[k] = p) (hcenter : p ∉ G.orthogonalPositions) : 0 < k ∧ k + 1 < List.length (G.unitPath i)

An occupied point away from source centers has a genuine predecessor and successor at every occurrence index. Together with unitPath_nodup, that occurrence index is unique.

theorem Cslib.Complexity.Graph.unitPath_neighbor_lengths (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i k : ℕ} (hi : i < G.edges.length) (hk : k < List.length (G.unitPath i)) {p : Orthogonal.Point} (heq : (G.unitPath i)[k] = p) (hcenter : p ∉ G.orthogonalPositions) : Orthogonal.length (List.getD (G.unitPath i) (k - 1) p) p = 1 ∧ Orthogonal.length p (List.getD (G.unitPath i) (k + 1) p) = 1

The two actual predecessor/successor lookups at a nonvertex cell are unit neighbors.

theorem Cslib.Complexity.Graph.unitPath_neighbors_distinct (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i k : ℕ} (hi : i < G.edges.length) (hk : k < List.length (G.unitPath i)) {p : Orthogonal.Point} (heq : (G.unitPath i)[k] = p) (hcenter : p ∉ G.orthogonalPositions) : List.getD (G.unitPath i) (k - 1) p ≠ List.getD (G.unitPath i) (k + 1) p

A nonvertex cell's predecessor and successor are distinct, so its two ports differ.

def Cslib.Complexity.Graph.pathColumn (G : Graph) (i : ℕ) (side : Bool) : ℤ

The vertical column assigned to one canonical graph incidence.

def Cslib.Complexity.Graph.BridgeStemCrossing (G : Graph) (i j : ℕ) (side : Bool) (p : Orthogonal.Point) : Prop

A genuine strict transverse crossing of edge i's bridge with one stem of edge j. The geometry is the canonical construction, not an assumed drawing witness.

theorem Cslib.Complexity.Graph.BridgeStemCrossing.point {G : Graph} {i j : ℕ} {side : Bool} {p : Orthogonal.Point} (hc : G.BridgeStemCrossing i j side p) : p = (G.pathColumn j side, Orthogonal.Layout.track G.vertices.length i)

A canonical crossing lies at its exact integer stem column and bridge row.

theorem Cslib.Complexity.Graph.BridgeStemCrossing.horizontal {G : Graph} {i j : ℕ} {side : Bool} {p : Orthogonal.Point} (hc : G.BridgeStemCrossing i j side p) : min (G.pathColumn i false) (G.pathColumn i true) < p.1 ∧ p.1 < max (G.pathColumn i false) (G.pathColumn i true)

The crossing lies strictly between the bridge's two port columns.

theorem Cslib.Complexity.Graph.BridgeStemCrossing.vertical {G : Graph} (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) {i j : ℕ} (hj : j < G.edges.length) {side : Bool} {p : Orthogonal.Point} (hc : G.BridgeStemCrossing i j side p) : (Orthogonal.Layout.elbow (List.idxOf (G.edgeEndpoint j side) G.vertices) (portAt G.canonicalPorts j side)).2 < p.2 ∧ p.2 < Orthogonal.Layout.track G.vertices.length j

The crossing lies strictly above the stem's elbow and below its top endpoint.

theorem Cslib.Complexity.Graph.unitPath_contact (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) {p : Orthogonal.Point} (hp : p ∈ G.unitPath i) (hq : p ∈ G.unitPath j) : p ∈ G.orthogonalPositions ∨ (∃ (side : Bool), G.BridgeStemCrossing i j side p) ∨ ∃ (side : Bool), G.BridgeStemCrossing j i side p

Actual contact of two distinct canonical unit paths is a vertex center or a strict bridge/stem crossing, in one of the two orientations.

theorem Cslib.Complexity.Graph.unitPath_on_column_track (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j k : ℕ} (hj : j < G.edges.length) (hk : k < G.edges.length) (side : Bool) : (G.pathColumn j side, Orthogonal.Layout.track G.vertices.length i) ∈ G.unitPath k → k = i ∨ k = j

Unique canonical tracks and incidence columns admit at most the named two paths through their intersection, independently of whether that intersection is actually occupied.

theorem Cslib.Complexity.Graph.unitPath_atMostTwo (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j k : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hk : k < G.edges.length) (hij : i ≠ j) {p : Orthogonal.Point} (hcenter : p ∉ G.orthogonalPositions) (hp : p ∈ G.unitPath i) (hq : p ∈ G.unitPath j) (hr : p ∈ G.unitPath k) : k = i ∨ k = j

Outside declared vertex centers, any two distinct occupied paths exclude every third path.

theorem Cslib.Complexity.Graph.unitPath_shared_mem_crossingCandidates (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) {p : Orthogonal.Point} (hcenter : p ∉ G.orthogonalPositions) (hp : p ∈ G.unitPath i) (hq : p ∈ G.unitPath j) : p ∈ G.crossingCandidates G.canonicalPorts

Every nonvertex shared point belongs to the original finite quadratic candidate cover.

theorem Cslib.Complexity.Graph.BridgeStemCrossing.not_vertex_center {G : Graph} {i j : ℕ} {side : Bool} {p : Orthogonal.Point} (hc : G.BridgeStemCrossing i j side p) : p ∉ G.orthogonalPositions

Every strict canonical crossing avoids every original source vertex center.

theorem Cslib.Complexity.Graph.BridgeStemCrossing.not_listed {G : Graph} (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) {side : Bool} {p : Orthogonal.Point} (hc : G.BridgeStemCrossing i j side p) : p ∉ (G.orthogonalRoutes G.canonicalPorts)[i] ∧ p ∉ (G.orthogonalRoutes G.canonicalPorts)[j]

A crossing is not any listed point of either original polygonal route, including its elbows and upper endpoints. Thus no crossing occurs at a bend.

theorem Cslib.Complexity.Graph.BridgeStemCrossing.neighbors {G : Graph} (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) {side : Bool} {p : Orthogonal.Point} (hc : G.BridgeStemCrossing i j side p) : Orthogonal.StraightThrough (G.unitPath i) p (1, 0) ∧ Orthogonal.StraightThrough (G.unitPath j) p (0, 1)

A strict crossing produces actual consecutive opposite horizontal/vertical unit neighbors on its two paths. Both the positions and their traversal order come from the canonical data.

theorem Cslib.Complexity.Graph.unitPath_crossing_neighbors (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hloop : ∀ edge ∈ G.edges, edge.1 ≠ edge.2) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) {p : Orthogonal.Point} (hcenter : p ∉ G.orthogonalPositions) (hp : p ∈ G.unitPath i) (hq : p ∈ G.unitPath j) : Orthogonal.StraightThrough (G.unitPath i) p (1, 0) ∧ Orthogonal.StraightThrough (G.unitPath j) p (0, 1) ∨ Orthogonal.StraightThrough (G.unitPath i) p (0, 1) ∧ Orthogonal.StraightThrough (G.unitPath j) p (1, 0)

Every actual nonvertex contact has one horizontally straight path and one vertically straight path, with opposite immediate unit neighbors.