Invariants of completed chronological forest expansions

Derivations from actual local growth certificates of Algorithm 1, [KKR18], arXiv:1602.03124v6, printed pp. 10 and 16. Saturation is essential: pairwise feasible graph adjacency alone is insufficient for the prefix-dependent walk semantics. Original-constraint revisits are retained throughout.

Main results

• search_completed_isFDAG: all six DAG invariants for completed expansions of a fresh run.

theorem Cslib.Logic.PL.CSP.Forest.Log.map_arcs_occurrence {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) : List.map DAG.Arc.occurrence es.arcs = es.used

Recording arcs and then forgetting orientations and timestamps recovers all used ports, including the input port of an expansion with no children.

theorem Cslib.Logic.PL.CSP.Forest.Log.map_outgoing_arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) : List.map (fun (a : DAG.Arc F) => a.occurrence.var) (List.filter (fun (a : DAG.Arc F) => !a.incoming) es.arcs) = es.children

Outgoing arcs are exactly the recorded discovery ports, preserving multiplicity.

theorem Cslib.Logic.PL.CSP.Forest.Log.outgoing_arc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {es : Log F} {b : F.Occurrence} (hb : b ∈ es.outgoing) : ∃ c ∈ es.arcs, c.occurrence = b ∧ c.incoming = false

Every output port has its actual outgoing stamped arc in the recorded graph.

def Cslib.Logic.PL.CSP.Forest.Log.birth {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] : Log F → V → ℕ

Rank of a variable: roots have rank zero; a newly discovered child at time t has rank 2*t+2. This finite chronological numbering never compares variable names.

theorem Cslib.Logic.PL.CSP.Forest.Log.birth_le {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) : es.birth v ≤ 2 * List.length es

Every variable rank is at most twice the number of completed expansions.

theorem Cslib.Logic.PL.CSP.Forest.Grown.used_nodup {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) : es.used.Nodup

No positional incidence is ever reused by a completed chronological forest.

theorem Cslib.Logic.PL.CSP.Forest.Grown.children_nodup {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) : es.children.Nodup

A variable is discovered at most once, even across different copies of a constraint.

theorem Cslib.Logic.PL.CSP.Forest.Grown.unique {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) {a b : DAG.Arc F} (ha : a ∈ es.arcs) (hb : b ∈ es.arcs) (he : a.occurrence = b.occurrence) : a = b

Incidence uniqueness, including orientation and timestamp, follows from the executable port-accounting invariant rather than an assumed graph property.

theorem Cslib.Logic.PL.CSP.Forest.Grown.indegree {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) {a b : DAG.Arc F} (ha : a ∈ es.arcs) (hb : b ∈ es.arcs) (hai : a.incoming = false) (hbi : b.incoming = false) (he : a.occurrence.var = b.occurrence.var) : a = b

Every variable has at most one incoming incidence arc (copy-to-variable orientation).

theorem Cslib.Logic.PL.CSP.Forest.Grown.saturated {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) {a : DAG.Arc F} (ha : a ∈ es.arcs) (hai : a.incoming = true) {b : F.Occurrence} (hpartner : b ∈ partners sem f a.occurrence) : ∃ c ∈ es.arcs, c.occurrence = b ∧ c.incoming = false ∧ c.time ≤ a.time

A complete scan supplies an outgoing witness for each feasible partner of an incoming arc. Its timestamp is no later than that incoming arc's timestamp.

theorem Cslib.Logic.PL.CSP.Forest.Grown.noShortcut {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) (hF : F.EdgeInstance) {a b : DAG.Arc F} (ha : a ∈ es.arcs) (hb : b ∈ es.arcs) (hai : a.incoming = true) (hc : a.occurrence.fst = b.occurrence.fst) (ht : a.time < b.time) : ¬ValidLabeling sem (DAG.pairFlip f a.occurrence b.occurrence)

Completed scans rule out every shortcut from an old incoming port to a later used port, including later incoming ports. This is condition 6 of Definition 32.

theorem Cslib.Logic.PL.CSP.Forest.Grown.rank_arc {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) {a : DAG.Arc F} (ha : a ∈ es.arcs) : if a.incoming = true then es.birth a.occurrence.var < 2 * a.time + 1 else 2 * a.time + 1 < es.birth a.occurrence.var

Every recorded directed arc increases its chronological node rank.

theorem Cslib.Logic.PL.CSP.Forest.Grown.copy_unique {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) {a b : DAG.Arc F} (ha : a ∈ es.arcs) (hb : b ∈ es.arcs) (ht : a.time = b.time) : a.copy = b.copy

Different original constraint positions cannot share a timestamp.

theorem Cslib.Logic.PL.CSP.Forest.Grown.ordered {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) : (Log.toDAG rs es).Ordered

The source's timestamp-compatible topological order, witnessed by an explicit finite rank. Equal ranks of unrelated roots are harmless and can be broken by the existing DAG API.

theorem Cslib.Logic.PL.CSP.Forest.Grown.feasible {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) (hf : ValidLabeling sem f) {a b : DAG.Arc F} (ha : a ∈ es.arcs) (hb : b ∈ es.arcs) (hai : a.incoming = true) (hc : a.copy = b.copy) : ValidLabeling sem (DAG.pairFlip f a.occurrence b.occurrence)

Feasibility at every copied constraint, with cancellation of equal input ports.

theorem Cslib.Logic.PL.CSP.Forest.Grown.isFDAG {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) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) : DAG.IsFDAG sem f (Log.toDAG rs es)

Lemma 34 for completed expansions, derived from chronological growth, including full same-original-constraint no-shortcut and an explicit ordered-forest rank.

theorem Cslib.Logic.PL.CSP.Forest.search_completed_isFDAG {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) : Result.Logs (fun (es : Log F) => DAG.IsFDAG sem f (Log.toDAG (roots f) es)) (search sem f)

Every completed forest appearing as a search result is an f-DAG, with no supplied forest-correctness premise. The partially scanned terminal copy is treated separately.