Whole-instance blossom contraction

The construction in Section 5.3 of [KKR18], arXiv:1602.03124v6, printed pp. 12–13. Constraints retain their original list positions, with the new exactly-one constraint appended. Each distinct touched original constraint is processed once; all its internal positions are contracted together, even when the cycle visits that constraint repeatedly. Outside positions retain their original order. Fresh binary natural names are obtained by an upper-bound fold followed by addition, without enumerating the interval below that bound.

The input and output are the original CSP Table ℕ. The intermediate rows below are finite buffers for its positional occurrence labeling, not a second CSP representation.

def Cslib.Logic.PL.CSP.Blossom.internal {F : CSP Table ℕ} (w : F.Walk) : List ℕ

Distinct variables used by the actual closed incidence trail.

def Cslib.Logic.PL.CSP.Blossom.positions (vs scope : List ℕ) : List ℕ

All internal positions of one original constraint, in original argument order.

theorem Cslib.Logic.PL.CSP.Blossom.validPositions_positions (vs scope : List ℕ) : Table.validPositions scope.length (positions vs scope) = true

Selected positions are distinct and in range, independently of variable-name magnitudes.

def Cslib.Logic.PL.CSP.Blossom.touched (F : CSP Table ℕ) (vs : List ℕ) : List (Fin (List.length F))

One index per distinct touched original constraint, in original constraint order.

def Cslib.Logic.PL.CSP.Blossom.freshBase (F : CSP Table ℕ) : ℕ

A name strictly larger than every old variable. Its computation scans actual occurrences.

def Cslib.Logic.PL.CSP.Blossom.connector (F : CSP Table ℕ) (i : Fin (List.length F)) : ℕ

Different original constraint positions receive different fresh binary names.

def Cslib.Logic.PL.CSP.Blossom.connectors (F : CSP Table ℕ) (vs : List ℕ) : List ℕ

The central scope contains one connector per touched original constraint.

