Native list-funded improvement driver

The full model/label/width guard is evaluated internally. False guards retain the raw initial state; true guards derive the concrete stack invariant and full bit-storage bound. The machine certificate therefore applies to every raw framed input, with no runtime validity premise. The bounds and representation bookkeeping here are original.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_safeImprove : Turing.MultiTapeTM.ComputableInPolyTime safeImprove EdgeForest.encInput (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

The complete guarded one-improvement solver is ordinary native polynomial-time on all raw explicit-table inputs. The proof constructs its full model checks, actual stack bound and list-funded unary clock internally; no optimizer, rank or runtime certificate is input.