Native polynomial-time complete explicit-table edge solver

The complete framed input includes binary names and arities, all relation rows, and every list frame. The guard supplies every model, row-validity and width check internally. The one-child improvement stack has a list-funded unary clock, full encoded storage bounded by stateBudget, and one native step machine uniform on all raw states. These certificates are original finite representation and resource bookkeeping for the existing whole-instance algorithm.

def Cslib.Complexity.CSP.EdgeSolver.Program.inputGuard (input : EdgeForest.Input) : Bool

Complete internal guard for one improvement input, including its actual buffer width.

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

Total guarded one-improvement program. Every row/model/width check is internal.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.inputGuard_spec (input : EdgeForest.Input) (h : inputGuard input = true) : input.body.EdgeInstance ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem input.body ∧ Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling input.body input.labels) ∧ input.labels.length = input.body.incidenceList.length

The internal guard supplies the actual model and valid exact-width occurrence labeling.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.safeImprove_width (input : EdgeForest.Input) {bits : List Bool} (h : safeImprove input = some bits) : bits.length = input.body.incidenceList.length

Every successful guarded improvement has the original actual occurrence width. This statement covers all raw inputs, without assuming a valid model or a well-formed buffer.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.safeImprove_buffer (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (hM : Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem F) : safeImprove { body := F, labels := buffer f } = improve { body := F, labels := buffer f }

The guarded wrapper agrees with the unguarded mathematical improvement on its actual model. Validity and width are checked by the wrapper itself on raw inputs.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_stateBudget : Turing.MultiTapeTM.ComputableInPolyTime stateBudget (encCSP encTable Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encUnary

The full stack-storage budget is itself native polynomial-time in unary on every raw CSP. Its computation scans actual lists and complete encoded names, never an interval of labels.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.polyBounded_stateBudget : Turing.MultiTapeTM.PolyBounded (fun (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) => ((encCSP encTable Turing.MultiTapeTM.encNat) F).length) stateBudget

Full framed stack storage is polynomial in the complete framed original input length.