Finite buffers for the two-phase edge-CSP augmentation

The input contains the existing explicit-table CSP, two occurrence bit buffers, and an excluded starting variable. Positions retain constraint and scope order. All scans traverse actual lists; no loop is paid for by a binary variable name or a table's declared arity.

This module compiles the two phases of Lemma 31 of [KKR18], arXiv v6, Section 6.1, printed p. 15. The improving comparison is supplied as input; this routine does not find it or solve the CSP. Walk codes represent the existing CSP.Walk, without introducing another trail predicate.

Main definitions

• Input: the complete explicit-table input, with two finite occurrence label buffers.
• WalkCode, code, decode: the representation bridge to the existing incidence walks.
• run: the total finite implementation, rejecting incorrect buffer widths.

Main results

• computableInPolyTime_run: uniform ordinary native polynomial time in the full framed input.
• run_eq: exact agreement with EdgeInstance.augmentingWalk, without semantic assumptions.
• run_spec: decoded augmentation and the combined exchange bound for a valid improvement.

structure Cslib.Complexity.CSP.EdgeAugmenting.Input : Type

Complete augmentation input, with bits in constraint-then-scope occurrence order.

• body : Logic.PL.CSP Logic.PL.CSP.Table ℕ

  The original CSP, with explicit table relations and binary variable names.

• labels : List Bool

  Original occurrence labels.

• comparison : List Bool

  Supplied improving comparison, in the same positional order.

• excluded : ℕ

  Variable excluded only as the start, not as the terminal variable.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.encInputFields : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool × List Bool × ℕ ↪ List Bool

The tuple of the fields of encInput.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_excluded_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).excluded) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_labels_deg : Turing.MultiTapeTM.ComputableInDegree Input.labels encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {x1 x2 : γ → List Bool} {x3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (encCSP encTable Turing.MultiTapeTM.encNat)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) (h3 : Turing.MultiTapeTM.ComputableInPolyTime x3 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { body := x0 x, labels := x1 x, comparison := x2 x, excluded := x3 x }) encIn encInput

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_excluded_deg : Turing.MultiTapeTM.ComputableInDegree Input.excluded encInput Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_labels_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).labels) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Logic.PL.CSP Logic.PL.CSP.Table ℕ × List Bool × List Bool × ℕ) => { body := p.1, labels := p.2.1, comparison := p.2.2.1, excluded := p.2.2.2 }) encInputFields encInput 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_excluded_inO : Turing.MultiTapeTM.ComputableInO Input.excluded encInput Turing.MultiTapeTM.encNat (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_comparison_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).comparison) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_body_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).body) encIn✝ (encCSP encTable Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_labels_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encInput S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).labels) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_body_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).body) encIn✝ (encCSP encTable Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_comparison_deg : Turing.MultiTapeTM.ComputableInDegree Input.comparison encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_comparison_inO : Turing.MultiTapeTM.ComputableInO Input.comparison encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {x1 x2 : γ → List Bool} {x3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (encCSP encTable Turing.MultiTapeTM.encNat) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) budget) (h3 : Turing.MultiTapeTM.ComputableInSpace x3 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { body := x0 x, labels := x1 x, comparison := x2 x, excluded := x3 x }) encIn encInput budget

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_labels_inO : Turing.MultiTapeTM.ComputableInO Input.labels encInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Input) => (a.body, a.labels, a.comparison, a.excluded)) encInput encInputFields 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_excluded_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).excluded) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_comparison_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Input} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encInput → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).comparison) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_body_deg : Turing.MultiTapeTM.ComputableInDegree Input.body encInput (encCSP encTable Turing.MultiTapeTM.encNat) 1 1

def Cslib.Complexity.CSP.EdgeAugmenting.encInput : Input ↪ List Bool

The CSP, original bits and comparison bits are framed in field order; the final variable name is binary. Tables include their binary arity and explicitly framed Boolean rows.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CSP Logic.PL.CSP.Table ℕ} {T0 S0 : γ → ℕ} {x1 : γ → List Bool} {T1 S1 : γ → ℕ} {x2 : γ → List Bool} {T2 S2 x3 T3 S3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (encCSP encTable Turing.MultiTapeTM.encNat) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) T2 S2) (h3 : Turing.MultiTapeTM.ComputableInO x3 encIn Turing.MultiTapeTM.encNat T3 S3) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { body := x0 x, labels := x1 x, comparison := x2 x, excluded := x3 x }) encIn encInput (fun (x : γ) => T0 x + (T1 x + (T2 x + T3 x))) fun (x : γ) => S0 x + (S1 x + (S2 x + S3 x))

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_body_inO : Turing.MultiTapeTM.ComputableInO Input.body encInput (encCSP encTable Turing.MultiTapeTM.encNat) (fun (a : Input) => (encInput a).length) fun (a : Input) => (encInput a).length

@[simp]

