Blossoms returned by chronological forest search

The two LCA cases of [KKR18], arXiv:1602.03124v6, Section 5.3, printed pp. 11–12, and Definition 39/Lemma 41, printed pp. 19–20. The cycle, preparation, pivot, timestamps and child ports are those computed by Meeting.blossomData.

Main results

• Meeting.Trace.blossom_correct: both raw extractor branches satisfy Definition 39.
• Meeting.Trace.variable_prepare_empty: a variable LCA is an inconsistent root.
• search_blossom_correct: an actual fresh-run blossom result supplies valid preparation, a source-strength blossom, and unchanged defect count, from instance hypotheses alone.

The proof uses chronological prefix transfer as an alternative to the source's repeated graph surgery, followed by its Lemma 37 rerooting at a constraint LCA. No contraction or lifting algorithm, encoded runtime bound, or planar dichotomy is claimed here.

def Cslib.Logic.PL.CSP.Forest.Meeting.forkDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (k : ℕ) : F.DAG

The two actual ancestral suffixes and their incoming terminal meeting ports. Shared root-side copies before step k are omitted. This is the graph used in Lemma 41's preparation.

@[simp]

theorem Cslib.Logic.PL.CSP.Forest.Meeting.mem_forkDAG_arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (k : ℕ) (a : DAG.Arc F) : a ∈ (m.forkDAG k).arcs ↔ a ∈ DAG.pathArcs (m.left.walk.drop k) m.older.stamp ∨ a ∈ DAG.pathArcs (m.right.walk.drop k) m.older.stamp ∨ a = { occurrence := m.current.input, time := List.length m.older, incoming := true } ∨ a = { occurrence := m.output, time := List.length m.older, incoming := true }

Every fork arc is an actual ancestral arc or one of the two incoming meeting ports.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.fork_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (k : ℕ) : (m.forkDAG k).Subgraph m.prunedDAG ∧ (m.forkDAG k).Supported

The suffix fork is a supported subgraph of the actual terminal pruned forest.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.prepare_fork_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) (k : ℕ) (hk : 2 * k + 1 ≤ m.commonNodes.length) : DAG.IsFDAG sem ((m.left.walk.take k).flip f) (m.forkDAG k)

Flipping the shared root prefix preserves the full f-DAG invariant on the actual remaining suffix fork. Unused earlier branches are discarded, and original constraints may recur later at different timestamps.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.ancestor_constraint_length {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) : m.commonNodes.length = 2 * ((m.commonNodes.length - 1) / 2) + 2

A constraint LCA ends the shared node prefix immediately before its two children.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_first_copies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) : (DAG.inArc m.older.stamp s).copy = c ∧ (DAG.inArc m.older.stamp t).copy = c

The two steps selected by the raw constraint-LCA branch use that actual copied node.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_children_ne {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) : s.2.var ≠ t.2.var

The child ports at a constraint LCA name distinct variables. Otherwise their common child would extend the computed common-node prefix, contradicting maximality.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_fork_earliest {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) : (m.forkDAG ((m.commonNodes.length - 1) / 2)).Earliest c

The copied constraint selected as the LCA is the earliest copy of the remaining fork.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_fork_leaf {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) (a : DAG.Arc F) : a ∈ (m.forkDAG ((m.commonNodes.length - 1) / 2)).arcs → a.occurrence.var = s.1.var → a = DAG.inArc m.older.stamp s

The root-side input at a constraint LCA is a leaf of the selected suffix fork.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_fork_incoming_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (a : DAG.Arc F) : a ∈ (m.forkDAG ((m.commonNodes.length - 1) / 2)).arcs → a.incoming = true → a.copy = (DAG.inArc m.older.stamp s).copy → a = DAG.inArc m.older.stamp s

At the LCA copy, the selected forest fork has precisely its original single incoming port. The second incoming meeting port is at the strictly later terminal copy.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.reroot_constraint_fork {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) : DAG.IsFDAG sem ((m.left.walk.take ((m.commonNodes.length - 1) / 2 + 1)).flip f) ((m.forkDAG ((m.commonNodes.length - 1) / 2)).reroot (DAG.inArc m.older.stamp s) (DAG.outArc m.older.stamp s))

Source Lemma 41's constraint-LCA surgery: flip the actual root-to-left-child path, remove its root-side input, and reverse that child's LCA incidence. The full remaining fork is an f-DAG for the prepared labeling.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_cycle_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) : have k := (m.commonNodes.length - 1) / 2; have w := m.left.walk.drop (k + 1); have z := m.right.walk.drop (k + 1); DAG.IsFDAG sem ((m.left.walk.take (k + 1)).flip f) (DAG.blossomDAG (((w.snoc m.current.input m.output).append z.reverse).snoc t.2 s.2) (List.map (fun (u : F.Occurrence × F.Occurrence) => m.older.stamp u.1) w.steps ++ [List.length m.older] ++ (List.map (fun (u : F.Occurrence × F.Occurrence) => m.older.stamp u.1) z.steps).reverse ++ [c.2]) (w.steps.length + 1))

The constraint-LCA cycle, with its actual terminal and LCA timestamps, embeds into the prepared rerooted fork. This proves the complete Definition 39 graph condition.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.drop_join_isWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (k : ℕ) (hk : m.commonNodes.length < 2 * k + 2) : (((m.left.walk.drop k).snoc m.current.input m.output).append (m.right.walk.drop k).reverse).IsWalk

