Intersection parity of finite closed passage systems

A closed passage system pairs the actual darts of a supported indexed edge set, using each exactly once and pairing only darts at the same vertex. This retains multiple visits, high-degree vertices, arbitrary local pairings and self-intersections. It adds no graph, topological universe or intersection-parity premise.

Intervals follow the literal cyclic successor rotate, stopping at its first visit to the second end. Two passages alternate when exactly one end is in this interval and their four darts are distinct. The finite face-color proof is an original reconstruction: boundaries telescope along a rotation interval, and the resulting endpoint contributions cancel along the second closed passage system.

The final result concerns the existing componentwise numerical genus model. It proves no drawing realization, drawing operation, weak or unified Hanani–Tutte theorem, recognition criterion, or Boolean CSP dichotomy.

Main definitions

• Cslib.Complexity.Graph.ClosedPassages: exactly-once finite dart pairing.
• Cslib.Complexity.Graph.RotationSystem.Alternates: literal cyclic port alternation.
• Cslib.Complexity.Graph.RotationSystem.intersectionParity: sum of passage-pair crossing bits.

Main results

• Cslib.Complexity.Graph.RotationSystem.sum_alternates_eq_faceColors: local telescoping.
• Cslib.Complexity.Graph.RotationSystem.intersectionParity_eq_false: closed-system parity.

structure Cslib.Complexity.Graph.ClosedPassages (G : Graph) (x : Fin G.edges.length → Bool) : Type

A finite pairing of all actual darts of a Boolean edge support. This is the local passage data of closed edge-disjoint routes; it need not consist of one connected route.

• count : ℕ

  Number of indexed passages, including separate visits to the same vertex.

