2.25. Whole-Instance Blossom Contraction and Lifting🔗

Import CslibFrontier.Algorithms.Lean.EdgeCSP.Blossom.Optimality and CslibFrontier.Algorithms.Lean.EdgeCSP.Blossom.Size. The actual constructor contracts every internal port of each distinct touched original constraint once, retains outside order and nullaries, and appends a genuine exactly-one node. Its reference labels use a one-hot central row:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.Blossom in
example {F : CSP Table ℕ} {f : OccurrenceLabeling F Bool} {w : Walk F}
    (hF : EdgeInstance F) (hf : ValidLabeling Table.sem f)
    (hb : w.IsBlossom Table.sem f) :
    ValidLabeling Table.sem (reference f (internal w)) ∧
      (contract f (internal w)).contractionMeasure < F.contractionMeasure :=
  ⟨valid_reference hf _ (touched_ne_nil w hb.steps_ne_nil),
    contractionMeasure_contract_lt hF hb⟩

If b internal variables touch r original constraints, r ≤ b and numVars(new)+b = numVars(old)+r. Positive constraint count increases by one. The resource 2*numVars−positiveCount strictly decreases even when r=b; variable count alone is insufficient. Nullary constraints are not counted.

Cslib.Logic.PL.CSP.Blossom.isOptimal_of_reference transfers optimality from the contracted reference. If a recursive call instead supplies any improving valid contracted labels, the executable lift returns valid original labels with exactly two fewer defects:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.Blossom in
example {F : CSP Table ℕ} {f : OccurrenceLabeling F Bool} {w : Walk F}
    (hF : EdgeInstance F) (hf : ValidLabeling Table.sem f)
    (hb : w.IsBlossom Table.sem f)
    (hM : EdgeInstance.EvenConstraints Table.sem F)
    (g : OccurrenceLabeling (contract f (internal w)) Bool)
    (hg : ValidLabeling Table.sem g)
    (hlt : (defects g).card < (defects (reference f (internal w))).card) :
    match liftComparison f w g with
    | some result => ValidLabeling Table.sem result ∧
        (defects result).card + 2 = (defects f).card
    | none => False := byF:CSP Table ℕf:F.OccurrenceLabeling Boolw:F.WalkhF:F.EdgeInstancehf:ValidLabeling Table.sem fhb:Walk.IsBlossom Table.sem f whM:EdgeInstance.EvenConstraints Table.sem Fg:(contract f (internal w)).OccurrenceLabeling Boolhg:ValidLabeling Table.sem ghlt:(defects g).card < (defects (reference f (internal w))).card⊢ match liftComparison f w g with
| some result => ValidLabeling Table.sem result ∧ (defects result).card + 2 = (defects f).card
| none => False
  obtain ⟨result, hr, hv, hc⟩ := liftComparison_spec hF hb hf hM g hg hltF:CSP Table ℕf:F.OccurrenceLabeling Boolw:F.WalkhF:F.EdgeInstancehf:ValidLabeling Table.sem fhb:Walk.IsBlossom Table.sem f whM:EdgeInstance.EvenConstraints Table.sem Fg:(contract f (internal w)).OccurrenceLabeling Boolhg:ValidLabeling Table.sem ghlt:(defects g).card < (defects (reference f (internal w))).cardresult:F.OccurrenceLabeling Boolhr:liftComparison f w g = some resulthv:ValidLabeling Table.sem resulthc:(defects result).card + 2 = (defects f).card⊢ match liftComparison f w g with
| some result => ValidLabeling Table.sem result ∧ (defects result).card + 2 = (defects f).card
| none => False
  rw [hrF:CSP Table ℕf:F.OccurrenceLabeling Boolw:F.WalkhF:F.EdgeInstancehf:ValidLabeling Table.sem fhb:Walk.IsBlossom Table.sem f whM:EdgeInstance.EvenConstraints Table.sem Fg:(contract f (internal w)).OccurrenceLabeling Boolhg:ValidLabeling Table.sem ghlt:(defects g).card < (defects (reference f (internal w))).cardresult:F.OccurrenceLabeling Boolhr:liftComparison f w g = some resulthv:ValidLabeling Table.sem resulthc:(defects result).card + 2 = (defects f).card⊢ match some result with
| some result => ValidLabeling Table.sem result ∧ (defects result).card + 2 = (defects f).card
| none => False]F:CSP Table ℕf:F.OccurrenceLabeling Boolw:F.WalkhF:F.EdgeInstancehf:ValidLabeling Table.sem fhb:Walk.IsBlossom Table.sem f whM:EdgeInstance.EvenConstraints Table.sem Fg:(contract f (internal w)).OccurrenceLabeling Boolhg:ValidLabeling Table.sem ghlt:(defects g).card < (defects (reference f (internal w))).cardresult:F.OccurrenceLabeling Boolhr:liftComparison f w g = some resulthv:ValidLabeling Table.sem resulthc:(defects result).card + 2 = (defects f).card⊢ match some result with
| some result => ValidLabeling Table.sem result ∧ (defects result).card + 2 = (defects f).card
| none => False
  exact ⟨hv, hc⟩All goals completed! 🐙

No agreement with old outside labels is required. The code derives the actual augmenting walk, restores its outside prefix, and selects an original exchange and shortest exit using the full no-shortcut blossom. Forward projection is Cslib.Logic.PL.CSP.Blossom.projectAugmentation_spec.

CslibFrontierTests/EdgeCSPBlossomContraction.lean and CslibFrontierTests/EdgeCSPBlossomLifting.lean execute repeated original constraints, nonempty preparation, changed outside values, sparse binary names, and exact r=b accounting. Old table row counts do not increase; the new exactly-one table has r rows of width r. These mathematical and executable results feed the complete native recursive solver documented next. Geometric recognition, planar hardness and the full dichotomy remain open.