Complete explicit-table even edge-CSP native P endpoint

For every raw CSP Table ℕ, the native decision routine accepts exactly the satisfiable actual edge instances with canonical nonempty even delta-matroid local relations. Model membership is checked internally by explicit stored-row pairs and coordinates. The runtime certificate has no input-validity hypothesis and uses the complete framed encCSP encTable encNat input, with binary arities/names, actual stored rows and every frame. The optimizer returns an actual minimum-defect occurrence labeling; the solver returns a satisfying occurrence buffer.

This is the explicit-table edge layer of Theorem 21 of [KKR18], arXiv:1602.03124v6, printed p. 8, implemented by Algorithm 1, Theorem 24 (printed p. 11), Section 5.3 and Lemmas 31, 34–35, 37, 40–45. Constraint scopes are positional lists without repetitions, each actual name occurs twice in distinct constraints, and duplicate constraints and rows are retained. Empty and true nullary instances are included; false/empty relations and malformed raw inputs are rejected by the decision problem's model guard. This is a guarded total decision problem rather than a promise endpoint. The Lean representation, framed-bit accounting and list-funded native compiler bookkeeping are original.

The planar reductions, hardness and dichotomy conclusions are separate endpoints.

def Cslib.Complexity.CSP.EdgeSolver.evenEdgeSAT : Set (Logic.PL.CSP Logic.PL.CSP.Table ℕ)

The ordinary guarded decision problem on complete raw explicit-table CSP inputs.

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

The actual semantic optimizer is implemented by the certified native finite stack.

theorem Cslib.Complexity.CSP.EdgeSolver.computableInPolyTime_solve : Turing.MultiTapeTM.ComputableInPolyTime solve (encCSP encTable Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool))

The actual solver, including every model and consistency guard, is ordinary native polynomial-time on every complete raw framed input.

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

The actual semantic decision routine is ordinary native polynomial-time on all raw input.

theorem Cslib.Complexity.CSP.EdgeSolver.solve_spec (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) {bits : List Bool} (h : solve F = some bits) : checkModel F = true ∧ bits.length = F.incidenceList.length ∧ Logic.PL.CSP.IsOptimalLabeling Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling F bits) ∧ (Logic.PL.CSP.defects (EdgeAugmenting.labeling F bits)).card = 0

Every returned solver buffer is an actual valid optimal zero-defect labeling, of exact original occurrence width. The successful call supplies every model and consistency check.

theorem Cslib.Complexity.CSP.EdgeSolver.decideSAT_eq_true_full (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : decideSAT F = true ↔ F ∈ evenEdgeSAT

SAT iff the total native full-model decision routine accepts, on every raw input.

theorem Cslib.Complexity.CSP.EdgeSolver.evenEdgeSAT_mem_P : evenEdgeSAT ∈ P (encCSP encTable Turing.MultiTapeTM.encNat)

Ordinary native polynomial-time decidability of the actual complete guarded edge problem. No model, comparison labeling, optimizer, lifter, rank or runtime certificate is input.