Blossoms with their full timestamped DAG certificate

Definition 39 of [KKR18], arXiv:1602.03124v6, printed p. 19. The closed incidence trail has one inconsistent base and consistent internal variables. Its timestamped graph consists of the forward initial arm and the reversed final arm, meeting at the copied constraint of step pivot. That constraint has two incoming ports. Every step retains a distinct copied constraint, including between the two arms. This makes explicit the two-arm geometry used by Lemma 40 when it invokes Corollary 36: the graph union alone can hide a shared four-port copy. Original constraints may recur at different times. The graph must satisfy every condition of DAG.IsFDAG, including no shortcuts; validity of the final or proper-prefix flip alone is not a blossom certificate.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.incoming_eq_of_parent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} (h : IsFDAG sem f T) (hF : F.EdgeInstance) {p a b : Arc F} (hp : p ∈ T.arcs) (ha : a ∈ T.arcs) (hb : b ∈ T.arcs) (hpo : p.incoming = false) (hai : a.incoming = true) (hbi : b.incoming = true) (hap : a.occurrence.var = p.occurrence.var) (hbp : b.occurrence.var = p.occurrence.var) : a = b

A variable that already has a parent cannot branch toward two different copies in an edge-instance DAG: its two original incidences are the parent port and one outgoing port.

def Cslib.Logic.PL.CSP.DAG.blossomArcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : List (F.Occurrence × F.Occurrence) → List ℕ → ℕ → List (Arc F)

The source's two arms of a cycle. The one-based pivot is the common terminal copied constraint; before it, steps run forward, and after it, steps run backward.

def Cslib.Logic.PL.CSP.DAG.blossomDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (times : List ℕ) (pivot : ℕ) : F.DAG

The full incidence DAG in Definition 39, retaining the cycle's base as a supported variable. Timestamps are attached to steps, so repeated original constraints remain distinct.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_supported {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (times : List ℕ) (pivot : ℕ) : (blossomDAG w times pivot).Supported

The cycle graph supports every generated incidence and its actual endpoints.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_time_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {ss : List (F.Occurrence × F.Occurrence)} {ts : List ℕ} {pivot : ℕ} {a : Arc F} (ha : a ∈ blossomArcs ss ts pivot) : a.time ∈ ts

Every generated arc uses one of the supplied step timestamps.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_copy_time_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (times : List ℕ) (pivot : ℕ) {c : Copy F} (hc : c ∈ (blossomDAG w times pivot).copies) : c.2 ∈ times

Every copied constraint in the cycle graph retains its supplied timestamp.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_append_after {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (ss : List (F.Occurrence × F.Occurrence)) (ts : List ℕ) (pivot : ℕ) (hl : ts.length = ss.length) (hp : pivot ≤ ss.length) (s : F.Occurrence × F.Occurrence) (t : ℕ) : blossomArcs (ss ++ [s]) (ts ++ [t]) pivot = blossomArcs ss ts pivot ++ [{ occurrence := s.1, time := t, incoming := false }, { occurrence := s.2, time := t, incoming := true }]

Once the pivot has been passed, appending a cycle step adds a backward-oriented pair.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_subgraph_of_arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (times : List ℕ) (pivot : ℕ) {T : F.DAG} (hbase : w.start ∈ T.vars) (hs : T.Supported) (ha : ∀ a ∈ blossomArcs w.steps times pivot, a ∈ T.arcs) : (blossomDAG w times pivot).Subgraph T

A computed cycle graph is a subgraph whenever its base and all its actual arcs are supported by the ambient graph. Copied-node support is inherited from those arcs.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_meeting_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (timeW timeZ : F.Occurrence → ℕ) (ss zs : List (F.Occurrence × F.Occurrence)) (a b : F.Occurrence) (t : ℕ) {e : Arc F} (he : e ∈ blossomArcs (ss ++ (a, b) :: List.map Prod.swap zs.reverse) (List.map (fun (s : F.Occurrence × F.Occurrence) => timeW s.1) ss ++ t :: (List.map (fun (s : F.Occurrence × F.Occurrence) => timeZ s.1) zs).reverse) (ss.length + 1)) : (∃ s ∈ ss, e = inArc timeW s ∨ e = outArc timeW s) ∨ e = { occurrence := a, time := t, incoming := true } ∨ e = { occurrence := b, time := t, incoming := true } ∨ ∃ s ∈ zs, e = inArc timeZ s ∨ e = outArc timeZ s

Every cycle arc comes from one of its two directed arms or the terminal incoming pair.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_subgraph_meeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {T : F.DAG} {w z : F.Walk} {timeW timeZ : F.Occurrence → ℕ} {a b : F.Occurrence} {t : ℕ} (hw : T.DirectedPath w timeW) (hz : T.DirectedPath z timeZ) (hs : T.Supported) (ha : { occurrence := a, time := t, incoming := true } ∈ T.arcs) (hb : { occurrence := b, time := t, incoming := true } ∈ T.arcs) : (blossomDAG ((w.snoc a b).append z.reverse) (List.map (fun (s : F.Occurrence × F.Occurrence) => timeW s.1) w.steps ++ [t] ++ (List.map (fun (s : F.Occurrence × F.Occurrence) => timeZ s.1) z.steps).reverse) (w.steps.length + 1)).Subgraph T

Two directed arms and their incoming meeting ports embed the computed cycle graph in the ambient DAG. The closed-trail and consistency requirements of a blossom are separate.

def Cslib.Logic.PL.CSP.Walk.copies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (times : List ℕ) : List (DAG.Copy F)

Original constraint positions paired with the supplied timestamps, one per cycle step. The two incidences of the meeting step refer to the same copy and are counted only once.

def Cslib.Logic.PL.CSP.Walk.DistinctCopies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (times : List ℕ) : Prop

Every cycle step has a timestamp and uses its own copied constraint node. Repeated original constraints are allowed at different times. This excludes a four-port shared copy hidden by taking the union of the two arms in DAG.blossomDAG.

theorem Cslib.Logic.PL.CSP.Walk.distinctCopies_of_nodup_times {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) {times : List ℕ} (hl : times.length = w.steps.length) (hn : times.Nodup) : w.DistinctCopies times

Distinct timestamps give distinct copied steps, independently of original constraint repetitions. Length equality prevents the zip from discarding steps.

def Cslib.Logic.PL.CSP.Walk.IsBlossom {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (w : F.Walk) : Prop

An f-blossom following source Definition 39, retaining distinct copied steps. Witnesses specify the copied constraints and terminal meeting, rather than assuming an event-correctness oracle.