Correctness of chronological forest events

Terminal events of Algorithm 1 of [KKR18], arXiv:1602.03124v6. Paths and copied constraints are the actual parent reconstructions of the executable search.

Main results

• search_augment_correct: a returned augmentation is an augmenting f-walk; its flip is valid and removes exactly two defects (Proposition 38, printed p. 18).
• Meeting.Trace.variable_blossom_isFDAG: the variable-LCA cycle's full graph certificate.

The constraint-LCA case and complete fresh-run blossom endpoint are proved in CslibFrontier/Algorithms/Lean/EdgeCSP/Forest/Blossom.lean.

theorem Cslib.Logic.PL.CSP.Forest.Log.incoming_time_unique {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {es : Log F} {a b : DAG.Arc F} (ha : a ∈ es.arcs) (hb : b ∈ es.arcs) (hai : a.incoming = true) (hbi : b.incoming = true) (ht : a.time = b.time) : a = b

A timestamp in a chronological log has only its single recorded incoming port.

theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_cons_old {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {es : Log F} {e : Expansion F} {rs : List V} {v : V} (hf : ∀ o ∈ e.outputs, ¬Visited rs es o.var) (hv : Visited rs es v) : ancestry (e :: es) v = es.ancestry v

Appending fresh children leaves every older visited variable's ancestry unchanged.

theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_times_pairwise {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (es.ancestry v).times

Actual ancestry timestamps strictly increase, without any condition on variable names.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_times_eq_stamp {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) (v : V) : (es.ancestry v).times = List.map (fun (s : F.Occurrence × F.Occurrence) => es.stamp s.1) (es.ancestry v).walk.steps

Recorded ancestry timestamps agree with the executable incoming-port lookup.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_chronological {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) (v : V) : List.Pairwise (fun (s t : F.Occurrence × F.Occurrence) => es.stamp s.1 < es.stamp t.1) (es.ancestry v).walk.steps

Ancestral steps are chronological with respect to their actual incoming timestamps.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_nodes {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) (v : V) : (es.ancestry v).nodes = Sum.inl (es.ancestry v).walk.start :: List.flatMap (fun (s : F.Occurrence × F.Occurrence) => [Sum.inr (DAG.inArc es.stamp s).copy, Sum.inl s.2.var]) (es.ancestry v).walk.steps

Ancestor nodes carry precisely the copied constraints certified by the incoming arcs.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_step_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {v : V} {s : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry v).walk.steps) : (es.ancestry s.1.var).walk.start = (es.ancestry v).walk.start ∧ (es.ancestry s.1.var).walk.steps ++ [s] <+: (es.ancestry v).walk.steps

The path to a step's input is the exact ancestral prefix before that step. This uses actual parent reconstruction, including across copies of the same original constraint.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_step_nodes_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {v : V} {s : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry v).walk.steps) : (es.ancestry s.1.var).nodes ++ [Sum.inr (DAG.inArc es.stamp s).copy] <+: (es.ancestry v).nodes

Before any ancestral copied constraint, its input's entire root path is shared.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_step_full_nodes_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {v : V} {s : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry v).walk.steps) : (es.ancestry s.1.var).nodes ++ [Sum.inr (DAG.inArc es.stamp s).copy, Sum.inl s.2.var] <+: (es.ancestry v).nodes

The full node prefix through any ancestral step is determined by its input's ancestry.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_step_prefix_length {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {v : V} {k : ℕ} {s : F.Occurrence × F.Occurrence} (hs : s ∈ List.drop k (es.ancestry v).walk.steps) : k ≤ (es.ancestry s.1.var).walk.steps.length

A step remaining after dropping k steps cannot have a shorter root-side parent path.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_shared_copy_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {u v : V} {s t : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry u).walk.steps) (ht : t ∈ (es.ancestry v).walk.steps) (hc : (DAG.inArc es.stamp s).copy = (DAG.inArc es.stamp t).copy) : (es.ancestry s.1.var).nodes ++ [Sum.inr (DAG.inArc es.stamp s).copy] <+: (es.ancestry u).nodes ∧ (es.ancestry s.1.var).nodes ++ [Sum.inr (DAG.inArc es.stamp s).copy] <+: (es.ancestry v).nodes

Paths sharing a copied constraint share its whole root-side node prefix.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_root_eq_of_copy {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {u v : V} {s t : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry u).walk.steps) (ht : t ∈ (es.ancestry v).walk.steps) (hc : (DAG.inArc es.stamp s).copy = (DAG.inArc es.stamp t).copy) : (es.ancestry u).walk.start = (es.ancestry v).walk.start

An ancestral copied constraint belongs to just one rooted tree. Repeated original constraints at different timestamps are not identified.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_disjoint_copies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {rs : List V} {es : Log F} (hg : Grown sem f rs es) {u v : V} (hu : Log.Visited rs es u) (hv : Log.Visited rs es v) (hne : (es.ancestry u).walk.start ≠ (es.ancestry v).walk.start) : Disjoint (DAG.pathDAG (es.ancestry u).walk es.stamp).copies (DAG.pathDAG (es.ancestry v).walk es.stamp).copies

Ancestries from different rooted trees have disjoint copied-constraint supports.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_output_consistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {es : Log F} (hg : Grown sem f (roots f) es) (v : V) {s : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry v).walk.steps) : ¬Inconsistent f s.2.var

