Native polynomial-time complete optimization

One checked improvement is followed by an outer list-funded optimization loop. The first optimal status freezes that loop. Native certificates cover every raw complete framed CSP; model and row checks are all internal, including malformed arities and sparse binary names. The finite representation and resource bookkeeping are original.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeSolver.Program.encOptimizeState : List Bool × Bool ↪ List Bool

Current original occurrence bits are framed, followed by the stopped flag.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_optimize : Turing.MultiTapeTM.ComputableInPolyTime optimize (encCSP encTable Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

The complete optimizer is ordinary native polynomial-time in the full framed original input, including every raw malformed explicit table and every binary label bit.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.computableInPolyTime_decideSAT : Turing.MultiTapeTM.ComputableInPolyTime decideSAT (encCSP encTable Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

The native decision routine supplies every model check internally and charges the full complete framed CSP, with no input-validity premise in the runtime certificate.