Preserving a blossom through an outside prefix

Lemma 43 of [KKR18], arXiv:1602.03124v6, printed p. 20, transfers the full six-invariant DAG through a shortest externally extendible prefix. This wrapper retains the original cycle, copied-step distinctness, and its one internal defect. It imposes no agreement condition on outside comparison labels.

theorem Cslib.Logic.PL.CSP.Blossom.blossomDAG_vars_eq_internal {F : CSP Table ℕ} {w : F.Walk} (hw : w.IsWalk) (hn : w.steps ≠ []) {ts : List ℕ} (hl : ts.length = w.steps.length) (pivot : ℕ) : (DAG.blossomDAG w ts pivot).vars = (internal w).toFinset

For a nonempty linked cycle, the displayed graph support is its actual internal variables.

theorem Cslib.Logic.PL.CSP.Blossom.blossom_after_prefix {F : CSP Table ℕ} {w q : F.Walk} {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hM : EdgeInstance.EvenConstraints Table.sem F) (hq : Walk.IsFWalk Table.sem f q) (hstart : q.start ∉ internal w) (hvars : ∀ o ∈ q.edges, o.var ∉ internal w) (hno : ∀ n < q.steps.length, ∀ e ∈ w.edges, ∀ (o : F.Occurrence), o.var = (q.take n).finish → o.fst = e.fst → ¬Walk.IsFWalk Table.sem f ((q.take n).snoc o e)) : Walk.IsBlossom Table.sem (q.flip f) w

An outside prefix with no earlier feasible extension preserves the actual blossom witness. The supplied no-extension test concerns original incidences, in both DAG orientations.

def Cslib.Logic.PL.CSP.Blossom.exitsAt {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) (n : ℕ) : List (F.Occurrence × F.Occurrence)

Actual unused outside ports and cycle ports allowing an exchange at a given prefix.

theorem Cslib.Logic.PL.CSP.Blossom.mem_exitsAt {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) (n : ℕ) (o e : F.Occurrence) : (o, e) ∈ exitsAt f w r n ↔ e ∈ w.edges ∧ o.var = (r.take n).finish ∧ o.fst = e.fst ∧ o ∉ (r.take n).edges ∧ ValidLabeling Table.sem (DAG.pairFlip ((r.take n).flip f) o e)

The exit scan reads precisely actual ports and the feasible two-port exchange.

structure Cslib.Logic.PL.CSP.Blossom.Exit (F : CSP Table ℕ) : Type

Data returned by the first-exit scan; no mathematical certificate is stored in the data.

• length : ℕ

  Number of whole original steps before the attachment.

• input : F.Occurrence

  Actual outside occurrence, unused in that prefix.

• output : F.Occurrence

  Actual cycle occurrence at the same original constraint.

def Cslib.Logic.PL.CSP.Blossom.firstExit {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) : Option (Exit F)

Find the first externally extendible prefix, then its first actual pair of ports.

theorem Cslib.Logic.PL.CSP.Blossom.firstExit_spec {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) (hex : ∃ n ≤ r.steps.length, exitsAt f w r n ≠ []) : ∃ (ex : Exit F), firstExit f w r = some ex ∧ ex.length ≤ r.steps.length ∧ (ex.input, ex.output) ∈ exitsAt f w r ex.length ∧ ∀ n < ex.length, exitsAt f w r n = []

The executable prefix selection succeeds when a local exit exists and proves that every earlier prefix fails every local exit test. It scans whole steps and actual ports only.

theorem Cslib.Logic.PL.CSP.Blossom.firstExit_no_extension {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) {k : ℕ} (hk : k ≤ r.steps.length) (hno : ∀ n < k, exitsAt f w r n = []) (n : ℕ) : n < (r.take k).steps.length → ∀ e ∈ w.edges, ∀ (o : F.Occurrence), o.var = ((r.take k).take n).finish → o.fst = e.fst → ¬Walk.IsFWalk Table.sem f (((r.take k).take n).snoc o e)

The first local exit proves the exact no-earlier-extension hypothesis of Lemma 43. An f-walk extension passes the local scan, so minimality forbids every such extension.

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

Execute the shortest outside prefix and the valid original blossom arm selected after it.

theorem Cslib.Logic.PL.CSP.Blossom.liftPrefix_spec {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hM : EdgeInstance.EvenConstraints Table.sem F) {r : F.Walk} (hr : Walk.IsFPrefix Table.sem f r) (hend : r.steps = [] ∨ r.start ≠ r.finish) (hroot : Inconsistent f r.start) (hstart : r.start ∉ internal w) (hvars : ∀ o ∈ r.edges, o.var ∉ internal w) (hex : ∃ n ≤ r.steps.length, exitsAt f w r n ≠ []) : ∃ (g : F.OccurrenceLabeling Bool), liftPrefix f w r = some g ∧ ValidLabeling Table.sem g ∧ (defects g).card + 2 = (defects f).card

Constructive difficult-case lifting in Lemma 44: an outside trail from an old defect, with any feasible local exit into the blossom, yields an actual valid labeling removing two old defects. Outside changes are performed before the arm scan and are fully accounted for.