Constructive lifting from the actual contracted instance

Lemma 44 of [KKR18], arXiv:1602.03124v6, printed pp. 20–22, uses an actual contracted augmenting walk. Its prefix before the first connector restores through the zero-connector row semantics, and the first connector step supplies an actual original exchange. The shortest exit and full no-shortcut DAG argument then lift the change.

theorem Cslib.Logic.PL.CSP.Blossom.lift_entering_augmentation {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) (fallback : F.Occurrence) {p : (contract f (internal w)).Walk} (hp : Walk.IsAugmenting Table.sem (reference f (internal w)) p) (hx : p.start ≠ baseConnector F (internal w) ⋯) (hex : ∃ o ∈ p.edges, o.var ∈ connectors F (internal w)) : ∃ (g : F.OccurrenceLabeling Bool), liftPrefix f w (restoreWalk f (internal w) fallback (p.take (p.boundaryIndex (connectors F (internal w))))) = some g ∧ ValidLabeling Table.sem g ∧ (defects g).card + 2 = (defects f).card

The first connector of a contracted augmenting walk yields a valid original improvement. Every outside-prefix and local-exchange fact is derived from the actual returned walk.

def Cslib.Logic.PL.CSP.Blossom.liftWalk {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (p : (contract f (internal w)).Walk) : Option (F.OccurrenceLabeling Bool)

Lift an actual contracted augmenting walk. The fallback is taken from an actual cycle step. Connector-free walks restore directly; all other walks use their first connector.

theorem Cslib.Logic.PL.CSP.Blossom.liftWalk_spec {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) {p : (contract f (internal w)).Walk} (hp : Walk.IsAugmenting Table.sem (reference f (internal w)) p) (hx : p.start ≠ baseConnector F (internal w) ⋯) : ∃ (g : F.OccurrenceLabeling Bool), liftWalk f w p = some g ∧ ValidLabeling Table.sem g ∧ (defects g).card + 2 = (defects f).card

Lemma 44 on actual positional augmenting walks: the constructor always returns valid original labels and removes exactly two original defects. It supports both connector outcomes.

def Cslib.Logic.PL.CSP.Blossom.liftComparison {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (w : F.Walk) (g : (contract f (internal w)).OccurrenceLabeling Bool) : Option (F.OccurrenceLabeling Bool)

Lift an arbitrary improving valid contracted comparison. Lemma 31 constructs its actual augmenting walk starting away from the single new reference defect; Lemma 44 lifts that walk. The output is a strict improvement by two, as in the source, rather than an asserted equality with the possibly much smaller comparison's defect count.

theorem Cslib.Logic.PL.CSP.Blossom.liftComparison_spec {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) (g : (contract f (internal w)).OccurrenceLabeling Bool) (hg : ValidLabeling Table.sem g) (hlt : (defects g).card < (defects (reference f (internal w))).card) : ∃ (result : F.OccurrenceLabeling Bool), liftComparison f w g = some result ∧ ValidLabeling Table.sem result ∧ (defects result).card + 2 = (defects f).card

Constructive strict-improvement transfer for every actual returned contracted labeling. No global model, outside-comparison promise, or solver/lifting provider is assumed.