Documentation

CslibFrontier.Algorithms.Lean.EdgeCSP.Forest.Ancestry

Actual incidence trails reconstructed from chronological parents #

Parent reconstruction uses only older expansion records. The endpoint and trail proofs below concern the existing Walk semantics; they do not posit a second graph or walk model. The source is Algorithm 1's root paths, [KKR18], arXiv:1602.03124v6, printed pp. 10–11.

Main results #

source
def Cslib.Logic.PL.CSP.Forest.Log.stamp {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} :
Log F → F.Occurrence → ℕ

Timestamp of the expansion using a port as input; zero when no such expansion exists. For actual incoming arcs the fallback is unreachable.

Instances For
    source
    theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_finish {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) :
    (es.ancestry v).walk.finish = v

    Ancestry reconstruction always ends at the requested variable, including the empty path for an undiscovered variable.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_edges_subset {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) :
    (es.ancestry v).walk.edges ⊆ es.used

    Every reconstructed trail port is an actual recorded input or output port.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.stamp_eq {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) (hi : a.incoming = true) :
    es.stamp a.occurrence = a.time

    Actual incoming ports retain their chronological timestamps in executable lookup.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_isWalk {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).walk.IsWalk

    Reconstructed ancestries are linked incidence trails, without any assumption of path correctness. Constraint copies may repeat their original constraint position.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_arcs {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} (hm : s ∈ (es.ancestry v).walk.steps) :
    DAG.inArc es.stamp s ∈ es.arcs ∧ DAG.outArc es.stamp s ∈ es.arcs

    Every reconstructed step is supported by its actual incoming and outgoing graph arcs. This certifies the copied node, not merely its original constraint.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_copies_injective {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 t : F.Occurrence × F.Occurrence} (hs : s ∈ (es.ancestry v).walk.steps) (ht : t ∈ (es.ancestry v).walk.steps) (hc : (DAG.inArc es.stamp s).copy = (DAG.inArc es.stamp t).copy) :
    s = t

    An ancestral path visits each copied constraint at most once. Distinct copies of the same original constraint remain allowed.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_start_root {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} (hv : Log.Visited rs es v) :
    (es.ancestry v).walk.start ∈ rs

    The reconstructed path of every visited variable starts at one of the supplied roots.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_directed {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} (hv : Log.Visited rs es v) :
    (Log.toDAG rs es).DirectedPath (es.ancestry v).walk es.stamp

    Executable parent reconstruction gives an actual directed path in the existing DAG, including copied-node injectivity and original-incidence trail nonreuse.

    source
    theorem Cslib.Logic.PL.CSP.Forest.Grown.ancestry_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} {rs : List V} {es : Log F} (hg : Grown sem f rs es) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {v : V} (hv : Log.Visited rs es v) (n : ℕ) :
    ValidLabeling sem (((es.ancestry v).walk.take n).flip f)

    Every variable-ended prefix of a reconstructed root path preserves validity. This uses the existing DAG-path/surgery theorem, including repeated original constraints.