Exact finite-buffer lifting agreement

Every surviving port, local exchange test and first-exit/arm scan is related to the original whole-instance lifting construction. This representation bookkeeping is original and preserves outside comparison changes and repeated copies of original constraints.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.restore_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (o : (Logic.PL.CSP.Blossom.contract f vs).Occurrence) : restore { body := F, labels := List.map f F.incidenceList } vs (EdgeAugmenting.occurrenceIndex fallback) (EdgeAugmenting.occurrenceIndex o) = EdgeAugmenting.occurrenceIndex (Logic.PL.CSP.Blossom.restorePortOr f vs fallback o)

The raw finite inverse is exactly the original surviving-port lookup, including its explicit fallback on malformed connector requests. No edge or validity assumption is needed.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.restoreWalk_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (p : (Logic.PL.CSP.Blossom.contract f vs).Walk) : restoreWalk { body := F, labels := List.map f F.incidenceList } vs (EdgeAugmenting.occurrenceIndex fallback) (EdgeAugmenting.code p) = EdgeAugmenting.code (Logic.PL.CSP.Blossom.restoreWalk f vs fallback p)

Restoring every binary step position gives exactly the source walk map, in source order.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.exitsAt_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) (n : ℕ) : exitsAt { body := F, labels := List.map f F.incidenceList } (EdgeAugmenting.code w) (EdgeAugmenting.code r) n = List.map (fun (x : F.Occurrence × F.Occurrence) => match x with | (o, e) => (EdgeAugmenting.occurrenceIndex o, EdgeAugmenting.occurrenceIndex e)) (Logic.PL.CSP.Blossom.exitsAt f w r n)

The finite exit scan has exactly the source's original-port order and pair-flip tests. Two equal ports cancel, as in the source's sequential pair flip.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.exitCode {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (e : Logic.PL.CSP.Blossom.Exit F) : ExitCode

Preserve the unary prefix length and binary original port positions of a source exit.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.firstExit_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) : firstExit { body := F, labels := List.map f F.incidenceList } (EdgeAugmenting.code w) (EdgeAugmenting.code r) = Option.map exitCode (Logic.PL.CSP.Blossom.firstExit f w r)

The finite first-exit scan selects exactly the same whole prefix and ordered actual ports.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.armCandidates_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) (o : F.Occurrence) : armCandidates F (EdgeAugmenting.code w) (EdgeAugmenting.occurrenceIndex o) = List.map EdgeAugmenting.code (Logic.PL.CSP.Blossom.armCandidates w o)

Actual prefix and reversed-suffix arm codes preserve every original copied step.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.attachment_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (o : F.Occurrence) : attachment { body := F, labels := List.map f F.incidenceList } (EdgeAugmenting.code w) (EdgeAugmenting.occurrenceIndex o) = Option.map EdgeAugmenting.code (Logic.PL.CSP.Blossom.attachmentWalk f w o)

Feasible-arm selection uses the exact current outside-prefix labeling.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.liftPrefix_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w r : F.Walk) : liftPrefix { body := F, labels := List.map f F.incidenceList } (EdgeAugmenting.code w) (EdgeAugmenting.code r) = Option.map (fun (g : F.Occurrence → Bool) => List.map g F.incidenceList) (Logic.PL.CSP.Blossom.liftPrefix f w r)

Full finite first-exit/arm lifting has exactly the mathematical constructor's result.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.liftWalk_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (p : (Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w)).Walk) : liftWalk { body := F, labels := List.map f F.incidenceList } (EdgeAugmenting.code w) (EdgeAugmenting.code p) = Option.map (fun (g : F.Occurrence → Bool) => List.map g F.incidenceList) (Logic.PL.CSP.Blossom.liftWalk f w p)

Native lifting has the exact source result in both connector cases. It restores every surviving original port and executes the same shortest-prefix and actual-arm scans.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.liftComparison_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (g : (Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w)).OccurrenceLabeling Bool) : liftComparison { body := F, labels := List.map f F.incidenceList } (EdgeAugmenting.code w) (List.map g (Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w)).incidenceList) = Option.map (fun (h : F.Occurrence → Bool) => List.map h F.incidenceList) (Logic.PL.CSP.Blossom.liftComparison f w g)

The full native comparison lifter agrees exactly with the mathematical constructor. Every comparison bit, including every outside change, is retained by the bridge.