Positional incidence darts under arbitrary variable maps

An arbitrary variable map retains every original constraint/argument position and both indexed edge ends. Its endpoint formula uses the target's actual dense names. Noninjective maps can change vertex fibers, so this coordinate equivalence alone supplies no rotation or numerical-genus claim. These original identities support actual variable identification.

def Cslib.Complexity.CSP.relabelDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) : (incidenceGraph F).Dart ≃ (incidenceGraph (Logic.PL.CSP.relabel f F)).Dart

Variable maps keep edge/end positions even when they identify source variable names.

theorem Cslib.Complexity.CSP.vertex_relabelDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (o : F.Occurrence) (side : Bool) : ((relabelDartEquiv F f) (incidenceDart o side)).vertex = if side = true then (Logic.PL.CSP.relabel f F).numVars + ↑o.fst else List.idxOf (f o.var) (Logic.PL.CSP.relabel f F).distinctVars

The target endpoint is its actual dense variable name or unchanged constraint position.

theorem Cslib.Complexity.CSP.index_relabelDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (d : (incidenceGraph F).Dart) : ((relabelDartEquiv F f) d).index = d.index

The literal binary index is unchanged by the variable map.

theorem Cslib.Complexity.CSP.reverse_relabelDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (d : (incidenceGraph F).Dart) : (relabelDartEquiv F f) d.reverse = ((relabelDartEquiv F f) d).reverse

Positional variable maps retain the two opposite ends of every actual edge occurrence.