Choosing an actual external blossom attachment

The finite first-input/last-output selection in Lemma 44 of [KKR18], arXiv:1602.03124v6, printed pp. 21–22. The scan tests actual two-port exchanges in the original tables. Its correctness supplies both no-shortcut guards; no compatibility promise about an outside comparison labeling is assumed.

def Cslib.Logic.PL.CSP.Blossom.accessibleArcs {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (arcs : List (DAG.Arc F)) (x : F.Occurrence) : List (DAG.Arc F)

Accessible actual arcs at the external port's original constraint.

def Cslib.Logic.PL.CSP.Blossom.attachmentArc {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (arcs : List (DAG.Arc F)) (x : F.Occurrence) : Option (DAG.Arc F)

Prefer the earliest accessible input; if none exists, use the latest accessible output. Both folds are funded by the actual arc list, independently of binary variable names.

theorem Cslib.Logic.PL.CSP.Blossom.attachmentArc_spec {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (arcs : List (DAG.Arc F)) (x : F.Occurrence) (hne : accessibleArcs f arcs x ≠ []) : ∃ (a : DAG.Arc F), attachmentArc f arcs x = some a ∧ a ∈ arcs ∧ x.fst = a.occurrence.fst ∧ ValidLabeling Table.sem (DAG.pairFlip f x a.occurrence) ∧ (∀ e ∈ arcs, e.incoming = true → e.occurrence.fst = x.fst → e.time < a.time → ¬ValidLabeling Table.sem (DAG.pairFlip f e.occurrence x)) ∧ (a.incoming = false → ∀ e ∈ arcs, x.fst = e.occurrence.fst → a.time < e.time → ¬ValidLabeling Table.sem (DAG.pairFlip f x e.occurrence))

The executable choice supplies exactly the local exchange and no-shortcut facts needed to attach the outside port, in either orientation.

theorem Cslib.Logic.PL.CSP.Blossom.valid_attachment_cut {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} {arcs : List (DAG.Arc F)} {T : F.DAG} (harcs : T.arcs = arcs.toFinset) (h : DAG.IsFDAG Table.sem f T) (hp : T.PairedCopies) (hM : EdgeInstance.EvenConstraints Table.sem F) (x : F.Occurrence) (hx : x.var ∉ T.vars) (hne : accessibleArcs f arcs x ≠ []) : ∃ (a : DAG.Arc F), attachmentArc f arcs x = some a ∧ a ∈ T.arcs ∧ x.fst = a.occurrence.fst ∧ ∀ (cs : Finset (DAG.Copy F)), a.copy ∉ cs → ValidLabeling Table.sem (((T.cutAt cs a).attachPort { occurrence := x, time := a.time, incoming := !a.incoming }).flip f)

Every successful finite attachment scan permits completion of any cut ending at its selected copy. All forbidden exchanges follow from the scan; they are not extra premises.