Past the common prefix, joining the two actual ancestral suffixes at the terminal pair gives an incidence trail. This applies to both LCA branches.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_cycle_isWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {s t : F.Occurrence × F.Occurrence} (hs : m.left.walk.steps[(m.commonNodes.length - 1) / 2]? = some s) (ht : m.right.walk.steps[(m.commonNodes.length - 1) / 2]? = some t) : have k := (m.commonNodes.length - 1) / 2; ((((m.left.walk.drop (k + 1)).snoc m.current.input m.output).append (m.right.walk.drop (k + 1)).reverse).snoc t.2 s.2).IsWalk

The constraint-LCA branch closes its joined suffixes through the two distinct, fresh LCA child incidences. No incidence is repeated by the resulting closed trail.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.constraint_blossom_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {c : DAG.Copy F} (hc : m.ancestor? = some (Sum.inr c)) {b : BlossomData F} (hb : m.blossomData = some b) : DAG.IsFDAG sem (b.prepare.flip f) (DAG.blossomDAG b.cycle b.times b.pivot)

The raw constraint-LCA extractor supplies precisely the rerooted cycle just proved to be an f-DAG, with its actual timestamps and child incidences.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_isFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {b : BlossomData F} (hb : m.blossomData = some b) : DAG.IsFDAG sem (b.prepare.flip f) (DAG.blossomDAG b.cycle b.times b.pivot)

Both LCA branches return the full timestamped f-DAG required in Definition 39, under the labeling obtained by their actual preparatory root-path flip.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.drop_join_consistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (k : ℕ) : Walk.InternallyConsistent f (((m.left.walk.drop k).snoc m.current.input m.output).append (m.right.walk.drop k).reverse).steps

Joining suffixes of actual ancestries preserves original internal consistency. Reversal is used here only for internal consistency, not for f-walk prefix validity.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_original_consistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {b : BlossomData F} (hb : m.blossomData = some b) : Walk.InternallyConsistent f b.cycle.steps

The actual cycle in either branch is internally consistent under the original labeling. Only its base can be inconsistent after preparation.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_cycle_isWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) {b : BlossomData F} (hb : m.blossomData = some b) : b.cycle.IsWalk

Both actual LCA cycles are closed incidence trails, including the final pair of fresh LCA child ports in the copied-constraint branch.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.blossom_prepare_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {m : Meeting F} {b : BlossomData F} (hb : m.blossomData = some b) : ∃ (n : ℕ), b.prepare = m.left.walk.take n

Every returned preparatory walk is an actual prefix of the left root ancestry.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.blossom_prepare_finish {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {m : Meeting F} {b : BlossomData F} (hb : m.blossomData = some b) : b.prepare.finish = b.cycle.start

The preparatory root path ends at the base of the actual returned cycle.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.blossom_metadata {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {m : Meeting F} {b : BlossomData F} (hb : m.blossomData = some b) : b.times.length = b.cycle.steps.length ∧ 0 < b.pivot ∧ b.pivot ≤ b.cycle.steps.length

Timestamp and pivot metadata from either extractor branch have exactly the lengths needed for its two-arm cycle, and the terminal meeting step is present.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_times_nodup {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {b : BlossomData F} (hb : m.blossomData = some b) : b.times.Nodup

Actual extractor timestamps distinguish every copied cycle step in both LCA branches. The cross-arm distinction follows from the ancestry common-prefix theorem. Original constraints may still occur repeatedly, at different timestamps.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_prepare_isWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {b : BlossomData F} (hb : m.blossomData = some b) : b.prepare.IsWalk ∧ Inconsistent f b.prepare.start

The returned preparatory path is a trail from an originally inconsistent root.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.variable_prepare_empty {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) {v : V} (ha : m.ancestor? = some (Sum.inl v)) : (m.left.walk.take ((m.commonNodes.length - 1) / 2)).steps = []

A variable LCA of an actual terminal event is a root. Its returned preparatory path is therefore empty, as specified in source Section 5.3.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_prepare_finish_consistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) {b : BlossomData F} (hb : m.blossomData = some b) (hn : b.prepare.steps ≠ []) : ¬Inconsistent f b.prepare.finish

A nonempty preparatory path ends at an originally consistent discovered variable.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_base_inconsistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) {b : BlossomData F} (hb : m.blossomData = some b) : Inconsistent (b.prepare.flip f) b.cycle.start

Preparation moves the original root defect to the actual cycle base.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_prepare_card_defects {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) {b : BlossomData F} (hb : m.blossomData = some b) : (defects (b.prepare.flip f)).card = (defects f).card

Preparatory root-path flipping preserves the number of defects. This is the counting interface needed before contracting the returned blossom.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_correct {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {b : BlossomData F} (hb : m.blossomData = some b) : Walk.IsBlossom sem (b.prepare.flip f) b.cycle

Source Lemma 41, arXiv:1602.03124v6, printed pp. 19–20: the actual returned cycle is a Definition 39 blossom after the actual preparatory path is flipped. The alternative proof transfers the later fork through chronological prefix flips, then uses Lemma 37 rerooting at a constraint LCA. No correctness premise is added to the raw extractor.

theorem Cslib.Logic.PL.CSP.Forest.search_blossom_correct {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {m : Meeting F} (hr : search sem f = Result.blossom m) : ∃ (b : BlossomData F), m.blossomData = some b ∧ Walk.IsBlossom sem (b.prepare.flip f) b.cycle ∧ ValidLabeling sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card

Fresh-run blossom correctness, including source-strength cycle validity, validity of the preparatory labeling, and preservation of its defect count. The only search premise is the actual result equation; all forest and event invariants are derived from the run.