Occurrence coordinates on actual incidence darts

The existing indexed occurrence and its endpoint side parametrize the incidence graph's actual darts. Repeated variables and identical constraints retain separate positions; nullary constraints have no darts. This coordinate equivalence has no polygon, genus, planarity or runtime premise. The declarations are relocated unchanged from Primal.Graph.

Main definitions

• Cslib.Complexity.CSP.incidenceDartEquiv: exact occurrence/end coordinates.

Main results

• Cslib.Complexity.CSP.incidenceDartEquiv_apply: the literal forward coordinate map.

noncomputable def Cslib.Complexity.CSP.incidenceDartEquiv {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : F.Occurrence × Bool ≃ (incidenceGraph F).Dart

Occurrence/end coordinates on the existing incidence graph.

@[simp]

theorem Cslib.Complexity.CSP.incidenceDartEquiv_apply {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (x : F.Occurrence × Bool) : (incidenceDartEquiv F) x = incidenceDart x.1 x.2

The forward incidence coordinate map is the existing occurrence/end map.