One improvement through blossom contraction

The whole algorithm of [KKR18], arXiv:1602.03124v6, Algorithm 1 (printed p. 10) and Section 5.3 (printed pp. 11–13), organized to return one improvement. Each call performs one fresh search and at most one recursive child call. A child improvement is lifted and returned immediately. A child optimum transfers through Lemma 42; the preparation has the original defect count. This arrangement avoids recursively optimizing a contracted child before restarting a local optimization loop.

The explicit depth parameter makes the function total even on malformed input. For an edge instance with even delta-matroid constraints and valid labels, a depth exceeding contractionMeasure suffices. This module proves semantic correctness and termination; encoded native resource bounds belong to the executable implementation.

The recursion organization and its bookkeeping are original; the search, preparation, contraction and lifting are the existing constructions from the cited source.

def Cslib.Logic.PL.CSP.Solver.improve (depth : ℕ) (F : CSP Table ℕ) : F.OccurrenceLabeling Bool → Option (F.OccurrenceLabeling Bool)

Return one valid labeling with exactly two fewer defects, or certify optimality by returning none. The latter interpretation requires the depth and model hypotheses of improve_spec; depth exhaustion on arbitrary raw inputs simply returns none.

theorem Cslib.Logic.PL.CSP.Solver.improve_spec (depth : ℕ) (F : CSP Table ℕ) (f : F.OccurrenceLabeling Bool) (hd : F.contractionMeasure < depth) (hF : F.EdgeInstance) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) : match improve depth F f with | none => IsOptimalLabeling Table.sem f | some g => ValidLabeling Table.sem g ∧ (defects g).card + 2 = (defects f).card

An adequately funded call either certifies optimality or removes exactly two defects. All contraction and lifting obligations are derived internally from the fresh search.

theorem Cslib.Logic.PL.CSP.Solver.improve_depth_eq (F : CSP Table ℕ) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) (a b : ℕ) (ha : F.contractionMeasure < a) (hb : F.contractionMeasure < b) : improve a F f = improve b F f

Sufficient contraction budgets give exactly the same deterministic improvement, including its outside changes. Depth affects only malformed or inadequately funded executions.