Incidence accounting for chronological forest traces

These are representation and scan facts for Algorithm 1 of [KKR18], arXiv:1602.03124v6, printed p. 10. Original constraints remain positional, copied constraints retain their chronological timestamps, and no theorem identifies different copies of the same original constraint.

Main results

• scan_saturated: a completed scan covers every feasible positional partner.
• Log.SameParent.mem_outgoing: step 4b identifies the exact already-used port.
• Log.mem_outgoing_of_arc: outgoing arcs use discovery ports.

def Cslib.Logic.PL.CSP.Forest.Log.outgoing {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : Log F → List F.Occurrence

Output ports in reverse expansion order and each expansion's scan order.

theorem Cslib.Logic.PL.CSP.Forest.Log.children_eq_map_outgoing {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) : es.children = List.map Occurrence.var es.outgoing

Forgetting output port positions gives precisely the discovered variables.

theorem Cslib.Logic.PL.CSP.Forest.Log.outgoing_subset_used {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) : es.outgoing ⊆ es.used

Every output port is used.

theorem Cslib.Logic.PL.CSP.Forest.Log.mem_outgoing_of_arc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {es : Log F} {a : DAG.Arc F} (ha : a ∈ es.arcs) (hi : a.incoming = false) : a.occurrence ∈ es.outgoing

Every recorded outgoing arc uses a discovery port.

theorem Cslib.Logic.PL.CSP.Forest.Log.parent?_sound {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) {p : Parent F} (hp : es.parent? v = some p) : p.output ∈ es.outgoing ∧ p.output.var = v ∧ p.time < List.length es

The parent lookup returns actual output ports with the requested variable.

theorem Cslib.Logic.PL.CSP.Forest.Log.SameParent.exists_output {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {es : Log F} {v : V} {i : Fin (List.length F)} (h : es.SameParent v i) : ∃ o ∈ es.outgoing, o.var = v ∧ o.fst = i

A skipped partner already has an actual output port at this original constraint.

theorem Cslib.Logic.PL.CSP.Forest.Log.SameParent.mem_outgoing {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (hF : F.EdgeInstance) {es : Log F} {b : F.Occurrence} (h : es.SameParent b.var b.fst) : b ∈ es.outgoing

In an edge instance a skipped feasible partner is the exact already-used positional port. This uses the source's distinct-variable-within-a-scope convention.

theorem Cslib.Logic.PL.CSP.Forest.Log.mem_arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) {a : DAG.Arc F} (ha : a ∈ es.arcs) : a.occurrence ∈ es.used ∧ a.time < List.length es

Every recorded arc uses a recorded port, at a strictly earlier timestamp than the next expansion. This holds even for malformed external logs.

theorem Cslib.Logic.PL.CSP.Forest.Log.toDAG_supported {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (rs : List V) (es : Log F) : (toDAG rs es).Supported

All arcs of the converted DAG have supported endpoints, including isolated roots.

theorem Cslib.Logic.PL.CSP.Forest.Log.Visited.mem_vars {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {rs : List V} {es : Log F} {v : V} (hv : Visited rs es v) : v ∈ (toDAG rs es).vars

A visited variable belongs to the converted DAG even when it is an isolated root.

theorem Cslib.Logic.PL.CSP.Forest.Log.exists_arc_iff {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (es : Log F) (o : F.Occurrence) : (∃ a ∈ es.arcs, a.occurrence = o) ↔ o ∈ es.used

Original occurrences of converted arcs are exactly the used ports.

theorem Cslib.Logic.PL.CSP.Forest.scan_outputs_mono {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (rs : List V) (es : Log F) (input : F.Occurrence) (bs os : List F.Occurrence) {out : List F.Occurrence} (h : scan rs es input os bs = ScanResult.continued out) : os ⊆ out

A continuing scan only adds outputs; it never discards a previously inserted child.

theorem Cslib.Logic.PL.CSP.Forest.scan_saturated {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (hF : F.EdgeInstance) (rs : List V) (es : Log F) (input : F.Occurrence) (bs os : List F.Occurrence) (hbs : ∀ b ∈ bs, b.fst = input.fst) {out : List F.Occurrence} (h : scan rs es input os bs = ScanResult.continued out) (b : F.Occurrence) : b ∈ bs → b ∈ out ++ es.outgoing

On completion, every candidate has an outgoing incidence, either newly discovered or already present at a copy of this same original constraint (step 4b). This is saturation of one actual completed scan, not a reachability assumption.