Finite stack for one edge-CSP improvement

Frames retain the prepared original body, its finite occurrence buffer and its actual cycle. Descent performs a fresh native forest search and pushes exactly one frame per contraction. The first improvement unwinds those frames once, lifting an arbitrary improving child buffer. An exhausted child propagates optimality immediately. There is no recursive optimization of children. Clocks use actual occurrence-list lengths, independently of binary label magnitudes.

This program uses the original CSP Table ℕ, existing occurrence buffers, native forest codes and augmenting-walk codes. Preparation, contraction and lifting execute actual finite buffer operations, with no implementation or lifting provider as input. Agreement proves exact mathematical agreement; PolyTime supplies ordinary native certificates with full encoded storage bounds.

structure Cslib.Complexity.CSP.EdgeSolver.Program.Frame : Type

Prepared parent problem and the cycle used for its actual whole-instance contraction.

• parent : EdgeForest.Input

  Original body and exact-width prepared buffer.

• cycle : EdgeAugmenting.WalkCode

  Binary original base name and binary global occurrence positions.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_cycle_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFrame → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).cycle) encIn✝ EdgeAugmenting.encWalkCode

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_cycle_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFrame S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).cycle) encIn✝ EdgeAugmenting.encWalkCode S✝

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_parent_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encFrame S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).parent) encIn✝ EdgeForest.encInput S✝

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_parent_deg : Turing.MultiTapeTM.ComputableInDegree Frame.parent encFrame EdgeForest.encInput 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_cycle_inO : Turing.MultiTapeTM.ComputableInO Frame.cycle encFrame EdgeAugmenting.encWalkCode (fun (a : Frame) => (encFrame a).length) fun (a : Frame) => (encFrame a).length

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeForest.Input} {x1 : γ → EdgeAugmenting.WalkCode} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn EdgeForest.encInput) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn EdgeAugmenting.encWalkCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { parent := x0 x, cycle := x1 x }) encIn encFrame

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_cycle_deg : Turing.MultiTapeTM.ComputableInDegree Frame.cycle encFrame EdgeAugmenting.encWalkCode 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_parent_inO : Turing.MultiTapeTM.ComputableInO Frame.parent encFrame EdgeForest.encInput (fun (a : Frame) => (encFrame a).length) fun (a : Frame) => (encFrame a).length

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_parent_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Frame} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encFrame → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).parent) encIn✝ EdgeForest.encInput

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.Program.encFrameFields : EdgeForest.Input × EdgeAugmenting.WalkCode ↪ List Bool

The tuple of the fields of encFrame.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → EdgeForest.Input} {x1 : γ → EdgeAugmenting.WalkCode} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn EdgeForest.encInput budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn EdgeAugmenting.encWalkCode budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { parent := x0 x, cycle := x1 x }) encIn encFrame budget

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : EdgeForest.Input × EdgeAugmenting.WalkCode) => { parent := p.1, cycle := p.2 }) encFrameFields encFrame 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Frame) => (a.parent, a.cycle)) encFrame encFrameFields 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeForest.Input} {T0 S0 : γ → ℕ} {x1 : γ → EdgeAugmenting.WalkCode} {T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn EdgeForest.encInput T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn EdgeAugmenting.encWalkCode T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { parent := x0 x, cycle := x1 x }) encIn encFrame (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

@[simp]

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encFrame_apply (a : Frame) : encFrame a = encFrameFields (a.parent, a.cycle)

def Cslib.Complexity.CSP.EdgeSolver.Program.encFrame : Frame ↪ List Bool

The framed parent input precedes the cycle's framed base and ordered position pairs.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.Program.buffer {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) : List Bool

Encode the actual positional labeling by scanning actual incidences.

def Cslib.Complexity.CSP.EdgeSolver.Program.push (input : EdgeForest.Input) (event : EdgeForest.MeetingCode) : Option (Frame × EdgeForest.Input)

Read the actual blossom event, perform its preparatory flip and construct the child. All old constraint positions and all nullaries are retained by Blossom.contract.

def Cslib.Complexity.CSP.EdgeSolver.Program.augment (input : EdgeForest.Input) (event : EdgeForest.MeetingCode) : Option (List Bool)

Flip the actual decoded native augmentation and return its exact-width buffer.

def Cslib.Complexity.CSP.EdgeSolver.Program.lift (frame : Frame) (comparison : List Bool) : Option (List Bool)

Lift one actual child improvement into its prepared parent. Every outside change in the comparison is retained; the full liftComparison construction selects and lifts its walk.

structure Cslib.Complexity.CSP.EdgeSolver.Program.State : Type

Finite stack state. Status is running, proved optimal, or an improving finite buffer.

• current : EdgeForest.Input

  Current contracted problem; restored to the parent after every pop.

• frames : List Frame

  Prepared parents, newest first.

• budget : ℕ

  Remaining contraction depth, in unary and funded by the original occurrence list.

• status : Option (Option (List Bool))

  none descends; some none stops; some (some bits) unwinds.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_status_deg : Turing.MultiTapeTM.ComputableInDegree State.status encState (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))) 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeForest.Input} {T0 S0 : γ → ℕ} {x1 : γ → List Frame} {T1 S1 x2 T2 S2 : γ → ℕ} {x3 : γ → Option (Option (List Bool))} {T3 S3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn EdgeForest.encInput T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn (Turing.MultiTapeTM.encList encFrame) T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encUnary T2 S2) (h3 : Turing.MultiTapeTM.ComputableInO x3 encIn (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))) T3 S3) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { current := x0 x, frames := x1 x, budget := x2 x, status := x3 x }) encIn encState (fun (x : γ) => T0 x + (T1 x + (T2 x + T3 x))) fun (x : γ) => S0 x + (S1 x + (S2 x + S3 x))

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_current_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encState → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).current) encIn✝ EdgeForest.encInput

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_frames_deg : Turing.MultiTapeTM.ComputableInDegree State.frames encState (Turing.MultiTapeTM.encList encFrame) 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_current_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encState S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).current) encIn✝ EdgeForest.encInput S✝

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_frames_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encState S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).frames) encIn✝ (Turing.MultiTapeTM.encList encFrame) S✝

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_budget_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encState → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).budget) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_frames_inO : Turing.MultiTapeTM.ComputableInO State.frames encState (Turing.MultiTapeTM.encList encFrame) (fun (a : State) => (encState a).length) fun (a : State) => (encState a).length

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → EdgeForest.Input} {x1 : γ → List Frame} {x2 : γ → ℕ} {x3 : γ → Option (Option (List Bool))} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn EdgeForest.encInput) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn (Turing.MultiTapeTM.encList encFrame)) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encUnary) (h3 : Turing.MultiTapeTM.ComputableInPolyTime x3 encIn (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { current := x0 x, frames := x1 x, budget := x2 x, status := x3 x }) encIn encState

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.Program.encStateFields : EdgeForest.Input × List Frame × ℕ × Option (Option (List Bool)) ↪ List Bool

The tuple of the fields of encState.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_budget_inO : Turing.MultiTapeTM.ComputableInO State.budget encState Turing.MultiTapeTM.encUnary (fun (a : State) => (encState a).length) fun (a : State) => (encState a).length

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_current_deg : Turing.MultiTapeTM.ComputableInDegree State.current encState EdgeForest.encInput 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : State) => (a.current, a.frames, a.budget, a.status)) encState encStateFields 1 1

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_status_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encState S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).status) encIn✝ (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))) S✝

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_budget_deg : Turing.MultiTapeTM.ComputableInDegree State.budget encState Turing.MultiTapeTM.encUnary 1 1

