Actual ports and timestamps of blossom arms

The displayed arms of Definition 39 of [KKR18], arXiv:1602.03124v6, printed p. 19, retain their actual original incidences and copied-step timestamps. The finite clock lookup below reads the supplied arc list; no graph or labeling oracle is introduced.

theorem Cslib.Logic.PL.CSP.Walk.IsBlossom.steps_ne_nil {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} (h : IsBlossom sem f w) : w.steps ≠ []

A source-strength blossom has an actual nonempty cycle.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.start_mem_vars {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (hw : w.IsWalk) (hn : w.steps ≠ []) : w.start ∈ List.map Occurrence.var w.edges

A nonempty linked trail uses an actual occurrence of its starting variable.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_map_occurrence {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) : List.map Arc.occurrence (blossomArcs ss ts pivot) = Walk.edgesOf ss

Forgetting orientations and timestamps gives exactly the original incidence list.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_get_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {ss : List (F.Occurrence × F.Occurrence)} {ts : List ℕ} (hl : ts.length = ss.length) (pivot j : ℕ) (hj : j < ss.length) : match ss[j] with | (input, output) => have stamp := ts[j]; { occurrence := input, time := stamp, incoming := decide (j < pivot) } ∈ blossomArcs ss ts pivot ∧ { occurrence := output, time := stamp, incoming := decide (pivot ≤ j + 1) } ∈ blossomArcs ss ts pivot

Both actual ports of a cycle step appear at its supplied timestamp and orientation.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {ss : List (F.Occurrence × F.Occurrence)} {ts : List ℕ} (hl : ts.length = ss.length) {pivot : ℕ} {a : Arc F} (ha : a ∈ blossomArcs ss ts pivot) : ∃ (j : ℕ) (hj : j < ss.length), match ss[j] with | (input, output) => have stamp := ts[j]; a = { occurrence := input, time := stamp, incoming := decide (j < pivot) } ∨ a = { occurrence := output, time := stamp, incoming := decide (pivot ≤ j + 1) }

Every actual blossom arc is one of the two supplied ports of a particular cycle step.

def Cslib.Logic.PL.CSP.DAG.blossomTime {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (times : List ℕ) (pivot : ℕ) (o : F.Occurrence) : ℕ

A finite lookup of the timestamp at an actual blossom incidence.

theorem Cslib.Logic.PL.CSP.DAG.blossomTime_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} {times : List ℕ} {pivot : ℕ} (h : IsFDAG sem f (blossomDAG w times pivot)) {a : Arc F} (ha : a ∈ blossomArcs w.steps times pivot) : blossomTime w times pivot a.occurrence = a.time

Incidence uniqueness makes the finite lookup agree with every actual certified arc.

theorem Cslib.Logic.PL.CSP.Walk.getElem_copies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) {ts : List ℕ} (hl : ts.length = w.steps.length) (j : ℕ) (hj : j < w.steps.length) : match w.steps[j] with | (input, snd) => (w.copies ts)[j] = (input.fst, ts[j])

The copied-step list retains the exact original constraint and supplied timestamp.

theorem Cslib.Logic.PL.CSP.Walk.DistinctCopies.index_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} {ts : List ℕ} (h : w.DistinctCopies ts) {i j : ℕ} (hi : i < w.steps.length) (hj : j < w.steps.length) (he : match w.steps[i] with | (firstInput, snd) => match w.steps[j] with | (secondInput, snd) => (firstInput.fst, ts[i]) = (secondInput.fst, ts[j])) : i = j

Equal copied nodes identify the actual cycle step, including repeated original constraints.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_copy {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (hw : w.IsWalk) (hd : w.DistinctCopies ts) {j : ℕ} (hj : j < w.steps.length) {e : Arc F} (he : e ∈ blossomArcs w.steps ts pivot) (hc : match w.steps[j] with | (input, snd) => e.copy = (input.fst, ts[j])) : e = { occurrence := w.steps[j].1, time := ts[j], incoming := decide (j < pivot) } ∨ e = { occurrence := w.steps[j].2, time := ts[j], incoming := decide (pivot ≤ j + 1) }

At a specified copied cycle step there are exactly its two original incidences.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_pairedCopies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (hw : w.IsWalk) (hd : w.DistinctCopies ts) : (blossomDAG w ts pivot).PairedCopies

Distinct copied steps give the two-arc hypothesis needed by Corollary 36 and Lemma 40. The terminal meeting contributes two incoming arcs at its own single copy.

theorem Cslib.Logic.PL.CSP.Walk.copies_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (ts : List ℕ) (n : ℕ) : (w.take n).copies (List.take n ts) = List.take n (w.copies ts)

Taking whole steps takes exactly the corresponding prefix of copied nodes.

theorem Cslib.Logic.PL.CSP.Walk.copies_drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (ts : List ℕ) (n : ℕ) : (w.drop n).copies (List.drop n ts) = List.drop n (w.copies ts)

Suffixes retain exactly the supplied suffix of copied nodes.

theorem Cslib.Logic.PL.CSP.Walk.DistinctCopies.take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} {ts : List ℕ} (h : w.DistinctCopies ts) (n : ℕ) : (w.take n).DistinctCopies (List.take n ts)

