Actual incidence transport for joining two constraint centers

The occurrence correspondence retains variable fibers and identifies exactly the two selected constraint positions. Dense variable names remain below every constraint center. The generic vertex merge is transported to the actual target incidence graph; the target genus follows from source genus and actual different components.

noncomputable def Cslib.Complexity.CSP.constraintJoinDartEquiv {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {T : Logic.PL.CSP Other W} (e : F.Occurrence ≃ T.Occurrence) (h k : (incidenceGraph F).Dart) : (Graph.RotationSystem.mergeGraph h k).Dart ≃ (incidenceGraph T).Dart

Transport retained edge/end positions after the literal constraint-center merge.

theorem Cslib.Complexity.CSP.constraintJoinDartEquiv_vertex_eq_iff {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {T : Logic.PL.CSP Other W} (e : F.Occurrence ≃ T.Occurrence) (a b : ℕ) (h k : (incidenceGraph F).Dart) (hh : h.vertex = F.numVars + a) (hk : k.vertex = F.numVars + b) (hv : ∀ (o p : F.Occurrence), (e o).var = (e p).var ↔ o.var = p.var) (hc : ∀ (o p : F.Occurrence), (e o).fst = (e p).fst ↔ Function.update id b a ↑o.fst = Function.update id b a ↑p.fst) (d f : (Graph.RotationSystem.mergeGraph h k).Dart) : ((constraintJoinDartEquiv e h k) d).vertex = ((constraintJoinDartEquiv e h k) f).vertex ↔ d.vertex = f.vertex

Exact endpoint guard for joining constraint centers. Variable fibers are retained; constraint-position fibers have exactly the selected-pair kernel.

noncomputable def Cslib.Complexity.CSP.constraintJoinRotation {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {T : Logic.PL.CSP Other W} (e : F.Occurrence ≃ T.Occurrence) (a b : ℕ) (hab : a ≠ b) (h k : (incidenceGraph F).Dart) (hh : h.vertex = F.numVars + a) (hk : k.vertex = F.numVars + b) (hv : ∀ (o p : F.Occurrence), (e o).var = (e p).var ↔ o.var = p.var) (hc : ∀ (o p : F.Occurrence), (e o).fst = (e p).fst ↔ Function.update id b a ↑o.fst = Function.update id b a ↑p.fst) (r : (incidenceGraph F).RotationSystem) : (incidenceGraph T).RotationSystem

Literal outgoing swap followed by the proved target occurrence transport.

theorem Cslib.Complexity.CSP.reverse_constraintJoinDartEquiv {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {T : Logic.PL.CSP Other W} (e : F.Occurrence ≃ T.Occurrence) (h k : (incidenceGraph F).Dart) (d : (Graph.RotationSystem.mergeGraph h k).Dart) : (constraintJoinDartEquiv e h k) d.reverse = ((constraintJoinDartEquiv e h k) d).reverse

Actual indexed reversals are retained through constraint-center identification.

theorem Cslib.Complexity.CSP.numericalGenusZero_constraintJoinRotation {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {T : Logic.PL.CSP Other W} (e : F.Occurrence ≃ T.Occurrence) (a b : ℕ) (hab : a ≠ b) (h k : (incidenceGraph F).Dart) (hh : h.vertex = F.numVars + a) (hk : k.vertex = F.numVars + b) (hv : ∀ (o p : F.Occurrence), (e o).var = (e p).var ↔ o.var = p.var) (hc : ∀ (o p : F.Occurrence), (e o).fst = (e p).fst ↔ Function.update id b a ↑o.fst = Function.update id b a ↑p.fst) (r : (incidenceGraph F).RotationSystem) (hr : r.NumericalGenusZero) (hd : ¬Graph.RotationCertificate.SameComponent (incidenceGraph F) h.vertex k.vertex) : (constraintJoinRotation e a b hab h k hh hk hv hc r).NumericalGenusZero

Numerical genus is derived internally from source genus and different actual components.

theorem Cslib.Complexity.CSP.rotate_constraintJoinRotation {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {T : Logic.PL.CSP Other W} (e : F.Occurrence ≃ T.Occurrence) (a b : ℕ) (hab : a ≠ b) (h k : (incidenceGraph F).Dart) (hh : h.vertex = F.numVars + a) (hk : k.vertex = F.numVars + b) (hv : ∀ (o p : F.Occurrence), (e o).var = (e p).var ↔ o.var = p.var) (hc : ∀ (o p : F.Occurrence), (e o).fst = (e p).fst ↔ Function.update id b a ↑o.fst = Function.update id b a ↑p.fst) (r : (incidenceGraph F).RotationSystem) (d : (incidenceGraph F).Dart) : (constraintJoinRotation e a b hab h k hh hk hv hc r).rotate ((occurrenceDartEquiv e) d) = (occurrenceDartEquiv e) (r.rotate ((Equiv.swap h k) d))

The transported successor is exactly the selected outgoing swap on old indexed darts.