Closed passages through a single indexed loop

ClosedPassages.loop is the single-loop constructor extracted from CslibFrontierTests.RotationIntersection, with its original proof and source credit. Numerical genus zero then excludes interlacing ends of any two distinct indexed loops, including in arbitrary-degree, disconnected graphs with sparse or repeated declarations. This is a combinatorial prerequisite for polygonal realization, not a geometric theorem.

Main results

• Cslib.Complexity.Graph.RotationSystem.not_alternates_loops: distinct loops do not interlace in a numerically genus-zero rotation with declared endpoints.

def Cslib.Complexity.Graph.ClosedPassages.loop {G : Graph} (e : Fin G.edges.length) (he : Dart.vertex (e, false) = Dart.vertex (e, true)) : G.ClosedPassages fun (i : Fin G.edges.length) => decide (i = e)

One passage using the two actual ends of a single listed loop.

@[simp]

theorem Cslib.Complexity.Graph.ClosedPassages.dart_loop {G : Graph} (e : Fin G.edges.length) (he : Dart.vertex (e, false) = Dart.vertex (e, true)) (i : Fin (loop e he).count) (b : Bool) : (loop e he).dart i b = (e, b)

The single-loop passage keeps the original edge occurrence and both endpoint tags.

theorem Cslib.Complexity.Graph.RotationSystem.not_alternates_loops {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)) : ¬r.Alternates (e, false) (e, true) (f, false) (f, true)

Two distinct listed loops cannot have alternating ends in a numerically genus-zero rotation. No connectedness, degree bound, drawing or Jordan-curve premise is used.