Appending actual CSP bodies with disjoint variable supports

The positional occurrence correspondence transports the disjoint graph rotation to the actual dense incidence names. Variable supports are disjoint; constraint positions occupy separate blocks. Original row order, directed argument order and source numerical genus are retained, including closed components and nullary constraints.

noncomputable def Cslib.Complexity.CSP.appendDartEquiv {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) : ((incidenceGraph F).disjointUnion (incidenceGraph H)).Dart ≃ (incidenceGraph (F ++ H)).Dart

Actual disjoint graph darts map to the original argument positions in the appended body.

theorem Cslib.Complexity.CSP.appendDartEquiv_inl {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (o : F.Occurrence) (side : Bool) : (appendDartEquiv F H) (((incidenceGraph F).disjointDartEquiv (incidenceGraph H)) (Sum.inl (incidenceDart o side))) = incidenceDart ((F.appendOccurrenceEquiv H) (Sum.inl o)) side

Left occurrence/end coordinates are literal through both indexed graph maps.

theorem Cslib.Complexity.CSP.appendDartEquiv_inr {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (o : H.Occurrence) (side : Bool) : (appendDartEquiv F H) (((incidenceGraph F).disjointDartEquiv (incidenceGraph H)) (Sum.inr (incidenceDart o side))) = incidenceDart ((F.appendOccurrenceEquiv H) (Sum.inr o)) side

Right occurrence/end coordinates retain the exact right constraint block shift.

theorem Cslib.Complexity.CSP.appendDartEquiv_vertex_eq_iff {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (hd : F.vars.Disjoint H.vars) (a b : ((incidenceGraph F).disjointUnion (incidenceGraph H)).Dart) : ((appendDartEquiv F H) a).vertex = ((appendDartEquiv F H) b).vertex ↔ a.vertex = b.vertex

Endpoint fibers match precisely when the actual occurring variable supports are disjoint. No condition is placed on repetitions inside either body or on its graph degrees.

theorem Cslib.Complexity.CSP.reverse_appendDartEquiv {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (d : ((incidenceGraph F).disjointUnion (incidenceGraph H)).Dart) : (appendDartEquiv F H) d.reverse = ((appendDartEquiv F H) d).reverse

Positional concatenation commutes with actual edge reversal.

noncomputable def Cslib.Complexity.CSP.appendRotation {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (hd : F.vars.Disjoint H.vars) (r : (incidenceGraph F).RotationSystem) (s : (incidenceGraph H).RotationSystem) : (incidenceGraph (F ++ H)).RotationSystem

Append two actual incidence rotations with disjoint occurring variable names.

theorem Cslib.Complexity.CSP.numericalGenusZero_appendRotation {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (hd : F.vars.Disjoint H.vars) (r : (incidenceGraph F).RotationSystem) (s : (incidenceGraph H).RotationSystem) (hr : r.NumericalGenusZero) (hs : s.NumericalGenusZero) : (appendRotation F H hd r s).NumericalGenusZero

Target numerical genus follows from the two endpoint-declared source incidences.

theorem Cslib.Complexity.CSP.rotate_appendRotation {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (hd : F.vars.Disjoint H.vars) (r : (incidenceGraph F).RotationSystem) (s : (incidenceGraph H).RotationSystem) (d : (incidenceGraph F).Dart ⊕ (incidenceGraph H).Dart) : (appendRotation F H hd r s).rotate ((appendDartEquiv F H) (((incidenceGraph F).disjointDartEquiv (incidenceGraph H)) d)) = (appendDartEquiv F H) (((incidenceGraph F).disjointDartEquiv (incidenceGraph H)) (Sum.map (⇑r.rotate) (⇑s.rotate) d))

Appended successors are exactly the two old source rotations in positional coordinates.

theorem Cslib.Complexity.CSP.respectsArgumentOrder_appendRotation {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (hd : F.vars.Disjoint H.vars) (r : (incidenceGraph F).RotationSystem) (s : (incidenceGraph H).RotationSystem) (hr : RespectsArgumentOrder r) (hs : RespectsArgumentOrder s) : RespectsArgumentOrder (appendRotation F H hd r s)

Original clockwise argument order is inherited on both exact constraint blocks.

theorem Cslib.Complexity.CSP.verifyRotationCertificate_appendRotation {Rel V : Type} [DecidableEq V] (F H : Logic.PL.CSP Rel V) (hd : F.vars.Disjoint H.vars) (r : (incidenceGraph F).RotationSystem) (s : (incidenceGraph H).RotationSystem) (hr : r.NumericalGenusZero) (hs : s.NumericalGenusZero) (hor : RespectsArgumentOrder r) (hos : RespectsArgumentOrder s) : verifyRotationCertificate (F ++ H) (Graph.RotationCertificate.ofRotation (appendRotation F H hd r s)) = true

Full checker acceptance for the actual appended body, derived from its source rotations.