Directed transport along actual CSP occurrence bijections

An occurrence bijection retaining the variable and constraint fiber partitions transports the actual incidence rotation. Intertwining the original cyclic argument successor preserves its sign, and numerical genus follows from indexed edge/reversal transport. Isolated nullary constraints need no occurrence or invented dart. These original structural tools do not provide an embedding: concrete scope operations must supply and prove their actual bijections.

noncomputable def Cslib.Complexity.CSP.occurrenceDartEquiv {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (e : F.Occurrence ≃ H.Occurrence) : (incidenceGraph F).Dart ≃ (incidenceGraph H).Dart

Reindex the actual two ends of each occurrence, retaining their endpoint side tags.

theorem Cslib.Complexity.CSP.occurrenceDartEquiv_apply {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (e : F.Occurrence ≃ H.Occurrence) (o : F.Occurrence) (side : Bool) : (occurrenceDartEquiv e) (incidenceDart o side) = incidenceDart (e o) side

The occurrence/end formula is literal and retains each original end tag.

theorem Cslib.Complexity.CSP.occurrenceDartEquiv_vertex_eq_iff {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (e : F.Occurrence ≃ H.Occurrence) (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 ↔ o.fst = p.fst) (a b : (incidenceGraph F).Dart) : ((occurrenceDartEquiv e) a).vertex = ((occurrenceDartEquiv e) b).vertex ↔ a.vertex = b.vertex

Fiber hypotheses concern actual names and constraint positions, not dense numbering. They allow arbitrary repeated original variable labels and constraint records.

theorem Cslib.Complexity.CSP.occurrenceDartEquiv_reverse {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (e : F.Occurrence ≃ H.Occurrence) (d : (incidenceGraph F).Dart) : (occurrenceDartEquiv e) d.reverse = ((occurrenceDartEquiv e) d).reverse

Reversal commutes with the occurrence bijection, including repeated/parallel edges.

noncomputable def Cslib.Complexity.CSP.occurrenceTransport {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (r : (incidenceGraph F).RotationSystem) (e : F.Occurrence ≃ H.Occurrence) (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 ↔ o.fst = p.fst) : (incidenceGraph H).RotationSystem

Transport the existing rotation along an actual fiber-preserving occurrence bijection.

theorem Cslib.Complexity.CSP.occurrenceTransport_rotate {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (r : (incidenceGraph F).RotationSystem) (e : F.Occurrence ≃ H.Occurrence) (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 ↔ o.fst = p.fst) (d : (incidenceGraph F).Dart) : (occurrenceTransport r e hv hc).rotate ((occurrenceDartEquiv e) d) = (occurrenceDartEquiv e) (r.rotate d)

Directed rotation intertwining on each actual source dart.

theorem Cslib.Complexity.CSP.numericalGenusZero_occurrenceTransport {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (r : (incidenceGraph F).RotationSystem) (e : F.Occurrence ≃ H.Occurrence) (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 ↔ o.fst = p.fst) (hr : r.NumericalGenusZero) : (occurrenceTransport r e hv hc).NumericalGenusZero

Componentwise numerical genus is retained internally, including arbitrary nullary and point components. No connectedness or target-genus provider is assumed.

theorem Cslib.Complexity.CSP.respectsArgumentOrder_occurrenceTransport {Rel Other V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {H : Logic.PL.CSP Other W} (r : (incidenceGraph F).RotationSystem) (e : F.Occurrence ≃ H.Occurrence) (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 ↔ o.fst = p.fst) (hn : ∀ (o : F.Occurrence), e (argumentSuccessor o) = argumentSuccessor (e o)) (hr : RespectsArgumentOrder r) : RespectsArgumentOrder (occurrenceTransport r e hv hc)

The original clockwise argument order survives precisely directed successor intertwining. A reflected higher-arity scope cannot silently satisfy this premise.