def Cslib.Logic.PL.CSP.Blossom.constraint {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : Constraint Table ℕ

One original constraint is replaced by its simultaneous local contraction. Untouched constraints, including nullary constraints, retain their relation and scope.

def Cslib.Logic.PL.CSP.Blossom.contract {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : CSP Table ℕ

Executable whole-instance contraction. This keeps every old constraint and appends the central exactly-one constraint, even when some old constraints have empty scopes.

def Cslib.Logic.PL.CSP.Blossom.transportRows {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) : List (List Bool)

Ordered outside projections of actual original labels, with supplied connector bits and one supplied central row. The buffers retain exactly the old constraint ordering.

def Cslib.Logic.PL.CSP.Blossom.referenceRows {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : List (List Bool)

The local reference rows of the contracted instance. The central row is honestly one-hot; zero at all connector occurrences would not satisfy its exactly-one relation.

def Cslib.Logic.PL.CSP.Blossom.labels (G : CSP Table ℕ) (rows : List (List Bool)) : G.OccurrenceLabeling Bool

Read an actual finite row buffer as the original positional labeling interface.

def Cslib.Logic.PL.CSP.Blossom.reference {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (contract f vs).OccurrenceLabeling Bool

The contracted initial labeling.

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.length_contract {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : List.length (contract f vs) = List.length F + 1

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.length_connectors (F : CSP Table ℕ) (vs : List ℕ) : (connectors F vs).length = (touched F vs).length

theorem Cslib.Logic.PL.CSP.Blossom.freshBase_gt {F : CSP Table ℕ} {v : ℕ} (hv : v ∈ F.vars) : v < freshBase F

The constructor never visits an integer interval funded by variable names.

theorem Cslib.Logic.PL.CSP.Blossom.connector_not_mem {F : CSP Table ℕ} (i : Fin (List.length F)) : connector F i ∉ F.vars

Fresh connectors cannot coincide with any old occurring variable.

theorem Cslib.Logic.PL.CSP.Blossom.connector_injective (F : CSP Table ℕ) : Function.Injective (connector F)

Connectors distinguish constraint positions even for identical original constraints.

theorem Cslib.Logic.PL.CSP.Blossom.connector_lt {F : CSP Table ℕ} (i : Fin (List.length F)) : connector F i < freshBase F + List.length F

Fresh names lie below one addition of the original constraint count to the scanned name bound. The constructor never loops over the interval below this binary bound.

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.nodup_touched (F : CSP Table ℕ) (vs : List ℕ) : (touched F vs).Nodup

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.nodup_connectors (F : CSP Table ℕ) (vs : List ℕ) : (connectors F vs).Nodup

theorem Cslib.Logic.PL.CSP.Blossom.canContract_constraint {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (i : Fin (List.length F)) : F[↑i].1.canContract (localTuple f i) (positions vs F[↑i].2) = true

Every local contraction guard follows from the original valid occurrence labeling.

theorem Cslib.Logic.PL.CSP.Blossom.arity_constraint {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (i : Fin (List.length F)) : (constraint f vs i).1.arity = (constraint f vs i).2.length

Output arity equals the actual output scope, including for untouched nullary constraints.

theorem Cslib.Logic.PL.CSP.Blossom.rows_constraint_le {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : (constraint f vs i).1.rows.length ≤ F[↑i].1.rows.length

The number of stored rows of each old constraint never increases. Duplicate rows retain multiplicity, as in Table.contract.

theorem Cslib.Logic.PL.CSP.Blossom.localTuple_labels (G : CSP Table ℕ) (rows : List (List Bool)) (i : Fin (List.length G)) (hw : (rows.getD ↑i []).length = G[↑i].2.length) : localTuple (labels G rows) i = rows.getD ↑i []

Reading a row buffer recovers each complete row when its width is the actual scope width.

theorem Cslib.Logic.PL.CSP.Blossom.valid_labels (G : CSP Table ℕ) (rows : List (List Bool)) (hw : ∀ (i : Fin (List.length G)), (rows.getD ↑i []).length = G[↑i].2.length) (hv : ∀ (i : Fin (List.length G)), G[↑i].1.sem (rows.getD ↑i []) = true) : ValidLabeling Table.sem (labels G rows)

A finite row buffer is valid exactly when all its actual local rows are accepted.

theorem Cslib.Logic.PL.CSP.Blossom.get_contract_old {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : (contract f vs)[↑i] = constraint f vs i

Every retained output constraint has its original list index.

theorem Cslib.Logic.PL.CSP.Blossom.get_referenceRows_old {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : (referenceRows f vs).getD ↑i [] = if (positions vs F[↑i].2).isEmpty = true then localTuple f i else Table.project (localTuple f i) (Table.outsidePositions F[↑i].2.length (positions vs F[↑i].2)) ++ [false]

The finite reference buffer at a retained original constraint.

theorem Cslib.Logic.PL.CSP.Blossom.get_contract_central {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (contract f vs)[List.length F] = (Table.exactlyOne (connectors F vs), connectors F vs)

The central relation occupies the single newly appended constraint position.

theorem Cslib.Logic.PL.CSP.Blossom.get_referenceRows_central {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (referenceRows f vs).getD (List.length F) [] = BitString.listSingle (connectors F vs).length 0

The reference buffer at the central constraint is one-hot, with position zero selected.

theorem Cslib.Logic.PL.CSP.Blossom.referenceRow_valid {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (i : Fin (List.length F)) : (constraint f vs i).1.sem ((referenceRows f vs).getD ↑i []) = true

Each original local reference row is accepted by its actual output constraint.

theorem Cslib.Logic.PL.CSP.Blossom.referenceRow_length {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : ((referenceRows f vs).getD ↑i []).length = (constraint f vs i).2.length

Reference rows have exactly the constructor's scope widths.

theorem Cslib.Logic.PL.CSP.Blossom.valid_reference {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (hne : touched F vs ≠ []) : ValidLabeling Table.sem (reference f vs)

The constructed initial labeling satisfies all constraints. A nonempty touched set is necessary: exactly-one on zero connectors rejects every row.

theorem Cslib.Logic.PL.CSP.Blossom.rows_contract_nonempty {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (hne : touched F vs ≠ []) (i : Fin (List.length (contract f vs))) : (contract f vs)[↑i].1.rows ≠ []

No output relation is empty: the explicit reference witnesses it, rather than an assumed model of the original instance.

theorem Cslib.Logic.PL.CSP.Blossom.even_constraint {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) (vs : List ℕ) (i : Fin (List.length F)) : BitString.IsEvenDeltaMatroid {t : Fin (constraint f vs i).2.length → Bool | (constraint f vs i).1.sem (List.ofFn t) = true}

Local evenness is preserved on the actual ordered output scope.

theorem Cslib.Logic.PL.CSP.Blossom.even_contract {F : CSP Table ℕ} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (hM : EdgeInstance.EvenConstraints Table.sem F) (vs : List ℕ) (hne : touched F vs ≠ []) : EdgeInstance.EvenConstraints Table.sem (contract f vs)

Every actual output relation is a nonempty even delta-matroid, including the central exactly-one relation with its odd common parity.