Diagonal boxes and upper tracks for finite orthogonal layouts

Vertex v is centered at (8v+4,8v+4). Its three ports leave to the left, up, and right, and then rise on columns 8v+2, 8v+4, and 8v+6. Edge e travels horizontally on row 8n+2e+2, above all n vertex boxes. All data are explicit finite lists.

Main definitions

• Cslib.Orthogonal.Layout.center, Cslib.Orthogonal.Layout.column: vertex centers and ports.
• Cslib.Orthogonal.Layout.route: six listed points defining a five-segment route.

Main results

• Cslib.Orthogonal.Layout.route_orthogonal: the routes are proper and orthogonal.
• Cslib.Orthogonal.Layout.route_bounds: explicit linear grid sides.
• Cslib.Orthogonal.Layout.route_simple: continuous simplicity.
• Cslib.Orthogonal.Layout.route_contact: shared endpoint or strict transverse crossing.
• Cslib.Orthogonal.Layout.center_mem_support_iff: no incidental vertex contacts.

References

The box/track construction and its proofs are original.

def Cslib.Orthogonal.Layout.center (v : ℕ) : Point

Vertex center inside its diagonal box of side eight.

def Cslib.Orthogonal.Layout.column (v : ℕ) (s : Fin 3) : ℤ

The three distinct upward port columns, ordered left to right.

def Cslib.Orthogonal.Layout.elbow (v : ℕ) (s : Fin 3) : Point

A two-unit initial step to the left, up, or right.

def Cslib.Orthogonal.Layout.track (n e : ℕ) : ℤ

A private upper horizontal row for the indexed edge.

def Cslib.Orthogonal.Layout.route (n e u v : ℕ) (s t : Fin 3) : Route

A route from port s at vertex u to port t at vertex v, on edge track e. The middle port has two consecutive collinear vertical segments.

def Cslib.Orthogonal.Layout.fan (v : ℕ) (s : Fin 3) : Set (ℝ × ℝ)

The local initial segment inside one vertex box.

def Cslib.Orthogonal.Layout.stem (n e v : ℕ) (s : Fin 3) : Set (ℝ × ℝ)

The upward part of a port, from its local elbow to the private edge track.

def Cslib.Orthogonal.Layout.bridge (n e u v : ℕ) (s t : Fin 3) : Set (ℝ × ℝ)

The upper horizontal part of an edge.

theorem Cslib.Orthogonal.Layout.support_route (n e u v : ℕ) (s t : Fin 3) : support (route n e u v s t) = fan u s ∪ stem n e u s ∪ bridge n e u v s t ∪ stem n e v t ∪ fan v t

Decompose the continuous route into its two local fans, two stems, and upper bridge.

theorem Cslib.Orthogonal.Layout.column_injective {u v : ℕ} {s t : Fin 3} (h : column u s = column v t) : u = v ∧ s = t

Port columns uniquely identify both the vertex and the port.

theorem Cslib.Orthogonal.Layout.fan_bounds {v : ℕ} {s : Fin 3} {p : ℝ × ℝ} (hp : p ∈ fan v s) : 8 * ↑v + 2 ≤ p.1 ∧ p.1 ≤ 8 * ↑v + 6 ∧ 8 * ↑v + 4 ≤ p.2 ∧ p.2 ≤ 8 * ↑v + 6

All points of the local fan stay in its vertex's small diagonal box.

theorem Cslib.Orthogonal.Layout.fan_disjoint {u v : ℕ} (huv : u ≠ v) (s t : Fin 3) : Disjoint (fan u s) (fan v t)

Distinct vertex boxes have disjoint local fans.

theorem Cslib.Orthogonal.Layout.mem_stem {n e v : ℕ} {s : Fin 3} {p : ℝ × ℝ} : p ∈ stem n e v s ↔ p.1 = ↑(column v s) ∧ p.2 ∈ Set.uIcc ↑(elbow v s).2 ↑(track n e)

Membership in a stem fixes its column and its closed vertical interval.

theorem Cslib.Orthogonal.Layout.mem_bridge {n e u v : ℕ} {s t : Fin 3} {p : ℝ × ℝ} : p ∈ bridge n e u v s t ↔ p.2 = ↑(track n e) ∧ p.1 ∈ Set.uIcc ↑(column u s) ↑(column v t)

Membership in a bridge fixes its row and its closed horizontal interval.

