Finite orthogonal routes indexed by the existing graph edge list

No new graph representation is introduced. Positions follow G.vertices and routes follow G.edges, so every edge occurrence keeps its original index, including parallel edge occurrences. The input port table is a finite list assigning a pair of three-way ports to each edge occurrence.

Main definitions

• Cslib.Complexity.Graph.orthogonalPositions: finite list of diagonal vertex positions.
• Cslib.Complexity.Graph.orthogonalRoutes: finite list of routes in edge-list order.

Main results

• Cslib.Complexity.Graph.orthogonalRoutes_endpoints: each indexed route has the actual edge's endpoint positions.
• Cslib.Complexity.Graph.orthogonalRoutes_wireLength_le: explicit quadratic total wire bound.

def Cslib.Complexity.Graph.orthogonalPositions (G : Graph) : List Orthogonal.Point

Vertex positions indexed by the existing declared vertex list.

def Cslib.Complexity.Graph.orthogonalRoutes (G : Graph) (ports : List (Fin 3 × Fin 3)) : List Orthogonal.Route

The finite route list, in exactly the order of the graph's edge occurrences. A missing port-table entry defaults to the left port at both ends. Contact separation requires that the supplied table assigns distinct ports to different incidences.

@[simp]

theorem Cslib.Complexity.Graph.orthogonalPositions_length (G : Graph) : G.orthogonalPositions.length = G.vertices.length

The output lists have the original vertex and edge counts.

@[simp]

theorem Cslib.Complexity.Graph.orthogonalRoutes_length (G : Graph) (ports : List (Fin 3 × Fin 3)) : (G.orthogonalRoutes ports).length = G.edges.length

The output lists have the original vertex and edge counts.

theorem Cslib.Complexity.Graph.getElem_orthogonalRoutes (G : Graph) (ports : List (Fin 3 × Fin 3)) {i : ℕ} (hi : i < G.edges.length) : (G.orthogonalRoutes ports)[i] = Orthogonal.Layout.route G.vertices.length i (List.idxOf G.edges[i].1 G.vertices) (List.idxOf G.edges[i].2 G.vertices) (ports.getD i (0, 0)).1 (ports.getD i (0, 0)).2

The route at index i is the route for the edge at the same index.

theorem Cslib.Complexity.Graph.getElem_orthogonalRoutes_endpoint (G : Graph) (ports : List (Fin 3 × Fin 3)) {i : ℕ} (hi : i < G.edges.length) : (G.orthogonalRoutes ports)[i] = Orthogonal.Layout.route G.vertices.length i (List.idxOf (G.edgeEndpoint i false) G.vertices) (List.idxOf (G.edgeEndpoint i true) G.vertices) (portAt ports i false) (portAt ports i true)

A side-indexed version of the exact route formula.

theorem Cslib.Complexity.Graph.orthogonalRoutes_endpoints (G : Graph) (ports : List (Fin 3 × Fin 3)) {i : ℕ} (hi : i < G.edges.length) : have r := (G.orthogonalRoutes ports)[i]; List.head? r = some (Orthogonal.Layout.center (List.idxOf G.edges[i].1 G.vertices)) ∧ List.getLast? r = some (Orthogonal.Layout.center (List.idxOf G.edges[i].2 G.vertices))

Every route has the actual indexed graph edge's endpoints, regardless of the port table.

theorem Cslib.Complexity.Graph.orthogonalRoutes_orthogonal (G : Graph) (ports : List (Fin 3 × Fin 3)) {i : ℕ} (hi : i < G.edges.length) (hu : G.edges[i].1 ∈ G.vertices) (hv : G.edges[i].2 ∈ G.vertices) (hne : G.edges[i].1 ≠ G.edges[i].2) : Orthogonal.IsOrthogonal (G.orthogonalRoutes ports)[i]

Declared, distinct edge endpoints give a proper orthogonal route.

theorem Cslib.Complexity.Graph.orthogonalRoutes_simple (G : Graph) (ports : List (Fin 3 × Fin 3)) {i : ℕ} (hi : i < G.edges.length) (hu : G.edges[i].1 ∈ G.vertices) (hv : G.edges[i].2 ∈ G.vertices) (hne : G.edges[i].1 ≠ G.edges[i].2) : Orthogonal.IsSimple (G.orthogonalRoutes ports)[i]

Declared, distinct edge endpoints give a continuously simple route.

def Cslib.Complexity.Graph.crossingCandidates (G : Graph) (ports : List (Fin 3 × Fin 3)) : List Orthogonal.Point

At most 2m² candidate grid sites suffice for every bridge/stem crossing. Candidates may repeat or be unused; this explicit list is a cover, not a claim that every candidate is crossed.

@[simp]

theorem Cslib.Complexity.Graph.crossingCandidates_length (G : Graph) (ports : List (Fin 3 × Fin 3)) : (G.crossingCandidates ports).length = 2 * G.edges.length ^ 2

A quadratic bound on the explicit crossing-site cover, counting repeated candidates.

theorem Cslib.Complexity.Graph.mem_crossingCandidates (G : Graph) (ports : List (Fin 3 × Fin 3)) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (side : Bool) : (Orthogonal.Layout.column (List.idxOf (G.edgeEndpoint j side) G.vertices) (portAt ports j side), Orthogonal.Layout.track G.vertices.length i) ∈ G.crossingCandidates ports

Every indexed bridge/port intersection point occurs in the finite candidate cover.

theorem Cslib.Complexity.Graph.orthogonalRoutes_contact_cover (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (G.orthogonalRoutes G.canonicalPorts)[i]) (hq : p ∈ Orthogonal.support (G.orthogonalRoutes G.canonicalPorts)[j]) : (∃ w < G.vertices.length, p = Orthogonal.realPoint (Orthogonal.Layout.center w)) ∨ ∃ z ∈ G.crossingCandidates G.canonicalPorts, p = Orthogonal.realPoint z

Every contact in the canonical drawing lies at a vertex center or in an explicit list of 2m² candidate crossing sites. Strict transversality is supplied by Layout.route_contact; this finite cover additionally bounds the number of distinct crossing sites.

theorem Cslib.Complexity.Graph.orthogonalRoutes_segments (G : Graph) (ports : List (Fin 3 × Fin 3)) : (List.map (fun (r : Orthogonal.Route) => (List.consecutivePairs r).length) (G.orthogonalRoutes ports)).sum = 5 * G.edges.length

Exactly five segments are emitted for every edge occurrence.

theorem Cslib.Complexity.Graph.orthogonalRoutes_wireLength_le (G : Graph) (ports : List (Fin 3 × Fin 3)) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) : (List.map Orthogonal.wireLength (G.orthogonalRoutes ports)).sum ≤ 90 * (G.vertices.length + G.edges.length) ^ 2

The total wire length is at most 90 (n+m)², for n declared vertices and m edge occurrences. Endpoint membership is the only graph hypothesis needed for this resource bound.