Copied-node distinctness is inherited by every variable-ended prefix.

theorem Cslib.Logic.PL.CSP.Walk.DistinctCopies.drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} {ts : List ℕ} (h : w.DistinctCopies ts) (n : ℕ) : (w.drop n).DistinctCopies (List.drop n ts)

Copied-node distinctness is inherited by every variable-ended suffix.

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

Prefixes retain their actual arc orientations, including a terminal two-input meeting.

theorem Cslib.Logic.PL.CSP.DAG.blossomArcs_drop_subset {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (ss : List (F.Occurrence × F.Occurrence)) (ts : List ℕ) (pivot n : ℕ) (a : Arc F) : a ∈ blossomArcs (List.drop n ss) (List.drop n ts) (pivot - n) → a ∈ blossomArcs ss ts pivot

Dropping whole steps retains actual arcs, with the meeting index shifted by their count.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_copies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} {ts : List ℕ} (hw : w.IsWalk) (hl : ts.length = w.steps.length) (pivot : ℕ) : (blossomDAG w ts pivot).copies = (w.copies ts).toFinset

A blossom graph's copied nodes are exactly the supplied copied steps.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_copy_not_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} {ts : List ℕ} (hw : w.IsWalk) (hd : w.DistinctCopies ts) (pivot j : ℕ) (hj : j < w.steps.length) : match w.steps[j] with | (input, snd) => (input.fst, ts[j]) ∉ (blossomDAG (w.take j) (List.take j ts) pivot).copies

The boundary step's copy is absent from every preceding whole step.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_copy_not_drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} {ts : List ℕ} (hw : w.IsWalk) (hd : w.DistinctCopies ts) (pivot j : ℕ) (hj : j < w.steps.length) : match w.steps[j] with | (input, snd) => (input.fst, ts[j]) ∉ (blossomDAG (w.drop (j + 1)) (List.drop (j + 1) ts) pivot).copies

The boundary step's copy is absent from every following whole step.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_vars {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (ts : List ℕ) (pivot : ℕ) (hl : ts.length = w.steps.length) : (blossomDAG w ts pivot).vars = insert w.start (List.map Occurrence.var w.edges).toFinset

The support of the displayed blossom is exactly its base and actual used variables.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_take_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (hs : (blossomDAG w ts pivot).Supported) (n : ℕ) : (blossomDAG (w.take n) (List.take n ts) pivot).Subgraph (blossomDAG w ts pivot)

Each variable-ended prefix is a supported subgraph with its actual copied steps.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_drop_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (hl : ts.length = w.steps.length) (hs : (blossomDAG w ts pivot).Supported) (n : ℕ) : (blossomDAG (w.drop n) (List.drop n ts) (pivot - n)).Subgraph (blossomDAG w ts pivot)

Each variable-ended suffix is a supported subgraph, with its meeting index shifted.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_occurrences {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (ts : List ℕ) (pivot : ℕ) (hl : ts.length = w.steps.length) : Finset.image Arc.occurrence (blossomDAG w ts pivot).arcs = w.edges.toFinset

Forgetting timestamps in a blossom graph gives exactly the original used incidences.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_flip {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (ts : List ℕ) (pivot : ℕ) (hl : ts.length = w.steps.length) (f : F.OccurrenceLabeling Bool) : (blossomDAG w ts pivot).flip f = w.flip f

Forgetting timestamps in a blossom graph gives the actual incidence flip.

theorem Cslib.Logic.PL.CSP.DAG.blossomDAG_valid_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {w : F.Walk} {ts : List ℕ} {pivot : ℕ} (h : IsFDAG sem f (blossomDAG w ts pivot)) (hw : w.IsWalk) (hd : w.DistinctCopies ts) (hM : EdgeInstance.EvenConstraints sem F) (n : ℕ) : ValidLabeling sem ((w.take n).flip f)

Lemma 40 for all variable-ended prefixes, derived from the full six-invariant DAG and distinct actual copied steps. Repeated original constraints and odd local parity are allowed.