@[simp]

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_apply (a : State) : encState a = encStateFields (a.current, a.frames, a.budget, a.status)

def Cslib.Complexity.CSP.EdgeSolver.Program.encState : State ↪ List Bool

Current input and stack are framed fields, followed by the two status tags and framed bits.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_budget_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encState S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).budget) encIn✝ Turing.MultiTapeTM.encUnary S✝

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_current_inO : Turing.MultiTapeTM.ComputableInO State.current encState EdgeForest.encInput (fun (a : State) => (encState a).length) fun (a : State) => (encState a).length

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_status_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encState → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).status) encIn✝ (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)))

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → EdgeForest.Input} {x1 : γ → List Frame} {x2 : γ → ℕ} {x3 : γ → Option (Option (List Bool))} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn EdgeForest.encInput budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn (Turing.MultiTapeTM.encList encFrame) budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encUnary budget) (h3 : Turing.MultiTapeTM.ComputableInSpace x3 encIn (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))) budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { current := x0 x, frames := x1 x, budget := x2 x, status := x3 x }) encIn encState budget

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_status_inO : Turing.MultiTapeTM.ComputableInO State.status encState (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))) (fun (a : State) => (encState a).length) fun (a : State) => (encState a).length

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_frames_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → State} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encState → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).frames) encIn✝ (Turing.MultiTapeTM.encList encFrame)

theorem Cslib.Complexity.CSP.EdgeSolver.Program.encState_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : EdgeForest.Input × List Frame × ℕ × Option (Option (List Bool))) => { current := p.1, frames := p.2.1, budget := p.2.2.1, status := p.2.2.2 }) encStateFields encState 1 1

def Cslib.Complexity.CSP.EdgeSolver.Program.step (state : State) : State

One descent or one lift. A stopped optimum needs no parent labeling reconstruction: count-preserving preparation and reference optimality transfer certify the original optimum.

def Cslib.Complexity.CSP.EdgeSolver.Program.improve (input : EdgeForest.Input) : Option (List Bool)

One-improvement stack program. Each contraction uses one descent and at most one lift. The additional steps fund the terminal search and final status. Clock value is unary and funded by the input occurrence list; no binary name or arity is expanded.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.Program.OptimizeState : Type

Outer optimization state: current original buffer and a flag preserving first exhaustion.

def Cslib.Complexity.CSP.EdgeSolver.Program.optimizeStep (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (state : OptimizeState) : OptimizeState

Improve the original problem once, stopping permanently after optimality is established.

def Cslib.Complexity.CSP.EdgeSolver.Program.optimize (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Option (List Bool)

Guarded finite optimization program. The occurrence list pays for all outer iterations. Malformed models reject before any forest search or contraction.

def Cslib.Complexity.CSP.EdgeSolver.Program.decideSAT (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Bool

Complete guarded finite decision program.