Actual blossom arms ending at an external port

These candidates are the two portions of the original incidence cycle used in Lemma 44 of [KKR18], arXiv:1602.03124v6, printed pp. 21–22. They retain repeated original constraints. Only the boundary incidence is replaced by the actual outside port. The cut/completion proof is an original alternative to the source's separate attachment cases; it retains all six f-DAG invariants and the same first-input/last-output choice.

def Cslib.Logic.PL.CSP.Blossom.inputArm {F : CSP Table ℕ} (w : F.Walk) (j : Fin w.steps.length) (x : F.Occurrence) : F.Walk

The prefix arm stops at the selected input and exits through the outside port.

def Cslib.Logic.PL.CSP.Blossom.outputArm {F : CSP Table ℕ} (w : F.Walk) (j : Fin w.steps.length) (x : F.Occurrence) : F.Walk

The other arm traverses the suffix backwards, then exits at the selected output.

theorem Cslib.Logic.PL.CSP.Blossom.inputArm_isWalk {F : CSP Table ℕ} {w : F.Walk} (hw : w.IsWalk) (j : Fin w.steps.length) (x : F.Occurrence) (hx : x.var ∉ internal w) (hc : match w.steps[↑j] with | (input, snd) => input.fst = x.fst) : (inputArm w j x).IsWalk ∧ (inputArm w j x).start = w.start ∧ (inputArm w j x).finish = x.var

The prefix candidate is an actual linked trail, with unchanged base and external endpoint.

theorem Cslib.Logic.PL.CSP.Blossom.outputArm_isWalk {F : CSP Table ℕ} {w : F.Walk} (hw : w.IsWalk) (hclosed : w.finish = w.start) (j : Fin w.steps.length) (x : F.Occurrence) (hx : x.var ∉ internal w) (hc : match w.steps[↑j] with | (fst, output) => output.fst = x.fst) : (outputArm w j x).IsWalk ∧ (outputArm w j x).start = w.start ∧ (outputArm w j x).finish = x.var

The reverse-suffix candidate is an actual linked trail with the same base and endpoint.

theorem Cslib.Logic.PL.CSP.Blossom.inputArm_flip {F : CSP Table ℕ} {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (hw : w.IsWalk) (hd : w.DistinctCopies ts) (h : (DAG.blossomDAG w ts pivot).Supported) (j : Fin w.steps.length) (x : F.Occurrence) (f : F.OccurrenceLabeling Bool) : have a := { occurrence := w.steps[↑j].1, time := ts[↑j], incoming := decide (↑j < pivot) }; (((DAG.blossomDAG w ts pivot).cutAt (DAG.blossomDAG (w.take ↑j) (List.take (↑j) ts) pivot).copies a).attachPort { occurrence := x, time := a.time, incoming := !a.incoming }).flip f = (inputArm w j x).flip f

Completing the graph cut of a prefix flips exactly the executable prefix arm.

theorem Cslib.Logic.PL.CSP.Blossom.outputArm_flip {F : CSP Table ℕ} {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (hw : w.IsWalk) (hd : w.DistinctCopies ts) (h : (DAG.blossomDAG w ts pivot).Supported) (j : Fin w.steps.length) (x : F.Occurrence) (f : F.OccurrenceLabeling Bool) : have a := { occurrence := w.steps[↑j].2, time := ts[↑j], incoming := decide (pivot ≤ ↑j + 1) }; (((DAG.blossomDAG w ts pivot).cutAt (DAG.blossomDAG (w.drop (↑j + 1)) (List.drop (↑j + 1) ts) (pivot - (↑j + 1))).copies a).attachPort { occurrence := x, time := a.time, incoming := !a.incoming }).flip f = (outputArm w j x).flip f

Completing the graph cut of a suffix flips exactly the executable reverse-suffix arm.

def Cslib.Logic.PL.CSP.Blossom.armCandidates {F : CSP Table ℕ} (w : F.Walk) (x : F.Occurrence) : List F.Walk

Two actual arm candidates per step at the outside port's original constraint.

theorem Cslib.Logic.PL.CSP.Blossom.mem_armCandidates {F : CSP Table ℕ} {w : F.Walk} (x : F.Occurrence) (p : F.Walk) : p ∈ armCandidates w x ↔ ∃ (j : Fin w.steps.length), match w.steps[↑j] with | (input, snd) => input.fst = x.fst ∧ (p = inputArm w j x ∨ p = outputArm w j x)

The scan retains exactly the two arms at matching original constraints.

theorem Cslib.Logic.PL.CSP.Blossom.armCandidates_isWalk {F : CSP Table ℕ} {w : F.Walk} (hw : w.IsWalk) (hclosed : w.finish = w.start) {x : F.Occurrence} (hx : x.var ∉ internal w) {p : F.Walk} (hp : p ∈ armCandidates w x) : p.IsWalk ∧ p.start = w.start ∧ p.finish = x.var

Every scanned candidate is an actual trail from the blossom base to the outside variable.

theorem Cslib.Logic.PL.CSP.Blossom.exists_valid_arm {F : CSP Table ℕ} {w : F.Walk} {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hM : EdgeInstance.EvenConstraints Table.sem F) (x : F.Occurrence) (hx : x.var ∉ internal w) (hex : ∃ o ∈ w.edges, x.fst = o.fst ∧ ValidLabeling Table.sem (DAG.pairFlip f x o)) : ∃ p ∈ armCandidates w x, ValidLabeling Table.sem (p.flip f)

A feasible exchange from an outside port into the blossom always yields one valid actual arm. The proof uses the selected copied node and the full f-DAG no-shortcut invariant.

def Cslib.Logic.PL.CSP.Blossom.attachmentWalk {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (x : F.Occurrence) : Option F.Walk

Construct an actual valid arm by scanning at most two candidates per cycle step.

theorem Cslib.Logic.PL.CSP.Blossom.attachmentWalk_spec {F : CSP Table ℕ} {w : F.Walk} {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hM : EdgeInstance.EvenConstraints Table.sem F) (x : F.Occurrence) (hx : x.var ∉ internal w) (hex : ∃ o ∈ w.edges, x.fst = o.fst ∧ ValidLabeling Table.sem (DAG.pairFlip f x o)) : ∃ (p : F.Walk), attachmentWalk f w x = some p ∧ p ∈ armCandidates w x ∧ p.IsWalk ∧ p.start = w.start ∧ p.finish = x.var ∧ ValidLabeling Table.sem (p.flip f)

The returned finite walk is valid and really runs from the old base to the outside port. Existence follows from the six-invariant blossom proof, not a lifting oracle.

theorem Cslib.Logic.PL.CSP.Blossom.armCandidates_edges {F : CSP Table ℕ} {w : F.Walk} {x : F.Occurrence} {p : F.Walk} (hp : p ∈ armCandidates w x) {o : F.Occurrence} (ho : o ∈ p.edges) : o = x ∨ o ∈ w.edges

Every arm uses old blossom incidences and its one actual external boundary port only.