Finite-buffer arbitrary-comparison lifting

Implement the first-connector, shortest-exit and actual-arm scans of the existing whole-instance lifting construction. The comparison may change every surviving outside row. The actual native two-phase augmentation routine supplies its walk; all subsequent scans use original incidence records, binary global positions and list-funded prefix lengths.

The mathematical source is Lemmas 31 and 44 of [KKR18], arXiv:1602.03124v6, printed pp. 14 and 20–22. Finite representation bookkeeping is original.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.scope (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (o : EdgeAugmenting.Record) : List ℕ

Scope of one original positional record, with a bounded list default.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.oldRecord (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (vs : List ℕ) (o : EdgeAugmenting.Record) : EdgeAugmenting.Record

Record of a surviving original port in the actual contracted body. Its constraint position and original binary name are retained; its argument position is its outside-list rank.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.restore (input : EdgeForest.Input) (vs : List ℕ) (fallback index : ℕ) : ℕ

Invert surviving ports by the original finite incidence scan, preserving source tie order. The fallback is an actual cycle port on certified inputs; malformed raw positions remain total.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.restoreWalk (input : EdgeForest.Input) (vs : List ℕ) (fallback : ℕ) (p : EdgeAugmenting.WalkCode) : EdgeAugmenting.WalkCode

Restore the actual outside prefix, retaining its original start and step order.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.exitsAt (input : EdgeForest.Input) (w r : EdgeAugmenting.WalkCode) (n : ℕ) : List (ℕ × ℕ)

Actual feasible original exits from one prefix, in source scan order. The original outside port must be unused; pair feasibility is tested on the prefix's current finite buffer.

structure Cslib.Complexity.CSP.EdgeSolver.NativeLifting.ExitCode : Type

First feasible exit, with a unary number of whole prefix steps and binary port positions.

• length : ℕ

  Actual prefix length; this clock is funded by the supplied walk's step list.

• input : ℕ

  Original outside port's binary global position.

• output : ℕ

  Original cycle port's binary global position.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_length_inO : Turing.MultiTapeTM.ComputableInO ExitCode.length encExitCode Turing.MultiTapeTM.encUnary (fun (a : ExitCode) => (encExitCode a).length) fun (a : ExitCode) => (encExitCode a).length

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCodeFields : ℕ × ℕ × ℕ ↪ List Bool

The tuple of the fields of encExitCode.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encUnary T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encNat T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { length := x0 x, input := x1 x, output := x2 x }) encIn encExitCode (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_output_deg : Turing.MultiTapeTM.ComputableInDegree ExitCode.output encExitCode Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_length_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ExitCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encExitCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).length) encIn✝ Turing.MultiTapeTM.encUnary S✝

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : ExitCode) => (a.length, a.input, a.output)) encExitCode encExitCodeFields 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_output_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ExitCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encExitCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).output) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encUnary budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { length := x0 x, input := x1 x, output := x2 x }) encIn encExitCode budget

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_input_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → ExitCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encExitCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).input) encIn✝ Turing.MultiTapeTM.encNat S✝

@[simp]

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_apply (a : ExitCode) : encExitCode a = encExitCodeFields (a.length, a.input, a.output)

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_output_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ExitCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encExitCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).output) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_length_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ExitCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encExitCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).length) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_input_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → ExitCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encExitCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).input) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_length_deg : Turing.MultiTapeTM.ComputableInDegree ExitCode.length encExitCode Turing.MultiTapeTM.encUnary 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × ℕ × ℕ) => { length := p.1, input := p.2.1, output := p.2.2 }) encExitCodeFields encExitCode 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_input_deg : Turing.MultiTapeTM.ComputableInDegree ExitCode.input encExitCode Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_input_inO : Turing.MultiTapeTM.ComputableInO ExitCode.input encExitCode Turing.MultiTapeTM.encNat (fun (a : ExitCode) => (encExitCode a).length) fun (a : ExitCode) => (encExitCode a).length

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encUnary) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { length := x0 x, input := x1 x, output := x2 x }) encIn encExitCode

theorem Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode_output_inO : Turing.MultiTapeTM.ComputableInO ExitCode.output encExitCode Turing.MultiTapeTM.encNat (fun (a : ExitCode) => (encExitCode a).length) fun (a : ExitCode) => (encExitCode a).length

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.encExitCode : ExitCode ↪ List Bool

Unary prefix length is framed, then the binary outside position is framed, then the binary cycle position.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.firstExit (input : EdgeForest.Input) (w r : EdgeAugmenting.WalkCode) : Option ExitCode

Find the earliest whole prefix with a feasible original exit, then its first actual pair.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.armCandidates (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (w : EdgeAugmenting.WalkCode) (outside : ℕ) : List EdgeAugmenting.WalkCode

Two actual arms at every matching original constraint, in original cycle-step order. Repeated original constraints are retained as separate copied steps.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.attachment (input : EdgeForest.Input) (w : EdgeAugmenting.WalkCode) (outside : ℕ) : Option EdgeAugmenting.WalkCode

Choose the first actual valid arm against the already changed outside prefix.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.liftPrefix (input : EdgeForest.Input) (w r : EdgeAugmenting.WalkCode) : Option (List Bool)

Perform the first feasible outside prefix and the first feasible actual original arm.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.liftWalk (input : EdgeForest.Input) (w p : EdgeAugmenting.WalkCode) : Option (List Bool)

Restore a connector-free augmentation directly, or restore the prefix before its first connector and execute the actual original exit/arm construction.

def Cslib.Complexity.CSP.EdgeSolver.NativeLifting.liftComparison (input : EdgeForest.Input) (w : EdgeAugmenting.WalkCode) (comparison : List Bool) : Option (List Bool)

Actual native comparison augmentation followed by whole-instance lifting. Every width check is supplied internally by the native augmentation routine.