Correctness of the finite explicit-table solver

The list-funded stack and outer optimization loop agree exactly with the mathematical one-improvement solver. The complete guard is internal to the decision program. Acceptance means satisfiability under the existing Table.sem and the actual edge/even-delta-matroid model; raw malformed inputs and nonmodel relations are rejected.

This is the edge-layer algorithm of [KKR18], arXiv:1602.03124v6, Section 5 and Algorithm 1 (printed pp. 8–13). It supplies no planar embedding, hardness or dichotomy endpoint. Native bit-complexity certification is a separate obligation.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.iterate_eq (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) (rounds : ℕ) : ((optimizeStep F)^[rounds] (buffer f, false)).1 = buffer (Logic.PL.CSP.Solver.optimizeAux F rounds f)

The finite outer loop has exactly the mathematical solver's output at every round count. The stopped bit only avoids repeated fresh searches after an exhausted optimum.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.optimize_eq (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : optimize F = EdgeSolver.optimize F

Exact agreement of the guarded finite optimizer with the proved mathematical optimizer. This equation holds on all raw explicit-table inputs; the model guard is inside both sides.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.optimize_spec (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (h : checkModel F = true) : ∃ (bits : List Bool), optimize F = some bits ∧ bits.length = F.incidenceList.length ∧ Logic.PL.CSP.IsOptimalLabeling Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling F bits)

The native-search stack returns an actual minimum-defect finite occurrence buffer.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.decideSAT_eq (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : decideSAT F = EdgeSolver.decideSAT F

Exact decision agreement on every raw input, including false or malformed nullaries.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.decideSAT_eq_true (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : decideSAT F = true ↔ F.EdgeInstance ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem F ∧ Logic.PL.CSP.Satisfiable Logic.PL.CSP.Table.sem F

Complete guarded SAT correctness in the actual edge model. Every model check and every optimization step is executed internally; there is no validity premise on this endpoint.