Exact chronological forest-search agreement

The finite program compiles the existing chronological forest search on every explicit-table CSP with an exact-width occurrence buffer. No edge, validity, evenness, reachability or supplied forest premise is used in this bridge.

def Cslib.Complexity.CSP.EdgeForest.workExpansion {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (e : Logic.PL.CSP.Forest.Expansion F) : WorkExpansion

Existing typed expansions represented using the shared positional record API.

def Cslib.Complexity.CSP.EdgeForest.workLog {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (es : Logic.PL.CSP.Forest.Log F) : WorkLog

Existing newest-first logs represented without changing expansion or port order.

theorem Cslib.Complexity.CSP.EdgeForest.roots_eq (input : Input) : roots input = Logic.PL.CSP.Forest.roots (EdgeAugmenting.labeling input.body input.labels)

Finite roots agree in their full deterministic order, without semantic assumptions.

theorem Cslib.Complexity.CSP.EdgeForest.partners_eq (input : Input) (a : input.body.Occurrence) (hw : input.labels.length = input.body.incidenceList.length) : partners input a.record = List.map Logic.PL.CSP.Occurrence.record (Logic.PL.CSP.Forest.partners Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling input.body input.labels) a)

Global partner validity and positional scan order agree, even for invalid input labelings.

theorem Cslib.Complexity.CSP.EdgeForest.scan_eq {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (rs : List ℕ) (es : Logic.PL.CSP.Forest.Log F) (a : F.Occurrence) (os bs : List F.Occurrence) : scan rs (workLog es) a.record (List.map Logic.PL.CSP.Occurrence.record os) (List.map Logic.PL.CSP.Occurrence.record bs) = match Logic.PL.CSP.Forest.scan rs es a os bs with | Logic.PL.CSP.Forest.ScanResult.continued out => (List.map Logic.PL.CSP.Occurrence.record out, none) | Logic.PL.CSP.Forest.ScanResult.meeting out b => (List.map Logic.PL.CSP.Occurrence.record out, some b.record)

Exact first-meeting scan, including current-copy children and same-original-parent skips.

theorem Cslib.Complexity.CSP.EdgeForest.run_eq (input : Input) (hw : input.labels.length = input.body.incidenceList.length) : run input = some (code (Logic.PL.CSP.Forest.search Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling input.body input.labels)))

Exact compilation of the existing chronological forest search on every raw explicit-table CSP. Correct buffer width alone suffices; the finite clock never fails on such an input.

theorem Cslib.Complexity.CSP.EdgeForest.run_eq_none_iff (input : Input) : run input = none ↔ input.labels.length ≠ input.body.incidenceList.length

Width mismatch is the only rejection: a correctly formed buffer never runs out of fuel.

theorem Cslib.Complexity.CSP.EdgeForest.decode_run (input : Input) (hw : input.labels.length = input.body.incidenceList.length) : (run input).bind (decode input.body) = some (Logic.PL.CSP.Forest.search Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling input.body input.labels))

Successful native output decodes to precisely the source result, with no supplied trace, forest invariant, implementation or semantic oracle.