Native polynomial time for the complete edge-model guard

The certificates cover every raw binary-arity table and binary-name CSP, including malformed widths. All row, row-pair and coordinate loops are funded by explicit framed lists. Local working indices and counts use unary encodings; original arities and variable names stay binary.

theorem Cslib.Complexity.CSP.EdgeSolver.computableInPolyTime_checkConstraint : Turing.MultiTapeTM.ComputableInPolyTime checkConstraint (encConstraint encTable Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

A full constraint guard is ordinary native polynomial-time on all raw tables and scopes.

theorem Cslib.Complexity.CSP.EdgeSolver.computableInPolyTime_checkEdge : Turing.MultiTapeTM.ComputableInPolyTime checkEdge (encCSP encTable Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

The edge incidence check scans actual scopes and names, including arbitrarily sparse binary names. Its count results are unary and bounded by the explicit occurrence list.

theorem Cslib.Complexity.CSP.EdgeSolver.computableInPolyTime_checkModel : Turing.MultiTapeTM.ComputableInPolyTime checkModel (encCSP encTable Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Every check in the full model guard is supplied internally by native machines. No input validity or relation-recognition premise appears in the runtime certificate.