Preparing a later f-DAG by an earlier directed path

The earlier-copy surgery in Lemma 35 of [KKR18], arXiv v6, printed pp. 16–17, transfers validity, feasibility, and no shortcuts to a supported subgraph whose copied constraints all have later timestamps. This form permits unused earlier branches to be discarded while preparing a blossom root path.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.occurrence_not_mem_of_earlier {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (h : IsFDAG sem f T) {a : Arc F} (ha : a ∈ T.arcs) (ht : ∀ s ∈ w.steps, a.time < time s.1) : a.occurrence ∉ w.edges

An incidence already used at an earlier timestamp cannot occur on a later directed path, by the ambient DAG's original-incidence uniqueness condition.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.rank_lt_output {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (hsup : T.Supported) {rank : Node F → ℕ} (hr : ∀ (x y : Node F), T.edge x y → rank x < rank y) {s : F.Occurrence × F.Occurrence} (hs : s ∈ w.steps) : rank (Sum.inl w.start) < rank (Sum.inl s.2.var)

Along a directed path, every output variable lies strictly after the starting root in any topological ranking of the ambient graph.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.finish_ne_start {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (h : IsFDAG sem f T) (hne : w.steps ≠ []) : w.finish ≠ w.start

A nonempty directed path in an f-DAG cannot return to its starting variable.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.start_arc_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (h : IsFDAG sem f T) {first : F.Occurrence × F.Occurrence} {tail : List (F.Occurrence × F.Occurrence)} (he : w.steps = first :: tail) {a : Arc F} (ha : a ∈ pathArcs w time) (hv : a.occurrence.var = w.start) : a = inArc time first

In the arc graph of a nonempty directed path, the first incoming incidence is the only arc incident with its starting variable. This is the leaf condition used in root surgery.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.flip_later_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {S T : F.DAG} (h : IsFDAG sem f T) (hM : EdgeInstance.EvenConstraints sem F) {a b : Arc F} (ha : a ∈ T.arcs) (hb : b ∈ T.arcs) (hai : a.incoming = true) (hbo : b.incoming = false) (hc : a.copy = b.copy) (hst : S.Subgraph T) (hs : S.Supported) (hl : ∀ c ∈ S.copies, a.time < c.2) : IsFDAG sem (pairFlip f a.occurrence b.occurrence) S

Flipping an earlier pair preserves all six f-DAG conditions on any supported later subgraph. This is a deletion form of Lemma 35, retaining isolated supported nodes.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.flip_later_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {S T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (h : IsFDAG sem f T) (hM : EdgeInstance.EvenConstraints sem F) (ho : List.Pairwise (fun (s t : F.Occurrence × F.Occurrence) => time s.1 < time t.1) w.steps) (hst : S.Subgraph T) (hs : S.Supported) (hl : ∀ c ∈ S.copies, ∀ s ∈ w.steps, time s.1 < c.2) : IsFDAG sem (w.flip f) S

Flipping a chronological directed path preserves the full f-DAG invariant on any supported subgraph strictly later than every step of the path. Original constraints may repeat; strict chronology concerns copied constraints.