• ports : Fin self.count × Bool ≃ { d : G.Dart // x d.1 = true }

  Exactly-once enumeration of both ends of every supported edge. The two ports of a passage are distinct because this map is an equivalence.

• vertex_eq (i : Fin self.count) : (↑(self.ports (i, false))).vertex = (↑(self.ports (i, true))).vertex

  Both ports of each passage are incident at the same original vertex.

def Cslib.Complexity.Graph.ClosedPassages.dart {G : Graph} {x : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (i : Fin P.count) (b : Bool) : G.Dart

The actual indexed dart at one port of a passage.

theorem Cslib.Complexity.Graph.ClosedPassages.supported {G : Graph} {x : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (i : Fin P.count) (b : Bool) : x (P.dart i b).1 = true

Every passage port belongs to the declared edge support.

theorem Cslib.Complexity.Graph.ClosedPassages.dart_ne {G : Graph} {x : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (i : Fin P.count) : P.dart i false ≠ P.dart i true

The two ends of one passage are distinct, including passages through loop ends.

theorem Cslib.Complexity.Graph.ClosedPassages.sum_ports {G : Graph} {x : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (f : G.Dart → Bool) : ∑ i : Fin P.count, (f (P.dart i false) + f (P.dart i true)) = ∑ d : G.Dart, if x d.1 = true then f d else 0

A dart sum over the support can be read as the sum over all indexed passage ports.

theorem Cslib.Complexity.Graph.ClosedPassages.vertexEven {G : Graph} {x : Fin G.edges.length → Bool} (P : G.ClosedPassages x) : G.VertexEven x

Exactly-once closed passage data have even parity at every original vertex.

noncomputable def Cslib.Complexity.Graph.RotationSystem.rotationDistance {G : Graph} (r : G.RotationSystem) (a b : G.Dart) : ℕ

Number of literal forward rotations to the first visit to b from a. It is zero when the endpoints are at different vertices, or when they coincide.

theorem Cslib.Complexity.Graph.RotationSystem.pow_rotationDistance {G : Graph} (r : G.RotationSystem) (a b : G.Dart) (h : a.vertex = b.vertex) : (r.rotate ^ r.rotationDistance a b) a = b

Forward rotation reaches the terminal dart at the recorded distance.

theorem Cslib.Complexity.Graph.RotationSystem.pow_ne_of_lt_rotationDistance {G : Graph} (r : G.RotationSystem) (a b : G.Dart) (h : a.vertex = b.vertex) {k : ℕ} (hk : k < r.rotationDistance a b) : (r.rotate ^ k) a ≠ b

No earlier iterate reaches the terminal dart.

theorem Cslib.Complexity.Graph.RotationSystem.rotationDistance_eq {G : Graph} (r : G.RotationSystem) (a b : G.Dart) (h : a.vertex = b.vertex) (n : ℕ) (hn : (r.rotate ^ n) a = b) (hmin : ∀ k < n, (r.rotate ^ k) a ≠ b) : r.rotationDistance a b = n

A checked first-hit calculation determines the literal forward distance. This permits finite clients to compute intervals without evaluating classical orbit decisions.

noncomputable def Cslib.Complexity.Graph.RotationSystem.rotationInterval {G : Graph} (r : G.RotationSystem) (a b : G.Dart) : Finset G.Dart

The literal directed cyclic interval (a,b]: rotate forward from a to the first b, excluding a and including b. For alternating passages all four darts are distinct, so including the terminal dart makes no difference. Different endpoint vertices give ∅.

theorem Cslib.Complexity.Graph.RotationSystem.vertex_of_mem_rotationInterval {G : Graph} (r : G.RotationSystem) (a b d : G.Dart) (hd : d ∈ r.rotationInterval a b) : d.vertex = a.vertex

Every dart of the rotation interval is at its starting vertex.

theorem Cslib.Complexity.Graph.RotationSystem.sum_rotationInterval {G : Graph} (r : G.RotationSystem) (a b : G.Dart) (h : a.vertex = b.vertex) (q : G.Dart → Bool) : ∑ d ∈ r.rotationInterval a b, (q d + q ((Equiv.symm r.rotate) d)) = q b + q a

Interval sums telescope along the actual rotation, without any topological assumption.

theorem Cslib.Complexity.Graph.RotationSystem.faceBoundary_rotate {G : Graph} (r : G.RotationSystem) (q : r.Face → Bool) (d : G.Dart) : r.faceBoundary q d.1 = q ⟦d⟧ + q ⟦(Equiv.symm r.rotate) d⟧

Adjacent face colors around a vertex differ by the boundary label on its intervening actual dart. This is the precise orientation identity for faceNext = rotate.symm ∘ reverse.

theorem Cslib.Complexity.Graph.RotationSystem.sum_faceBoundary_rotationInterval {G : Graph} (r : G.RotationSystem) (q : r.Face → Bool) (a b : G.Dart) (h : a.vertex = b.vertex) : ∑ d ∈ r.rotationInterval a b, r.faceBoundary q d.1 = q ⟦b⟧ + q ⟦a⟧

Boundary labels along a rotation interval telescope to its two incident face colors.

noncomputable def Cslib.Complexity.Graph.RotationSystem.Alternates {G : Graph} (r : G.RotationSystem) (a b c d : G.Dart) : Prop

Two directed passages alternate in the literal rotation when their four actual darts are distinct, they share a vertex, and exactly one end of the first is in the directed interval between the second's ends. No reflection quotient is taken.

theorem Cslib.Complexity.Graph.RotationSystem.alternates_eq_interval {G : Graph} (r : G.RotationSystem) (a b c d : G.Dart) (hab : a ≠ b) (hcd : c ≠ d) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hv : a.vertex = b.vertex) (hw : c.vertex = d.vertex) : decide (r.Alternates a b c d) = decide (a ∈ r.rotationInterval c d) + decide (b ∈ r.rotationInterval c d)

For four distinct ports, the alternating bit is exactly the sum of the two interval membership bits. The off-vertex case is zero because rotation intervals stay at one vertex.

theorem Cslib.Complexity.Graph.RotationSystem.sum_alternates_eq_interval {G : Graph} (r : G.RotationSystem) {x y : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (Q : G.ClosedPassages y) (hdisj : ∀ (e : Fin G.edges.length), x e = true → y e = true → False) (j : Fin Q.count) : ∑ i : Fin P.count, decide (r.Alternates (P.dart i false) (P.dart i true) (Q.dart j false) (Q.dart j true)) = ∑ d ∈ r.rotationInterval (Q.dart j false) (Q.dart j true), x d.1

Against one passage of an edge-disjoint system, the sum of all alternating passage pairs counts precisely the supported darts in its literal rotation interval. Local pairing choices and multiple visits are unrestricted.

theorem Cslib.Complexity.Graph.RotationSystem.sum_alternates_eq_faceColors {G : Graph} (r : G.RotationSystem) {x y : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (Q : G.ClosedPassages y) (hdisj : ∀ (e : Fin G.edges.length), x e = true → y e = true → False) (q : r.Face → Bool) (hq : r.faceBoundary q = x) (j : Fin Q.count) : ∑ i : Fin P.count, decide (r.Alternates (P.dart i false) (P.dart i true) (Q.dart j false) (Q.dart j true)) = q ⟦Q.dart j true⟧ + q ⟦Q.dart j false⟧

If the first support is a face boundary, its local alternating count along one passage of an edge-disjoint system is the sum of the two incident face colors.

noncomputable def Cslib.Complexity.Graph.RotationSystem.intersectionParity {G : Graph} (r : G.RotationSystem) {x y : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (Q : G.ClosedPassages y) : Bool

Total intersection parity of indexed passage pairs, using literal local alternation in the actual rotation. Distinct visits and arbitrary local pairing choices are counted separately.

theorem Cslib.Complexity.Graph.RotationSystem.intersectionParity_faceBoundary {G : Graph} (r : G.RotationSystem) {x y : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (Q : G.ClosedPassages y) (hdisj : ∀ (e : Fin G.edges.length), x e = true → y e = true → False) (q : r.Face → Bool) (hq : r.faceBoundary q = x) : r.intersectionParity P Q = false

Face-boundary support has even total intersection with every edge-disjoint closed passage system, independently of genus. Adjacent face colors agree on the second support; its exactly-once dart enumeration makes every endpoint contribution occur twice.

theorem Cslib.Complexity.Graph.RotationSystem.intersectionParity_eq_false {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hgenus : r.NumericalGenusZero) {x y : Fin G.edges.length → Bool} (P : G.ClosedPassages x) (Q : G.ClosedPassages y) (hdisj : ∀ (e : Fin G.edges.length), x e = true → y e = true → False) : r.intersectionParity P Q = false

Any two supported edge-disjoint closed passage systems on a componentwise numerically genus-zero rotation have even total local intersection parity. Endpoints must be declared; vertex names may be sparse or duplicated, and loops, parallel edges, isolated vertices, disconnected supports, multiple visits and arbitrary local pairings are allowed. All local circular-order and parity facts are proved internally. No geometric or Hanani–Tutte premise is assumed or concluded.