Every output variable of a reconstructed ancestry is consistent in the reference labeling. Inconsistent variables are roots, never discovered children.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_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} {es : Log F} (hg : Grown sem f (roots f) es) {v : V} (hne : (es.ancestry v).walk.steps ≠ []) : ¬Inconsistent f v

A nonempty ancestry ends at a discovered, hence consistent, variable.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_isFPrefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {es : Log F} (hg : Grown sem f (roots f) es) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {v : V} (hv : Log.Visited (roots f) es v) : Walk.IsFPrefix sem f (es.ancestry v).walk

All ancestral prefixes have the source's internal-consistency and validity properties, including the empty path at an inconsistent root.

theorem Cslib.Logic.PL.CSP.Forest.Ancestry.nodes_last_variable {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (p : Ancestry F) : ∃ (v : V), p.nodes.getLast? = some (Sum.inl v)

Every reconstructed node list ends at a variable, including the length-zero ancestry.

theorem Cslib.Logic.PL.CSP.Forest.Ancestry.nodes_length {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (p : Ancestry F) (hl : p.times.length = p.walk.steps.length) : p.nodes.length = 2 * p.walk.steps.length + 1

A correctly stamped ancestry has one variable node and two nodes per step.

theorem Cslib.Logic.PL.CSP.Forest.Ancestry.nodes_getElem?_even {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (p : Ancestry F) (hl : p.times.length = p.walk.steps.length) (k : ℕ) (hk : k ≤ p.walk.steps.length) : p.nodes[2 * k]? = some (Sum.inl (p.walk.take k).finish)

Even node indices are exactly the endpoints of the corresponding walk prefixes.

theorem Cslib.Logic.PL.CSP.Forest.Ancestry.nodes_getElem?_odd {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (p : Ancestry F) (hl : p.times.length = p.walk.steps.length) (k : ℕ) (hk : k < p.walk.steps.length) : p.nodes[2 * k + 1]? = some (Sum.inr (p.walk.steps[k].1.fst, p.times[k]))

Odd node indices are exactly the timestamped constraints of the corresponding steps.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.commonNodes_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : m.commonNodes <+: m.left.nodes ∧ m.commonNodes <+: m.right.nodes

The executable common-node list is a prefix of both actual ancestral node lists.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.commonNodes_maximal {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (ps : List (DAG.Node F)) (hl : ps <+: m.left.nodes) (hr : ps <+: m.right.nodes) : ps.length ≤ m.commonNodes.length

Every common node prefix is contained in the prefix selected by the extractor.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.shared_copy_common_length {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) {s t : F.Occurrence × F.Occurrence} (hs : s ∈ m.left.walk.steps) (ht : t ∈ m.right.walk.steps) (hc : (DAG.inArc m.older.stamp s).copy = (DAG.inArc m.older.stamp t).copy) : 2 * (m.older.ancestry s.1.var).walk.steps.length + 2 ≤ m.commonNodes.length

A copied constraint shared by the two ancestries lies inside their computed common prefix, with its complete root path.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.commonNodes_ne_nil {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (he : m.left.walk.start = m.right.walk.start) : m.commonNodes ≠ []

A common root always supplies at least one common node.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.commonNodes_getElem? {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) {i : ℕ} (hi : i < m.commonNodes.length) : m.left.nodes[i]? = m.right.nodes[i]?

Every index inside the common prefix names the same actual node on both paths.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.common_times_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (k : ℕ) (hk : 2 * k + 1 ≤ m.commonNodes.length) : List.take k m.left.times = List.take k m.right.times

Whole shared steps carry the same timestamp prefix on both ancestries.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.prefix_time_lt_right_drop {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 : ℕ) (hk : 2 * k + 1 ≤ m.commonNodes.length) {s t : F.Occurrence × F.Occurrence} (hs : s ∈ List.take k m.left.walk.steps) (ht : t ∈ List.drop k m.right.walk.steps) : m.older.stamp s.1 < m.older.stamp t.1

A shared root prefix predates every step on the remaining right arm.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.ancestor_at_common_index {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) {a : DAG.Node F} (ha : m.ancestor? = some a) : m.left.nodes[m.commonNodes.length - 1]? = some a ∧ m.right.nodes[m.commonNodes.length - 1]? = some a

The selected ancestor occurs at the final shared index on each ancestral node list.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.ancestor?_isSome {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (he : m.left.walk.start = m.right.walk.start) : m.ancestor?.isSome = true

The common-node computation finds an ancestor whenever the two roots agree.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.ancestor_constraint_index_lt {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 - 1) / 2 < m.left.walk.steps.length ∧ (m.commonNodes.length - 1) / 2 < m.right.walk.steps.length

A copied-constraint ancestor occurs before a step on each path. The Option branches in the raw extractor cannot fail on that case, even for timestamp zero.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.ancestor_variable_length {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) {v : V} (hv : m.ancestor? = some (Sum.inl v)) : m.commonNodes.length = 2 * ((m.commonNodes.length - 1) / 2) + 1

A variable LCA is the last node of a whole-step common prefix.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.ancestor_variable_prefix {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) {v : V} (hv : m.ancestor? = some (Sum.inl v)) : (m.left.walk.take ((m.commonNodes.length - 1) / 2)).finish = v ∧ (m.right.walk.take ((m.commonNodes.length - 1) / 2)).finish = v

A variable ancestor is the actual endpoint of both shared walk prefixes.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.left_drop_disjoint_right {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 : ℕ) (hk : m.commonNodes.length < 2 * k + 2) : Disjoint (DAG.pathDAG (m.left.walk.drop k) m.older.stamp).copies (DAG.pathDAG m.right.walk m.older.stamp).copies

Past the last common copied node, the left ancestry shares no copied constraint with the right ancestry. This is derived from exact parent prefixes, not assumed as an event-correctness premise.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.blossomData_isSome {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) (he : m.left.walk.start = m.right.walk.start) : m.blossomData.isSome = true

At a same-root event the actual raw extractor returns cycle data; neither LCA case is lost through an absent ancestor or an out-of-bounds child port.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.older_subgraph_pruned {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) : (Log.toDAG m.roots m.older).Subgraph m.prunedDAG

The older forest survives terminal pruning as a supported subgraph.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.left_directed {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) : m.prunedDAG.DirectedPath m.left.walk m.older.stamp

The actual left ancestral path remains directed after terminal pruning.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.right_directed {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) : m.prunedDAG.DirectedPath m.right.walk m.older.stamp

The actual right ancestral path remains directed after terminal pruning.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.copy_fresh {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) {v : V} (hv : Log.Visited m.roots m.older v) : m.copy ∉ (DAG.pathDAG (m.older.ancestry v).walk m.older.stamp).copies

The new terminal copy is absent from every older ancestry, including timestamp zero.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.augment_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} {m : Meeting F} (h : Trace sem f m) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) (hne : m.left.walk.start ≠ m.right.walk.start) (n : ℕ) : ValidLabeling sem ((m.walk.take n).flip f)

Both ancestral paths and the terminal pair give valid flips at every prefix of the actual returned augmentation walk. Reversed prefixes are justified by directed suffixes.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.augment_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) (hne : m.left.walk.start ≠ m.right.walk.start) : m.walk.IsWalk

The candidate from two different rooted trees is an actual incidence trail.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.augment_isAugmenting {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) (hne : m.left.walk.start ≠ m.right.walk.start) : Walk.IsAugmenting sem f m.walk

Source Proposition 38 at the walk level: the returned candidate is an augmenting f-walk, including internal consistency and validity after every prefix.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_prepare_valid {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) : ValidLabeling sem (b.prepare.flip f)

Every preparatory root-path flip actually returned by the cycle extractor is valid. This is the preparatory-labeling assertion of source Lemma 41; the remaining blossom assertion additionally requires the closed cycle's complete f-DAG certificate.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.blossom_cycle_closed {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.cycle.finish = b.cycle.start

The cycle returned by either actual LCA branch is closed at its recorded base.

theorem Cslib.Logic.PL.CSP.Forest.Meeting.Trace.variable_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) {base : V} (ha : m.ancestor? = some (Sum.inl base)) {b : BlossomData F} (hb : m.blossomData = some b) : DAG.IsFDAG sem (b.prepare.flip f) (DAG.blossomDAG b.cycle b.times b.pivot)

In the variable-LCA branch, the cycle's actual timestamped graph is an f-DAG after the returned preparatory flip. Both feasibility and no shortcuts are preserved.

def Cslib.Logic.PL.CSP.Forest.Result.Classified {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] : Result F → Prop

Agreement of a terminal tag with the two reconstructed roots.

theorem Cslib.Logic.PL.CSP.Forest.run_event_roots {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (rs : List V) (es : Log F) (remaining : List F.Occurrence) : (run sem f rs es remaining).Classified

The executable event tag records exactly whether the two ancestries have the same root.

theorem Cslib.Logic.PL.CSP.Forest.search_augment_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.augment m) : Walk.IsAugmenting sem f m.walk ∧ ValidLabeling sem (m.walk.flip f) ∧ (defects (m.walk.flip f)).card + 2 = (defects f).card

Source Proposition 38 for a fresh executable run: an actual returned augmentation is an augmenting f-walk and its flip is valid and removes exactly two defects.