Transporting changed outside labels through whole contraction

The row projection in Section 5.3 of [KKR18], arXiv:1602.03124v6, printed pp. 12–13, applies to actual original occurrence labels. Connector zero fixes the internal reference bits but places no restriction on outside changes. Connector one records one actual changed internal port. All constructors retain the original positional interface.

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

Project changed original labels, supplying each connector bit and the actual central row.

theorem Cslib.Logic.PL.CSP.Blossom.get_transportRows_old {F : CSP Table ℕ} (g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (i : Fin (List.length F)) : (transportRows g vs bits central).getD ↑i [] = if (positions vs F[↑i].2).isEmpty = true then localTuple g i else Table.project (localTuple g i) (Table.outsidePositions F[↑i].2.length (positions vs F[↑i].2)) ++ [bits i]

The old-constraint row of a general transport buffer.

theorem Cslib.Logic.PL.CSP.Blossom.get_transportRows_central {F : CSP Table ℕ} (g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) : (transportRows g vs bits central).getD (List.length F) [] = central

The general buffer retains its supplied central row verbatim.

theorem Cslib.Logic.PL.CSP.Blossom.transportRow_length {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (i : Fin (List.length F)) : ((transportRows g vs bits central).getD ↑i []).length = (constraint f vs i).2.length

Every projected old row has exactly the constructor's actual scope width.

theorem Cslib.Logic.PL.CSP.Blossom.transportRows_length {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) {central : List Bool} (hc : central.length = (connectors F vs).length) (i : Fin (List.length (contract f vs))) : ((transportRows g vs bits central).getD ↑i []).length = (contract f vs)[↑i].2.length

All actual output row widths agree when the central row has its finite scope width.

theorem Cslib.Logic.PL.CSP.Blossom.transportRows_project {F : CSP Table ℕ} (g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (i : Fin (List.length F)) : (transportRows g vs bits central).getD ↑i [] = Table.project (localTuple g i) (Table.outsidePositions F[↑i].2.length (positions vs F[↑i].2)) ++ if (positions vs F[↑i].2).isEmpty = true then [] else [bits i]

The old rows project outside coordinates in their original order, with a bit appended precisely at touched constraints.

theorem Cslib.Logic.PL.CSP.Blossom.transport_oldPort {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (o : F.Occurrence) (ho : o.var ∉ vs) : transport f vs g bits central (oldPort f vs o ho) = g o

Arbitrarily changed outside values survive the actual positional transport.

theorem Cslib.Logic.PL.CSP.Blossom.transport_connectorPort {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (i : Fin (List.length F)) (hi : i ∈ touched F vs) : transport f vs g bits central (connectorPort f vs i hi) = bits i

The connector's old-constraint endpoint reads its supplied finite bit.

theorem Cslib.Logic.PL.CSP.Blossom.transport_centralPort {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (k : Fin (connectors F vs).length) : transport f vs g bits central (centralPort f vs k) = central.getD (↑k) false

The central endpoint reads the supplied central row at the actual scope position.

theorem Cslib.Logic.PL.CSP.Blossom.valid_transport {F : CSP Table ℕ} {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (hg : ValidLabeling Table.sem g) (vs : List ℕ) (bits : Fin (List.length F) → Bool) {central : List Bool} (hc : (Table.exactlyOne (connectors F vs)).sem central = true) (hd : ∀ i ∈ touched F vs, Table.deviations (localTuple f i) (localTuple g i) (positions vs F[↑i].2) ≤ 1) (hb : ∀ i ∈ touched F vs, bits i = decide (Table.deviations (localTuple f i) (localTuple g i) (positions vs F[↑i].2) = 1)) : ValidLabeling Table.sem (transport f vs g bits central)

Feasible original rows with at most one selected deviation transport to feasible actual contracted labels, with their computed connector bits and any accepted central one-hot row.

theorem Cslib.Logic.PL.CSP.Blossom.valid_of_transport_zero {F : CSP Table ℕ} {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) {central : List Bool} (hc : central.length = (connectors F vs).length) (hi : ∀ (o : F.Occurrence), o.var ∈ vs → g o = f o) (hg : ValidLabeling Table.sem (transport f vs g (fun (x : Fin (List.length F)) => false) central)) : ValidLabeling Table.sem g

Zero connectors reflect validity for arbitrary outside changes when the internal reference bits are retained. This is the local inverse used before the first new connector of a walk.

theorem Cslib.Logic.PL.CSP.Blossom.inconsistent_transport_old {F : CSP Table ℕ} (hF : F.EdgeInstance) (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (o : F.Occurrence) (ho : o.var ∉ vs) : Inconsistent (transport f vs g bits central) o.var ↔ Inconsistent g o.var

Arbitrary outside defects are preserved exactly by projection.

theorem Cslib.Logic.PL.CSP.Blossom.inconsistent_transport_connector {F : CSP Table ℕ} (hF : F.EdgeInstance) (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) (k : Fin (touched F vs).length) : Inconsistent (transport f vs g bits central) (connector F (touched F vs)[↑k]) ↔ bits (touched F vs)[↑k] ≠ central.getD (↑k) false

The connector's defect is exactly disagreement of its two supplied endpoint bits.

def Cslib.Logic.PL.CSP.Blossom.connectorDefects (F : CSP Table ℕ) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) : List ℕ

The actual finite connector defects, scanned by distinct touched-constraint position.

theorem Cslib.Logic.PL.CSP.Blossom.defects_transport {F : CSP Table ℕ} (hF : F.EdgeInstance) (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (bits : Fin (List.length F) → Bool) (central : List Bool) : defects (transport f vs g bits central) = defects g \ vs.toFinset ∪ (connectorDefects F vs bits central).toFinset

Exact defect transport for arbitrary outside values and arbitrary finite connector rows.

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

Restore every original internal reference bit and read all changed outside bits from their actual surviving contracted ports. This is a total executable finite-label construction.

theorem Cslib.Logic.PL.CSP.Blossom.transport_expandZero {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (g : (contract f vs).OccurrenceLabeling Bool) (hbits : ∀ (i : Fin (List.length F)) (hi : i ∈ touched F vs), g (connectorPort f vs i hi) = false) (hcentral : ∀ (k : Fin (connectors F vs).length), g (centralPort f vs k) = (BitString.listSingle (connectors F vs).length 0).getD (↑k) false) : transport f vs (expandZero f vs g) (fun (x : Fin (List.length F)) => false) (BitString.listSingle (connectors F vs).length 0) = g

If the connector endpoints keep their reference values, projecting the restored labels recovers every actual contracted label, including arbitrary changed outside values.

theorem Cslib.Logic.PL.CSP.Blossom.valid_expandZero {F : CSP Table ℕ} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (g : (contract f vs).OccurrenceLabeling Bool) (hg : ValidLabeling Table.sem g) (hbits : ∀ (i : Fin (List.length F)) (hi : i ∈ touched F vs), g (connectorPort f vs i hi) = false) (hcentral : ∀ (k : Fin (connectors F vs).length), g (centralPort f vs k) = (BitString.listSingle (connectors F vs).length 0).getD (↑k) false) : ValidLabeling Table.sem (expandZero f vs g)

Restoring a valid zero-connector comparison gives a valid original labeling; outside coordinates need not agree with the prepared reference.

theorem Cslib.Logic.PL.CSP.Blossom.connectorDefects_zero {F : CSP Table ℕ} (vs : List ℕ) (hne : touched F vs ≠ []) : (connectorDefects F vs (fun (x : Fin (List.length F)) => false) (BitString.listSingle (connectors F vs).length 0)).toFinset = {baseConnector F vs hne}

Zero old connector ends and the honest central reference create one fresh defect.

theorem Cslib.Logic.PL.CSP.Blossom.card_defects_transport_zero {F : CSP Table ℕ} (hF : F.EdgeInstance) (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (hne : touched F vs ≠ []) : (defects (transport f vs g (fun (x : Fin (List.length F)) => false) (BitString.listSingle (connectors F vs).length 0))).card + (defects g ∩ vs.toFinset).card = (defects g).card + 1

General zero-connector transport deletes the old internal defects and inserts exactly one fresh connector defect, even when every outside value has changed.

theorem Cslib.Logic.PL.CSP.Blossom.card_defects_expandZero {F : CSP Table ℕ} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} {w : F.Walk} (hb : Walk.IsBlossom Table.sem f w) (g : (contract f (internal w)).OccurrenceLabeling Bool) (hbits : ∀ (i : Fin (List.length F)) (hi : i ∈ touched F (internal w)), g (connectorPort f (internal w) i hi) = false) (hcentral : ∀ (k : Fin (connectors F (internal w)).length), g (centralPort f (internal w) k) = (BitString.listSingle (connectors F (internal w)).length 0).getD (↑k) false) : (defects (expandZero f (internal w) g)).card = (defects g).card

A prepared blossom's internal defect is retained by zero expansion, and therefore the expanded original labeling has exactly the returned comparison's defect count.