theorem Cslib.Orthogonal.Layout.mem_fan {v : ℕ} {s : Fin 3} {p : ℝ × ℝ} : p ∈ fan v s ↔ s = 0 ∧ p.2 = 8 * ↑v + 4 ∧ 8 * ↑v + 2 ≤ p.1 ∧ p.1 ≤ 8 * ↑v + 4 ∨ s = 1 ∧ p.1 = 8 * ↑v + 4 ∧ 8 * ↑v + 4 ≤ p.2 ∧ p.2 ≤ 8 * ↑v + 6 ∨ s = 2 ∧ p.2 = 8 * ↑v + 4 ∧ 8 * ↑v + 4 ≤ p.1 ∧ p.1 ≤ 8 * ↑v + 6

The three local fans, in left/up/right order, have these explicit real supports.

theorem Cslib.Orthogonal.Layout.elbow_below_track {n e v : ℕ} (hv : v < n) (s : Fin 3) : (elbow v s).2 < track n e

Every edge row lies strictly above every vertex box.

theorem Cslib.Orthogonal.Layout.center_elbow_axisAligned (v : ℕ) (s : Fin 3) : AxisAligned (center v) (elbow v s)

The fixed initial segment is proper and orthogonal.

theorem Cslib.Orthogonal.Layout.route_segments_length (n e u v : ℕ) (s t : Fin 3) : (List.consecutivePairs (route n e u v s t)).length = 5

The complete route has exactly five segments.

@[simp]

theorem Cslib.Orthogonal.Layout.route_head (n e u v : ℕ) (s t : Fin 3) : List.head? (route n e u v s t) = some (center u)

The route starts and ends at the specified centers.

@[simp]

theorem Cslib.Orthogonal.Layout.route_last (n e u v : ℕ) (s t : Fin 3) : List.getLast? (route n e u v s t) = some (center v)

The route starts and ends at the specified centers.

theorem Cslib.Orthogonal.Layout.route_orthogonal {n e u v : ℕ} (hu : u < n) (hv : v < n) (huv : u ≠ v) (s t : Fin 3) : IsOrthogonal (route n e u v s t)

Proper orthogonality uses only distinct vertices and the vertex range bounds.

theorem Cslib.Orthogonal.Layout.route_bounds {n m e u v : ℕ} (he : e < m) (hu : u < n) (hv : v < n) (s t : Fin 3) {p : Point} (hp : p ∈ route n e u v s t) : 0 ≤ p.1 ∧ p.1 ≤ 8 * ↑n ∧ 0 ≤ p.2 ∧ p.2 ≤ 8 * ↑n + 2 * ↑m

All six listed points lie in a rectangle with width 8n and height 8n+2m. The convention permits an empty graph and uses only edges e < m.

theorem Cslib.Orthogonal.Layout.route_wireLength_le {n m e u v : ℕ} (he : e < m) (hu : u < n) (hv : v < n) (s t : Fin 3) : wireLength (route n e u v s t) ≤ 80 * n + 10 * m

One edge has wire length at most 80n+10m, with no assumption on degree.

theorem Cslib.Orthogonal.Layout.center_mem_support_iff {n e u v w : ℕ} (hu : u < n) (hv : v < n) (hw : w < n) (huv : u ≠ v) (s t : Fin 3) : realPoint (center w) ∈ support (route n e u v s t) ↔ w = u ∨ w = v

A route visits no vertex center except its two prescribed endpoints. This concerns the whole real segment support, not only its six listed points.

theorem Cslib.Orthogonal.Layout.fan_contact {v : ℕ} {s t : Fin 3} (hst : s ≠ t) {p : ℝ × ℝ} (hs : p ∈ fan v s) (ht : p ∈ fan v t) : p = realPoint (center v)

Two different ports in a single vertex box meet only at the vertex center.

theorem Cslib.Orthogonal.Layout.fan_stem_port_eq {n e u v : ℕ} (hv : v < n) {s t : Fin 3} {p : ℝ × ℝ} (hp : p ∈ fan u s) (hq : p ∈ stem n e v t) : u = v ∧ s = t

A fan can contact a stem only when both belong to the same port.

theorem Cslib.Orthogonal.Layout.stem_disjoint {n e f u v : ℕ} {s t : Fin 3} (h : (u, s) ≠ (v, t)) : Disjoint (stem n e u s) (stem n f v t)

Different port columns give disjoint stems, independently of their edge heights.

theorem Cslib.Orthogonal.Layout.fan_bridge_disjoint {n e u v w : ℕ} (hw : w < n) (s t q : Fin 3) : Disjoint (fan w q) (bridge n e u v s t)

A local fan lies strictly below every upper bridge.

