Laminar port ranks for numerical genus-zero loop graphs

Literal first-hit port ranks give disjoint or nested intervals for distinct indexed loops at a common vertex. The order is derived from numerical genus zero.

theorem Cslib.Complexity.Graph.RotationSystem.portRank_loops_laminar {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hr : r.NumericalGenusZero) (e f : Fin G.edges.length) (hef : e ≠ f) (he : Dart.vertex (e, false) = Dart.vertex (e, true)) (hf : Dart.vertex (f, false) = Dart.vertex (f, true)) (hv : Dart.vertex (e, false) = Dart.vertex (f, false)) : max (r.portRank (e, false)) (r.portRank (e, true)) < min (r.portRank (f, false)) (r.portRank (f, true)) ∨ max (r.portRank (f, false)) (r.portRank (f, true)) < min (r.portRank (e, false)) (r.portRank (e, true)) ∨ min (r.portRank (e, false)) (r.portRank (e, true)) < min (r.portRank (f, false)) (r.portRank (f, true)) ∧ max (r.portRank (f, false)) (r.portRank (f, true)) < max (r.portRank (e, false)) (r.portRank (e, true)) ∨ min (r.portRank (f, false)) (r.portRank (f, true)) < min (r.portRank (e, false)) (r.portRank (e, true)) ∧ max (r.portRank (e, false)) (r.portRank (e, true)) < max (r.portRank (f, false)) (r.portRank (f, true))

In numerical genus zero, the linear intervals of two distinct indexed loops at one vertex are disjoint or strictly nested. This derives the ordering from the numerical hypothesis; a noncrossing matching is not an input.