Exact agreement of the finite improvement stack

The stack implements the recursive one-improvement program, rather than a recursive child optimizer. The explicit unary budget gives agreement on all raw states, independently of any edge or width hypotheses. A decreasing operational potential pays for every descent, terminal search and lift. The mathematical contraction measure supplies enough budget on valid models.

def Cslib.Complexity.CSP.EdgeSolver.Program.recurse : ℕ → EdgeForest.Input → Option (List Bool)

Recursive view of the finite program. It recurses once per blossom and returns immediately after one lift. Depth exhaustion is defined on arbitrary malformed raw states as well.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.improve_eq_recurse (input : EdgeForest.Input) : improve input = recurse (input.body.occurrences.length + 1) input

The finite native-search stack agrees exactly with the one-child recursive program on every raw input, including malformed widths. Its entire operational clock is list-funded.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.lift_eq {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (g : (Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w)).OccurrenceLabeling Bool) : lift { parent := { body := F, labels := buffer f }, cycle := EdgeAugmenting.code w } (buffer g) = Option.map buffer (Logic.PL.CSP.Blossom.liftComparison f w g)

One frame executes the actual arbitrary-comparison lifting construction exactly.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.push_code (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) (m : Logic.PL.CSP.Forest.Meeting F) : push { body := F, labels := buffer f } (EdgeForest.codeMeeting m) = Option.map (fun (b : Logic.PL.CSP.Forest.BlossomData F) => have prepared := b.prepare.flip f; have vs := Logic.PL.CSP.Blossom.internal b.cycle; ({ parent := { body := F, labels := buffer prepared }, cycle := EdgeAugmenting.code b.cycle }, { body := Logic.PL.CSP.Blossom.contract prepared vs, labels := buffer (Logic.PL.CSP.Blossom.reference prepared vs) })) m.blossomData

Finite preparation and contraction agree exactly with the complete source constructor.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.augment_code (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) (m : Logic.PL.CSP.Forest.Meeting F) : augment { body := F, labels := buffer f } (EdgeForest.codeMeeting m) = some (buffer (m.walk.flip f))

The finite augmentation returns the exact actual source walk's positional flip.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.recurse_eq (depth : ℕ) (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) : recurse depth { body := F, labels := buffer f } = Option.map buffer (Logic.PL.CSP.Solver.improve depth F f)

Exact source agreement of the recursive finite-buffer program at every depth. No edge-instance, valid-labeling or evenness premise is needed for this representation bridge.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.improve_eq (input : EdgeForest.Input) (hw : input.labels.length = input.body.incidenceList.length) : improve input = Option.map buffer (Logic.PL.CSP.Solver.improve (input.body.occurrences.length + 1) input.body (EdgeAugmenting.labeling input.body input.labels))

Exact stack/source agreement on every exact-width raw input. The buffer round trip is the shared EdgeAugmenting.buffer_eq API, available through an ordinary Buffer import.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.contractionMeasure_lt_clock (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (hF : F.EdgeInstance) : F.contractionMeasure < F.occurrences.length + 1

The actual occurrence list funds more than the concrete contraction measure on every edge instance, including nullaries and contractions that leave the variable count unchanged.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.improve_eq_source (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) : improve { body := F, labels := buffer f } = Option.map buffer (Logic.PL.CSP.Solver.improve (F.contractionMeasure + 1) F f)

On the actual model the list-funded program gives exactly the deterministic mathematical improvement with its canonical sufficient contraction budget.