Local growth certificates derived from executable partner scans

The certificates below record the actual step-2 choice and completed step-4 scan of [KKR18], arXiv:1602.03124v6, Algorithm 1, printed p. 10. They record local port conditions, not an assumed f-DAG or an optimality oracle.

Main results

• search_grown: all completed expansions in a fresh executable search have local certificates.
• Grown.outgoing_not_root: discovered variables are not initial roots.

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

Outputs accumulated before a scan continues or returns its first meeting.

theorem Cslib.Logic.PL.CSP.Forest.scan_outputs {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) (hfresh : ∀ o ∈ os, ¬Log.Visited rs es o.var) (hnodup : (List.map Occurrence.var os).Nodup) : have out := (scan rs es input os bs).outputs; (∀ o ∈ out, ¬Log.Visited rs es o.var) ∧ (List.map Occurrence.var out).Nodup ∧ out ⊆ os ++ bs

Every inserted child is fresh relative to the older forest, different from all other inserted children, and an actual member of the candidate list or the initial output list.

inductive Cslib.Logic.PL.CSP.Forest.Grown {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) : Log F → Prop

Every expansion can be justified by a previously grown forest, a genuinely unused input at a visited variable, and the local facts proved by its scan. Saturation concerns every feasible partner, including partners skipped because their parent has the same original constraint at an older timestamp.

• nil {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} : Grown sem f rs []

  Initial forest consists solely of isolated roots.

• cons {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} {e : Expansion F} (previous : Grown sem f rs es) (visited : Log.Visited rs es e.input.var) (unused : e.input ∉ es.used) (fresh : ∀ o ∈ e.outputs, ¬Log.Visited rs es o.var) (distinct : (List.map Occurrence.var e.outputs).Nodup) (feasible : ∀ o ∈ e.outputs, o ∈ partners sem f e.input) (saturated : ∀ o ∈ partners sem f e.input, o ∈ e.outputs ++ es.outgoing) : Grown sem f rs (e :: es)

  A complete scan extends a previously grown forest.

theorem Cslib.Logic.PL.CSP.Forest.Grown.outgoing_not_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) {o : F.Occurrence} (ho : o ∈ es.outgoing) : o.var ∉ rs

Every discovery variable is a nonroot, including across repeated constraint copies.

theorem Cslib.Logic.PL.CSP.Forest.Grown.of_scan {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) {rs : List V} {es : Log F} (hg : Grown sem f rs es) {input : F.Occurrence} (hv : Log.Visited rs es input.var) (hu : input ∉ es.used) {os : List F.Occurrence} (hs : scan rs es input [] (partners sem f input) = ScanResult.continued os) : Grown sem f rs ({ input := input, outputs := os } :: es)

A real continuing scan, together with the selected frontier incidence, supplies all local conditions of a growth certificate. No forest/DAG correctness is assumed.

theorem Cslib.Logic.PL.CSP.Forest.Log.Grown.used_visited {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) {o : F.Occurrence} (ho : o ∈ es.used) : Visited rs es o.var

Any port already used by a grown forest belongs to a visited variable.

theorem Cslib.Logic.PL.CSP.Forest.Log.Grown.output_not_used {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) {os : List F.Occurrence} (hf : ∀ o ∈ os, ¬Visited rs es o.var) {o : F.Occurrence} (ho : o ∈ os) : o ∉ es.used

Every fresh output port is distinct from every older used port.

theorem Cslib.Logic.PL.CSP.Forest.Log.Grown.output_var_ne {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} {e : Expansion F} (hg : Grown sem f rs (e :: es)) {o : F.Occurrence} (ho : o ∈ e.outputs) : e.input.var ≠ o.var

The two ports of an inserted step name distinct variables, even before invoking the edge-instance hypothesis used elsewhere.

def Cslib.Logic.PL.CSP.Forest.Result.Logs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (P : Log F → Prop) : Result F → Prop

The predicate on all completed logs returned by a search; a meeting also has an older completed log, while its current scan is deliberately partial.

theorem Cslib.Logic.PL.CSP.Forest.run_grown {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) (rs : List V) (es : Log F) (remaining : List F.Occurrence) (hg : Grown sem f rs es) (hu : ∀ o ∈ remaining, o ∉ es.used) : Result.Logs (Grown sem f rs) (run sem f rs es remaining)

Every completed expansion in the actual executable run has a local growth certificate. The only recursive precondition is exact remaining-port freshness, supplied by the program's filter and true initially. This theorem assumes neither DAG nor event correctness.

theorem Cslib.Logic.PL.CSP.Forest.search_grown {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) : Result.Logs (Grown sem f (roots f)) (search sem f)

Every completed log in a fresh search is derived from actual frontier choices and scans.