theorem Cslib.Orthogonal.Layout.bridge_disjoint {n e f u v a b : ℕ} (hef : e ≠ f) (s t q r : Fin 3) : Disjoint (bridge n e u v s t) (bridge n f a b q r)

Distinct edge tracks give disjoint upper bridges.

theorem Cslib.Orthogonal.Layout.fan_stem_disjoint {n e u v : ℕ} (hv : v < n) {s t : Fin 3} (h : (u, s) ≠ (v, t)) : Disjoint (fan u s) (stem n e v t)

Fans and stems at distinct ports are disjoint, even within one vertex box.

theorem Cslib.Orthogonal.Layout.fan_stem_endpointContacts {n e v : ℕ} (hv : v < n) (s : Fin 3) : EndpointContacts (center v) (elbow v s) (elbow v s) (column v s, track n e)

The two consecutive parts of one port meet only at their common elbow.

theorem Cslib.Orthogonal.Layout.stem_bridge_endpointContacts (n e u v : ℕ) (s t : Fin 3) : EndpointContacts (elbow u s) (column u s, track n e) (column u s, track n e) (column v t, track n e)

A stem meets its own bridge only at their common upper endpoint.

theorem Cslib.Orthogonal.Layout.route_nodup {n e u v : ℕ} (hu : u < n) (hv : v < n) (huv : u ≠ v) (s t : Fin 3) : List.Nodup (route n e u v s t)

The six listed points are distinct for an edge with distinct endpoints.

theorem Cslib.Orthogonal.Layout.route_simple {n e u v : ℕ} (hu : u < n) (hv : v < n) (huv : u ≠ v) (s t : Fin 3) : IsSimple (route n e u v s t)

The whole real polygonal route is simple: distinct consecutive segments contact only at their common listed endpoints, and no listed point is repeated.

theorem Cslib.Orthogonal.Layout.bridge_stem_transverse {n e f u v w : ℕ} (hw : w < n) (hef : e ≠ f) {s t q : Fin 3} (hu : (w, q) ≠ (u, s)) (hv : (w, q) ≠ (v, t)) {p : ℝ × ℝ} (hp : p ∈ bridge n e u v s t) (hq : p ∈ stem n f w q) : Transverse (column u s, track n e) (column v t, track n e) (elbow w q) (column w q, track n f) p

Every contact of an upper bridge with another edge's distinct port stem is a genuine transverse crossing, strictly inside both segments. In particular it is never at a bend.

theorem Cslib.Orthogonal.Layout.bridge_stem_crossing_point {n e f u v w : ℕ} {s t q : Fin 3} {p : ℝ × ℝ} (h : Transverse (column u s, track n e) (column v t, track n e) (elbow w q) (column w q, track n f) p) : p = realPoint (column w q, track n e)

A bridge/stem transverse crossing has its exact integer column/row coordinates.

theorem Cslib.Orthogonal.Layout.fan_pair_contact {u v : ℕ} {s t : Fin 3} (h : (u, s) ≠ (v, t)) {p : ℝ × ℝ} (hp : p ∈ fan u s) (hq : p ∈ fan v t) : u = v ∧ p = realPoint (center u)

Distinct ports' fans can contact only at their common graph endpoint.

theorem Cslib.Orthogonal.Layout.route_contact {n e f u v a b : ℕ} (hu : u < n) (hv : v < n) (ha : a < n) (hb : b < n) (hef : e ≠ f) {s t q r : Fin 3} (huaq : (u, s) ≠ (a, q)) (hubr : (u, s) ≠ (b, r)) (hvaq : (v, t) ≠ (a, q)) (hvbr : (v, t) ≠ (b, r)) {p : ℝ × ℝ} (hp : p ∈ support (route n e u v s t)) (hq : p ∈ support (route n f a b q r)) : (∃ (w : ℕ), (w = u ∨ w = v) ∧ (w = a ∨ w = b) ∧ p = realPoint (center w)) ∨ Transverse (column u s, track n e) (column v t, track n e) (elbow a q) (column a q, track n f) p ∨ Transverse (column u s, track n e) (column v t, track n e) (elbow b r) (column b r, track n f) p ∨ Transverse (column a q, track n f) (column b r, track n f) (elbow u s) (column u s, track n e) p ∨ Transverse (column a q, track n f) (column b r, track n f) (elbow v t) (column v t, track n e) p

Any pairwise route contact is either a shared graph endpoint or a strict transverse bridge/stem crossing. The four port inequalities require different edge incidences to use different ports, including at a shared vertex. All statements concern continuous real supports.