Full framed storage of the running edge-CSP solver

The bounds include every stored prepared parent, all explicit relation rows and binary names, every binary step position, every list/pair/option frame, and the actual unary depth budget. They apply to the actual contraction histories derived by StateGood.step. They are original bookkeeping, and do not replace encoded bit length by unit-cost graph access.

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

Full framed occurrence input budget for every actual descended body.

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

Binary start and all framed step-position pairs of every actual blossom cycle.

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

A prepared parent is framed, followed by its full binary-position cycle.

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

All current fields and at most one frame per spent original occurrence.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.InputGood.encoded_le {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {input : EdgeForest.Input} (h : InputGood F D input) (hF : F.EdgeInstance) : (EdgeForest.encInput input).length ≤ inputBudget F

Baseline buffers charge their actual incidence width and complete descended body.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.Stack.frame_encoded_le {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {input : EdgeForest.Input} {frames : List Frame} (h : Stack F D input frames) (hF : F.EdgeInstance) (frame : Frame) : frame ∈ frames → (encFrame frame).length ≤ frameBudget F

Every stored frame has the same complete polynomial original-input storage budget.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.StateGood.encoded_le {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {state : State} (h : StateGood F D state) (hF : F.EdgeInstance) : (encState state).length ≤ stateBudget F

Full encoded storage of every actual running stack, including all tags and unary clocks.