Guarded explicit-table optimization and satisfiability

Initial local labels are actual first stored rows. The full model guard rejects empty or malformed relations and repeated scope variables. Optimization uses the complete original contraction/lifting mathematics. Its finite output is in the existing occurrence-list order.

The functions in this module specify the executable result; native multitape polynomial-time realization additionally requires finite implementations and encoded storage bounds.

def Cslib.Complexity.CSP.EdgeSolver.initialRows (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : List (List Bool)

One actual first stored row per original constraint. A missing row defaults to []; the full model guard rejects it, including a false nullary relation.

def Cslib.Complexity.CSP.EdgeSolver.initial (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : F.OccurrenceLabeling Bool

The initial positional labeling, with no global assignment search.

theorem Cslib.Complexity.CSP.EdgeSolver.initialRows_spec (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (h : checkModel F = true) (i : Fin (List.length F)) : F[↑i].1.sem ((initialRows F).getD ↑i []) = true ∧ ((initialRows F).getD ↑i []).length = F[↑i].2.length

Every initial stored row is accepted and has exactly its actual scope width.

theorem Cslib.Complexity.CSP.EdgeSolver.initial_valid (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (h : checkModel F = true) : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (initial F)

Choosing one actual first stored row per constraint gives valid occurrence labels, including true nullaries and repeated stored rows.

def Cslib.Complexity.CSP.EdgeSolver.optimize (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Option (List Bool)

Guarded minimum-defect finite occurrence buffer. none means an input outside the model, not an unsatisfiable valid model.

def Cslib.Complexity.CSP.EdgeSolver.solve (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Option (List Bool)

Return a satisfying finite occurrence buffer, rejecting both unsatisfiable instances and instances outside the checked edge/even-delta-matroid model.

def Cslib.Complexity.CSP.EdgeSolver.decideSAT (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Bool

A total guarded SAT decision on raw binary-name, explicit-table CSPs.

theorem Cslib.Complexity.CSP.EdgeSolver.optimize_width (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) {bits : List Bool} (h : optimize F = some bits) : bits.length = F.incidenceList.length

Every accepted optimizer output has exactly one bit per actual occurrence.

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

The optimizer returns an actual minimum over all valid original positional labelings.

theorem Cslib.Complexity.CSP.EdgeSolver.no_inconsistent_iff (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (bits : List Bool) : F.vars.any (EdgeAugmenting.inconsistent F bits) = false ↔ (Logic.PL.CSP.defects (EdgeAugmenting.labeling F bits)).card = 0

The finite original-name consistency scan is exactly zero actual occurrence defects.

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

Every returned optimizer buffer has actual width and is a minimum over all valid original occurrence labelings. The complete model guard is derived from its successful return.

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

SAT correctness on the full raw input: acceptance is equivalent to passing the actual finite model checks and satisfiability under Table.sem. No runtime assumption is supplied.