Directed f-DAG paths and positional walks

Corollary 36 of [KKR18], arXiv v6, printed p. 17, is connected to the existing Walk representation. A directed path certificate supplies actual indexed arcs and excludes repeated copied constraint nodes. Original constraint positions may recur at different timestamps. Its proper prefixes inherit the same graph certificate, so all variable-ended prefix flips are proved valid. Endpoint inequality and internal consistency are explicit additional hypotheses for Walk.IsFWalk; neither is part of Definition 32.

For the two meeting paths in part (1), take their variable-ended portions as w,z and their final incoming arcs as a,b. valid_flip_meeting proves validity of the union incidence flip. Its graph argument is stronger: only disjointness of copied constraint supports and freshness of the terminal copy are needed, with at least one incoming terminal arc. No claim about prefix validity under arbitrary path reversal is made.

Main results

• DirectedPath.valid_flip, DirectedPath.valid_take: path and prefix flip validity.
• DirectedPath.isFWalk: the bridge with endpoint and internal-consistency hypotheses explicit.
• DirectedPath.valid_flip_meeting: the two-path incidence flip of Corollary 36(1).

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

Stamp the incoming incidence of one positional walk step.

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

Stamp the outgoing incidence at the same copied constraint as the step's incoming port.

def Cslib.Logic.PL.CSP.DAG.pathArcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (time : F.Occurrence → ℕ) : Finset (Arc F)

The directed arcs traversed by a stamped positional walk.

def Cslib.Logic.PL.CSP.DAG.pathDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (time : F.Occurrence → ℕ) : F.DAG

The finite incidence graph of a stamped path, retaining its length-zero starting root.

structure Cslib.Logic.PL.CSP.DAG.DirectedPath {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) (w : F.Walk) (time : F.Occurrence → ℕ) : Prop

A directed incidence path certificate. Copied nodes do not recur; original constraints can. No validity or surgery conclusion is assumed. The path's existing IsWalk records positional adjacency and nonreuse of original incidences.

• walk : w.IsWalk

  The underlying sequence is a linked incidence trail.

• start_mem : w.start ∈ T.vars

  The initial variable belongs to the graph, also when the path has length zero.

• incoming (s : F.Occurrence × F.Occurrence) : s ∈ w.steps → inArc time s ∈ T.arcs

  Each step's first port is an incoming graph arc.

• outgoing (s : F.Occurrence × F.Occurrence) : s ∈ w.steps → outArc time s ∈ T.arcs

  Each step's second port is an outgoing graph arc at the same timestamp.

• copies_injective (s : F.Occurrence × F.Occurrence) : s ∈ w.steps → ∀ t ∈ w.steps, (inArc time s).copy = (inArc time t).copy → s = t

  A copied constraint node occurs in only one step.

theorem Cslib.Logic.PL.CSP.DAG.linked_constraint {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {v : V} {ss : List (F.Occurrence × F.Occurrence)} (h : Walk.Linked v ss) {s : F.Occurrence × F.Occurrence} (hs : s ∈ ss) : match s, hs with | (input, output), hs => input.fst = output.fst

Every step of a linked incidence trail uses one original constraint position.

theorem Cslib.Logic.PL.CSP.DAG.pathDAG_supported {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (time : F.Occurrence → ℕ) : (pathDAG w time).Supported

A path graph retains exactly its actual supported incidences and copied nodes.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (hs : T.Supported) : (pathDAG w time).Subgraph T

A stamped directed path determines a supported subgraph of its ambient DAG.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.pairedCopies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) : (pathDAG w time).PairedCopies

Every copied constraint of a directed path has precisely its incoming and outgoing arc.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.take {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) (n : ℕ) : T.DirectedPath (w.take n) time

Every variable-ended prefix remains a directed path certificate.

theorem Cslib.Logic.PL.CSP.DAG.pathDAG_flip {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (time : F.Occurrence → ℕ) (f : F.OccurrenceLabeling Bool) : (pathDAG w time).flip f = w.flip f

A path graph flips exactly the incidences of the existing positional walk.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.valid_flip {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) (hM : EdgeInstance.EvenConstraints sem F) : ValidLabeling sem (w.flip f)

Corollary 36(2), on actual positional walk paths.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.valid_take {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) (hM : EdgeInstance.EvenConstraints sem F) (n : ℕ) : ValidLabeling sem ((w.take n).flip f)

Directed paths have valid flips at every variable-ended prefix, including the empty prefix.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.isFWalk {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) (hM : EdgeInstance.EvenConstraints sem F) (hi : Walk.InternallyConsistent f w.steps) (he : w.start ≠ w.finish) : Walk.IsFWalk sem f w

Endpoint inequality and internal consistency turn a directed DAG path into an f-walk. All prefix validity is a conclusion of Corollary 36, rather than part of the certificate.

def Cslib.Logic.PL.CSP.DAG.union {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (S U : F.DAG) : F.DAG

Union of finite incidence subgraphs, retaining every isolated supported node.

def Cslib.Logic.PL.CSP.DAG.terminalPair {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (a b : Arc F) : F.DAG

The two terminal incidences of paths meeting at one copied constraint.

theorem Cslib.Logic.PL.CSP.DAG.Supported.union {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {S U : F.DAG} (hs : S.Supported) (hu : U.Supported) : (S.union U).Supported

Uniting supported graphs preserves endpoint support.

theorem Cslib.Logic.PL.CSP.DAG.Subgraph.union {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {S U T : F.DAG} (hs : S.Subgraph T) (hu : U.Subgraph T) : (S.union U).Subgraph T

Uniting two subgraphs of the same graph remains a subgraph.

theorem Cslib.Logic.PL.CSP.DAG.PairedCopies.union {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {S U : F.DAG} (hs : S.PairedCopies) (hu : U.PairedCopies) (hss : S.Supported) (hus : U.Supported) (hd : Disjoint S.copies U.copies) : (S.union U).PairedCopies

The two-arc property combines across disjoint sets of copied constraints.

theorem Cslib.Logic.PL.CSP.DAG.pairedCopies_terminalPair {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {a b : Arc F} (hi : a.incoming = true) (hc : a.copy = b.copy) (hne : a ≠ b) : (terminalPair a b).PairedCopies

Two distinct arcs at one terminal copy, at least one incoming, satisfy the two-arc property.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.valid_flip_meeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} {w z : F.Walk} {timeW timeZ : F.Occurrence → ℕ} {a b : Arc F} (hw : T.DirectedPath w timeW) (hz : T.DirectedPath z timeZ) (h : IsFDAG sem f T) (hM : EdgeInstance.EvenConstraints sem F) (ha : a ∈ T.arcs) (hb : b ∈ T.arcs) (hai : a.incoming = true) (hcopy : a.copy = b.copy) (hne : a ≠ b) (hd : Disjoint (pathDAG w timeW).copies (pathDAG z timeZ).copies) (hwfresh : a.copy ∉ (pathDAG w timeW).copies) (hzfresh : a.copy ∉ (pathDAG z timeZ).copies) : ValidLabeling sem ((((pathDAG w timeW).union (pathDAG z timeZ)).union (terminalPair a b)).flip f)

Corollary 36(1): flip two directed paths together with their incoming terminal ports. Only disjointness of their copied constraint nodes is needed by the stronger two-arc theorem; the source's paths, disjoint except at the terminal copy, satisfy these hypotheses.