theorem Cslib.Complexity.CSP.EdgeAugmenting.encInput_apply (a : Input) : encInput a = encInputFields (a.body, a.labels, a.comparison, a.excluded)

structure Cslib.Complexity.CSP.EdgeAugmenting.WalkCode : Type

A representation of an existing walk by global occurrence indices.

• start : ℕ

  Starting variable, encoded in binary.

• steps : List (ℕ × ℕ)

  Global occurrence indices in each ordered exchange, retaining repeated constraints.

def Cslib.Complexity.CSP.EdgeAugmenting.instDecidableEqWalkCode.decEq (x✝ x✝¹ : WalkCode) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.CSP.EdgeAugmenting.instDecidableEqWalkCode : DecidableEq WalkCode

@[instance_reducible]

instance Cslib.Complexity.CSP.EdgeAugmenting.instReprWalkCode : Repr WalkCode

def Cslib.Complexity.CSP.EdgeAugmenting.instReprWalkCode.repr : WalkCode → ℕ → Std.Format

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × List (ℕ × ℕ)) => { start := p.1, steps := p.2 }) encWalkCodeFields encWalkCode 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_start_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWalkCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).start) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_start_deg : Turing.MultiTapeTM.ComputableInDegree WalkCode.start encWalkCode Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_steps_deg : Turing.MultiTapeTM.ComputableInDegree WalkCode.steps encWalkCode (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) 1 1

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeFields : ℕ × List (ℕ × ℕ) ↪ List Bool

The tuple of the fields of encWalkCode.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : WalkCode) => (a.start, a.steps)) encWalkCode encWalkCodeFields 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_steps_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWalkCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).steps) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_start_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWalkCode S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).start) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_start_inO : Turing.MultiTapeTM.ComputableInO WalkCode.start encWalkCode Turing.MultiTapeTM.encNat (fun (a : WalkCode) => (encWalkCode a).length) fun (a : WalkCode) => (encWalkCode a).length

@[simp]

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_apply (a : WalkCode) : encWalkCode a = encWalkCodeFields (a.start, a.steps)

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_steps_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWalkCode → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).steps) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_steps_inO : Turing.MultiTapeTM.ComputableInO WalkCode.steps encWalkCode (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (fun (a : WalkCode) => (encWalkCode a).length) fun (a : WalkCode) => (encWalkCode a).length

def Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode : WalkCode ↪ List Bool

A binary start, framed, followed by framed pairs of binary global occurrence indices.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { start := x0 x, steps := x1 x }) encIn encWalkCode (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { start := x0 x, steps := x1 x }) encIn encWalkCode budget

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCode_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { start := x0 x, steps := x1 x }) encIn encWalkCode

def Cslib.Complexity.CSP.EdgeAugmenting.code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) : WalkCode

Project the existing walk to global occurrence indices.

def Cslib.Complexity.CSP.EdgeAugmenting.repair (input : Input) : List Bool × ℕ

First phase on finite buffers. The unary clock counts actual occurrence disagreements.

def Cslib.Complexity.CSP.EdgeAugmenting.recordAt (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (i : ℕ) : Record

Read an actual incidence record at a global position, defaulting to (0, 0, 0) when that position is outside the finite original occurrence list.

def Cslib.Complexity.CSP.EdgeAugmenting.finish (input : Input) (w : WalkCode) : ℕ

Read the last output port's original variable. An empty walk retains its original start; an invalid last position uses the same zero-record default as recordAt.

def Cslib.Complexity.CSP.EdgeAugmenting.buildWalk (input : Input) (g : List Bool) (start : ℕ) : Option WalkCode

Second phase on finite buffers. A stopped bit preserves the first reached original defect; an exhausted or unsuccessful scan rejects.

def Cslib.Complexity.CSP.EdgeAugmenting.run (input : Input) : Option WalkCode

Total finite implementation of the two phases. Both buffers must have exactly the actual occurrence count; malformed widths reject before either phase.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_steps_deg : Turing.MultiTapeTM.ComputableInDegree WalkCode.steps encWalkCodeWork (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_start_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWalkCodeWork → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).start) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_steps_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWalkCodeWork S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).steps) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) S✝

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { start := x0 x, steps := x1 x }) encIn encWalkCodeWork

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : WalkCode) => (a.start, a.steps)) encWalkCodeWork encWalkCodeWorkFields 1 1

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWorkFields : ℕ × List (ℕ × ℕ) ↪ List Bool

The tuple of the fields of encWalkCodeWork.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_steps_inO : Turing.MultiTapeTM.ComputableInO WalkCode.steps encWalkCodeWork (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) (fun (a : WalkCode) => (encWalkCodeWork a).length) fun (a : WalkCode) => (encWalkCodeWork a).length

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_start_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encWalkCodeWork S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).start) encIn✝ Turing.MultiTapeTM.encNat S✝

@[simp]

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_apply (a : WalkCode) : encWalkCodeWork a = encWalkCodeWorkFields (a.start, a.steps)

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_steps_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → WalkCode} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encWalkCodeWork → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).steps) encIn✝ (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))

def Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork : WalkCode ↪ List Bool

Work representation: the binary start is framed, and bounded occurrence positions are unary. This internal representation is converted to the binary encWalkCode on output.

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { start := x0 x, steps := x1 x }) encIn encWalkCodeWork (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 : γ → ℕ} {x1 : γ → List (ℕ × ℕ)} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { start := x0 x, steps := x1 x }) encIn encWalkCodeWork budget

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_start_inO : Turing.MultiTapeTM.ComputableInO WalkCode.start encWalkCodeWork Turing.MultiTapeTM.encNat (fun (a : WalkCode) => (encWalkCodeWork a).length) fun (a : WalkCode) => (encWalkCodeWork a).length

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_start_deg : Turing.MultiTapeTM.ComputableInDegree WalkCode.start encWalkCodeWork Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.encWalkCodeWork_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × List (ℕ × ℕ)) => { start := p.1, steps := p.2 }) encWalkCodeWorkFields encWalkCodeWork 1 1

theorem Cslib.Complexity.CSP.EdgeAugmenting.computableInPolyTime_run : Turing.MultiTapeTM.ComputableInPolyTime run encInput (Turing.MultiTapeTM.encOption encWalkCode)

Uniform native polynomial time on complete framed inputs, without validity, edge-instance, even-delta-matroid or improvement assumptions. Width errors reject; all other data are processed by list scans and occurrence clocks.

def Cslib.Complexity.CSP.EdgeAugmenting.decode (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (w : WalkCode) : Option F.Walk

Decode global positions into the existing dependent occurrence type. Out-of-range indices reject. This is a representation bridge, with no additional mathematical walk predicate.

theorem Cslib.Complexity.CSP.EdgeAugmenting.decode_code {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (w : F.Walk) : decode F (code w) = some w

The walk representation is lossless, including empty walks and repeated constraint visits.

theorem Cslib.Complexity.CSP.EdgeAugmenting.recordAt_index {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (o : F.Occurrence) : recordAt F (occurrenceIndex o) = o.record

Looking up the binary position of an actual occurrence recovers its exact positional record, including both original local coordinates and its original variable name.

theorem Cslib.Complexity.CSP.EdgeAugmenting.finish_eq (input : Input) (w : input.body.Walk) : finish input (code w) = w.finish

The finite binary-position endpoint of an encoded actual walk is exactly its original mathematical endpoint, including the length-zero fallback.

theorem Cslib.Complexity.CSP.EdgeAugmenting.run_eq (input : Input) (hf : input.labels.length = input.body.incidenceList.length) (hg : input.comparison.length = input.body.incidenceList.length) : run input = Option.map code (Logic.PL.CSP.EdgeInstance.augmentingWalk Logic.PL.CSP.Table.sem (labeling input.body input.labels) (labeling input.body input.comparison) input.excluded)

Exact compilation of the mathematical two-phase routine, including its deterministic scan order, both Hamming clocks and failure cases. Only the two exact buffer-width guards are needed.

theorem Cslib.Complexity.CSP.EdgeAugmenting.run_spec (input : Input) (hfwidth : input.labels.length = input.body.incidenceList.length) (hgwidth : input.comparison.length = input.body.incidenceList.length) (hedge : input.body.EdgeInstance) (heven : Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem input.body) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (labeling input.body input.labels)) (hg : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (labeling input.body input.comparison)) (hlt : (Logic.PL.CSP.defects (labeling input.body input.comparison)).card < (Logic.PL.CSP.defects (labeling input.body input.labels)).card) : ∃ (w : input.body.Walk), run input = some (code w) ∧ decode input.body (code w) = some w ∧ Logic.PL.CSP.Walk.IsAugmenting Logic.PL.CSP.Table.sem (labeling input.body input.labels) w ∧ w.start ≠ input.excluded ∧ 2 * ((repair input).2 + w.steps.length) ≤ hammingDist (labeling input.body input.labels) (labeling input.body input.comparison)

A valid improving comparison yields an actual augmenting walk, decoded into the existing model. The start alone avoids the excluded variable; the exchange bound is the original one.

theorem Cslib.Complexity.CSP.EdgeAugmenting.length_repair (input : Input) : (repair input).1.length = input.comparison.length

Repair flips bits without changing the comparison buffer's width, on every input.

theorem Cslib.Complexity.CSP.EdgeAugmenting.run_steps_length_le (input : Input) {w : WalkCode} (hw : run input = some w) : w.steps.length ≤ input.labels.length

Every successful output has at most the original buffer's length in steps, independently of semantic validity. With the width guard this is the actual occurrence count.

theorem Cslib.Complexity.CSP.EdgeAugmenting.run_eq_none_of_length (input : Input) (h : input.labels.length ≠ input.body.incidenceList.length ∨ input.comparison.length ≠ input.body.incidenceList.length) : run input = none

The width guard rejects either short or long original/comparison buffers.