Attaching an external port to a timestamped incidence DAG

The last part of Lemma 44 of [KKR18], arXiv:1602.03124v6, printed pp. 21–22, attaches an outside variable to a selected copied blossom constraint. The finite support permits either orientation: an external source receives a rank below the old graph, and an external sink receives a rank above its maximum. No timestamp renumbering or minimum-timestamp predecessor is needed. The cut/completion lemmas below are an original unified argument for the source's attachment cases; they retain all six IsFDAG invariants.

theorem Cslib.Logic.PL.CSP.DAG.PairedCopies.full_copy {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T S : F.DAG} (hT : T.PairedCopies) (hS : S.PairedCopies) (hst : S.Subgraph T) {e : Arc F} (he : e ∈ T.arcs) (hc : e.copy ∈ S.copies) : e ∈ S.arcs

A paired subgraph contains every ambient arc at each of its copied nodes.

def Cslib.Logic.PL.CSP.DAG.cutAt {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) (cs : Finset (Copy F)) (a : Arc F) : F.DAG

Keep whole selected copies and one boundary arc at a further copy. Isolated old variables remain in the support, so externality can still be checked against the original blossom.

theorem Cslib.Logic.PL.CSP.DAG.Supported.cutAt {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} (h : T.Supported) (cs : Finset (Copy F)) (a : Arc F) : (T.cutAt cs a).Supported

Cutting at an actual arc is a supported subgraph operation.

theorem Cslib.Logic.PL.CSP.DAG.cutAt_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) (cs : Finset (Copy F)) {a : Arc F} (ha : a ∈ T.arcs) (hs : T.Supported) : (T.cutAt cs a).Subgraph T

Cutting deletes actual arcs and copies only.

theorem Cslib.Logic.PL.CSP.DAG.PairedCopies.cutAt {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} {cs : Finset (Copy F)} {a : Arc F} (hp : T.PairedCopies) (hc : a.copy ∉ cs) : (∀ e ∈ (T.cutAt cs a).arcs, e.copy = a.copy → e = a) ∧ ∀ c ∈ (T.cutAt cs a).copies, c ≠ a.copy → ∃ b ∈ (T.cutAt cs a).arcs, ∃ d ∈ (T.cutAt cs a).arcs, b.incoming = true ∧ b.copy = c ∧ d.copy = c ∧ b ≠ d ∧ ∀ e ∈ (T.cutAt cs a).arcs, e.copy = c → e = b ∨ e = d

Every copy of the cut has its old pair, except the selected boundary copy, which has exactly its selected arc. This is the structural certificate used before attaching a port.

theorem Cslib.Logic.PL.CSP.DAG.cutAt_arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T S : F.DAG} (hT : T.PairedCopies) (hS : S.PairedCopies) (hst : S.Subgraph T) (hs : S.Supported) {a : Arc F} (ha : a ∈ T.arcs) : (T.cutAt S.copies a).arcs = insert a S.arcs

Cutting at the end of a paired subgraph retains its precise original arcs and the one boundary arc. This identifies the eventual flip with an actual arm of the cycle.

def Cslib.Logic.PL.CSP.DAG.attachPort {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (T : F.DAG) (a : Arc F) : F.DAG

Attach one actual original port at an already supported copied constraint.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.attachPort {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} (h : IsFDAG sem f T) (a : Arc F) (hx : a.occurrence.var ∉ T.vars) (hc : a.copy ∈ T.copies) (hp : ∀ b ∈ T.arcs, a.copy = b.copy → ValidLabeling sem (pairFlip f a.occurrence b.occurrence)) (hbefore : ∀ b ∈ T.arcs, b.incoming = true → b.occurrence.fst = a.occurrence.fst → b.time < a.time → ¬ValidLabeling sem (pairFlip f b.occurrence a.occurrence)) (hafter : a.incoming = true → ∀ b ∈ T.arcs, a.occurrence.fst = b.occurrence.fst → a.time < b.time → ¬ValidLabeling sem (pairFlip f a.occurrence b.occurrence)) : IsFDAG sem f (T.attachPort a)

Attaching an outside source or sink preserves all six f-DAG conditions when the local pair is feasible and the before/after forbidden moves hold. Blossom lifting derives these forbidden moves by selecting the first accessible input or the last accessible output.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.valid_complete_cut {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} (h : IsFDAG sem f T) (hp : T.PairedCopies) (hM : EdgeInstance.EvenConstraints sem F) (cs : Finset (Copy F)) {a : Arc F} (ha : a ∈ T.arcs) (hc : a.copy ∉ cs) (x : F.Occurrence) (hx : x.var ∉ T.vars) (hxa : x.fst = a.occurrence.fst) (hv : ValidLabeling sem (pairFlip f x a.occurrence)) (hbefore : ∀ e ∈ T.arcs, e.incoming = true → e.occurrence.fst = x.fst → e.time < a.time → ¬ValidLabeling sem (pairFlip f e.occurrence x)) (hafter : a.incoming = false → ∀ e ∈ T.arcs, x.fst = e.occurrence.fst → a.time < e.time → ¬ValidLabeling sem (pairFlip f x e.occurrence)) : ValidLabeling sem (((T.cutAt cs a).attachPort { occurrence := x, time := a.time, incoming := !a.incoming }).flip f)

Complete a cut blossom arm by one external port. The missing copy receives precisely the boundary port and its external mate; all other retained copies keep their original pair. The before/after conditions are local finite tests, discharged by the first-input/last-output selection in blossom lifting.