Actual contraction histories of the running solver stack

The stored baseline labelings all have the original defect count: preparation and honest reference contraction preserve that count. An improving status has exactly two fewer defects. The stack links each current body to its actual prepared parent, so an arbitrary changed-outside comparison is in the domain of the existing lifting theorem. All invariants below are derived from the original guarded model and actual execution, never supplied as runtime certificates. This bookkeeping is original.

def Cslib.Complexity.CSP.EdgeSolver.Program.InputGood (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (D : ℕ) (input : EdgeForest.Input) : Prop

An actual valid baseline in the original problem's concrete contraction history.

inductive Cslib.Complexity.CSP.EdgeSolver.Program.Stack (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (D : ℕ) : EdgeForest.Input → List Frame → Prop

Actual parent/child body links of a solver stack. Relabeling the current baseline is allowed; every frame still records its own exact prepared labeling and cycle.

• nil {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {input : EdgeForest.Input} (good : InputGood F D input) : Stack F D input []

  A current problem without stored parents.

• cons {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} (f : G.OccurrenceLabeling Bool) (w : G.Walk) (blossom : Logic.PL.CSP.Walk.IsBlossom Logic.PL.CSP.Table.sem f w) {frames : List Frame} (parents : Stack F D { body := G, labels := buffer f } frames) (bits : List Bool) (good : InputGood F D { body := Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w), labels := bits }) : Stack F D { body := Logic.PL.CSP.Blossom.contract f (Logic.PL.CSP.Blossom.internal w), labels := bits } ({ parent := { body := G, labels := buffer f }, cycle := EdgeAugmenting.code w } :: frames)

  An actual contracted child over an actual stored prepared parent.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.Stack.current {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {input : EdgeForest.Input} {frames : List Frame} (h : Stack F D input frames) : InputGood F D input

The current baseline is a valid actual member of the contraction history.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.Stack.relabel {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {input : EdgeForest.Input} {frames : List Frame} (h : Stack F D input frames) (f : input.body.OccurrenceLabeling Bool) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (hd : (Logic.PL.CSP.defects f).card = D) : Stack F D { body := input.body, labels := buffer f } frames

Preparation changes only the current baseline. It preserves the actual parent/body links.

def Cslib.Complexity.CSP.EdgeSolver.Program.StatusGood (D : ℕ) (input : EdgeForest.Input) : Option (Option (List Bool)) → Prop

A returned finite comparison is valid and removes exactly two original baseline defects.

structure Cslib.Complexity.CSP.EdgeSolver.Program.StateGood (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (D : ℕ) (state : State) : Prop

The stack's mathematical history, returned-buffer invariant and actual unary clock bound.

• stack : Stack F D state.current state.frames

  Every stored frame is an actual prepared parent of the next body.

• result : StatusGood D state.current state.status

  Improving status bits are an actual valid comparison with two fewer original defects.

• clock : state.frames.length + state.budget ≤ F.vars.length + 1

  Every pushed frame spends one actual original occurrence-funded depth unit.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.InputGood.materialized {F G : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} (f : G.OccurrenceLabeling Bool) (h : InputGood F D { body := G, labels := buffer f }) : ∃ (k : ℕ), Size.Chain F k G ∧ Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem G ∧ (Logic.PL.CSP.defects f).card = D

Recover the actual baseline properties when an input is materialized from a labeling.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.StateGood.step {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {state : State} (hF : F.EdgeInstance) (h : StateGood F D state) : StateGood F D (Program.step state)

Every real stack transition preserves its actual contraction history, valid comparisons and occurrence-funded clock. All model obligations come from fresh source search and lifting.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.StateGood.initial (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (f : F.OccurrenceLabeling Bool) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (hM : Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem F) : StateGood F (Logic.PL.CSP.defects f).card { current := { body := F, labels := buffer f }, frames := [], budget := F.occurrences.length + 1, status := none }

The original valid model internally supplies the initial stack invariant.

theorem Cslib.Complexity.CSP.EdgeSolver.Program.StateGood.iterate {F : Logic.PL.CSP Logic.PL.CSP.Table ℕ} {D : ℕ} {state : State} (hF : F.EdgeInstance) (h : StateGood F D state) (n : ℕ) : StateGood F D (Program.step^[n] state)

Every actual iteration internally retains the derived stack invariant.