Unit neighbors at canonical endpoint ports

Main definitions

• Cslib.Orthogonal.Layout.portStep: the left, upward and right unit port directions.

Main results

• Cslib.Orthogonal.infix_head_pair_getD, .infix_last_pair_getD: indexed endpoint neighbors from a consecutive pair in a path without repetitions.
• Cslib.Orthogonal.Layout.fanWalk, .returnFanWalk: the exact two-step endpoint fans.

theorem Cslib.Orthogonal.infix_head_pair_getD {r : Route} (hn : List.Nodup r) {a b : Point} (hp : [a, b] <:+: r) (hh : List.head? r = some a) (d : Point) : 2 ≤ List.length r ∧ List.getD r 1 d = b

A consecutive pair starting at the unique first point determines index one.

theorem Cslib.Orthogonal.infix_last_pair_getD {r : Route} (hn : List.Nodup r) {a b : Point} (hp : [a, b] <:+: r) (hh : List.getLast? r = some b) (d : Point) : 2 ≤ List.length r ∧ List.getD r (List.length r - 2) d = a

A consecutive pair ending at the unique final point determines the penultimate index.

def Cslib.Orthogonal.Layout.portStep (s : Fin 3) : Point

The unit directions of the left, upward and right canonical endpoint ports.

theorem Cslib.Orthogonal.Layout.portStep_injective : Function.Injective portStep

Distinct ports have distinct unit directions.

theorem Cslib.Orthogonal.Layout.fanWalk (v : ℕ) (s : Fin 3) : segmentWalk (center v) (elbow v s) = [center v, center v + portStep s, elbow v s]

The local fan has exactly two unit steps in its port's direction.

theorem Cslib.Orthogonal.Layout.returnFanWalk (v : ℕ) (s : Fin 3) : segmentWalk (elbow v s) (center v) = [elbow v s, center v + portStep s, center v]

The return fan has the same middle unit point in the reverse order.