Actual incidence transport for identification of two variable names

A map with precisely the selected-pair kernel on occurring labels matches the generic vertex merge after actual dense naming. All indexed argument ends remain in place; labels outside the occurring set are unrestricted. Cofaciality and argument-end conditions are separate obligations of an ordered realization, not consequences of arbitrary renaming.

def Cslib.Complexity.CSP.identificationDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (h k : (incidenceGraph F).Dart) : (Graph.RotationSystem.mergeGraph h k).Dart ≃ (incidenceGraph (Logic.PL.CSP.relabel f F)).Dart

Retain edge/end positions when transporting a generic merge to the actual renamed CSP.

theorem Cslib.Complexity.CSP.identificationDartEquiv_vertex_eq_iff {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (x y : V) (hx : x ∈ F.vars) (hy : y ∈ F.vars) (h k : (incidenceGraph F).Dart) (hh : h.vertex = List.idxOf x F.distinctVars) (hk : k.vertex = List.idxOf y F.distinctVars) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id y x a = Function.update id y x b) (a b : (Graph.RotationSystem.mergeGraph h k).Dart) : ((identificationDartEquiv F f h k) a).vertex = ((identificationDartEquiv F f h k) b).vertex ↔ a.vertex = b.vertex

The selected-pair kernel is required only on actually occurring names. Dense renaming and repeated source labels are accounted for internally, without a free-port injection.

theorem Cslib.Complexity.CSP.index_identificationDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (h k : (incidenceGraph F).Dart) (d : (Graph.RotationSystem.mergeGraph h k).Dart) : ((identificationDartEquiv F f h k) d).index = d.index

The coordinate transport retains the literal binary dart index.

theorem Cslib.Complexity.CSP.reverse_identificationDartEquiv {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (h k : (incidenceGraph F).Dart) (d : (Graph.RotationSystem.mergeGraph h k).Dart) : (identificationDartEquiv F f h k) d.reverse = ((identificationDartEquiv F f h k) d).reverse

Actual edge reversal is retained by the merge-to-renamed-CSP transport.

def Cslib.Complexity.CSP.identifyVariablesRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (x y : V) (hx : x ∈ F.vars) (hy : y ∈ F.vars) (hxy : x ≠ y) (h k : (incidenceGraph F).Dart) (hh : h.vertex = List.idxOf x F.distinctVars) (hk : k.vertex = List.idxOf y F.distinctVars) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id y x a = Function.update id y x b) (rho : (incidenceGraph F).RotationSystem) : (incidenceGraph (Logic.PL.CSP.relabel f F)).RotationSystem

Construct the actual renamed CSP rotation by the selected outgoing-corner swap and positional dense-name transport. The label map need only have the selected-pair kernel on occurring names; distinct old variables need not remain distinct in the target.

theorem Cslib.Complexity.CSP.numericalGenusZero_identifyVariablesRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (x y : V) (hx : x ∈ F.vars) (hy : y ∈ F.vars) (hxy : x ≠ y) (h k : (incidenceGraph F).Dart) (hh : h.vertex = List.idxOf x F.distinctVars) (hk : k.vertex = List.idxOf y F.distinctVars) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id y x a = Function.update id y x b) (rho : (incidenceGraph F).RotationSystem) (hr : rho.NumericalGenusZero) (hf : rho.faceNext.SameCycle h k) : (identifyVariablesRotation F f x y hx hy hxy h k hh hk hkernel rho).NumericalGenusZero

Numerical genus is preserved on the actual target CSP when the chosen existing corners are cofacial. The target proof is derived from generic surgery and the actual source/target endpoint guards, not assumed as an embedding provider.

theorem Cslib.Complexity.CSP.rotate_identifyVariablesRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (x y : V) (hx : x ∈ F.vars) (hy : y ∈ F.vars) (hxy : x ≠ y) (h k : (incidenceGraph F).Dart) (hh : h.vertex = List.idxOf x F.distinctVars) (hk : k.vertex = List.idxOf y F.distinctVars) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id y x a = Function.update id y x b) (rho : (incidenceGraph F).RotationSystem) (d : (incidenceGraph F).Dart) : (identifyVariablesRotation F f x y hx hy hxy h k hh hk hkernel rho).rotate ((relabelDartEquiv F f) d) = (relabelDartEquiv F f) (rho.rotate ((Equiv.swap h k) d))

The literal successor is the old forward rotation after swapping just the two selected outgoing corners. The positional target coordinate map does not reflect either block.

theorem Cslib.Complexity.CSP.respectsArgumentOrder_identifyVariablesRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (x y : V) (hx : x ∈ F.vars) (hy : y ∈ F.vars) (hxy : x ≠ y) (h k : (incidenceGraph F).Dart) (hh : h.vertex = List.idxOf x F.distinctVars) (hk : k.vertex = List.idxOf y F.distinctVars) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id y x a = Function.update id y x b) (hs : h.2 = false) (ks : k.2 = false) (rho : (incidenceGraph F).RotationSystem) (ho : RespectsArgumentOrder rho) : RespectsArgumentOrder (identifyVariablesRotation F f x y hx hy hxy h k hh hk hkernel rho)

Swapping variable-side outgoing corners retains every original relation's directed argument cycle. Both end-tag hypotheses are explicit: swapping constraint corners would not have this property at arbitrary arity.

theorem Cslib.Complexity.CSP.ofRotation_identifyVariablesRotation {Rel V W : Type} [DecidableEq V] [DecidableEq W] (F : Logic.PL.CSP Rel V) (f : V → W) (x y : V) (hx : x ∈ F.vars) (hy : y ∈ F.vars) (hxy : x ≠ y) (h k : (incidenceGraph F).Dart) (hh : h.vertex = List.idxOf x F.distinctVars) (hk : k.vertex = List.idxOf y F.distinctVars) (hkernel : ∀ a ∈ F.vars, ∀ b ∈ F.vars, f a = f b ↔ Function.update id y x a = Function.update id y x b) (rho : (incidenceGraph F).RotationSystem) : Graph.RotationCertificate.ofRotation (identifyVariablesRotation F f x y hx hy hxy h k hh hk hkernel rho) = (Graph.RotationCertificate.ofRotation rho).swapSuccessors h.index k.index

Complete generated-table identity for actual incidence identification: dense-name transport retains positions, so only the two selected outgoing entries are exchanged.