Positional transport of the contracted reference labeling

Surviving old ports retain their labels. The old-constraint end of every fresh connector is zero, and the new central end is the actual one-hot reference from Section 5.3 of [KKR18], arXiv:1602.03124v6, printed p. 12. All port constructors search finite actual position lists and use binary names only as data.

theorem Cslib.Logic.PL.CSP.Blossom.mem_outsidePositions (vs scope : List ℕ) (j : ℕ) : j ∈ Table.outsidePositions scope.length (positions vs scope) ↔ j < scope.length ∧ scope.getD j 0 ∉ vs

An original argument position survives exactly when its variable is outside the blossom.

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

Every surviving port has a valid index in the actual old-constraint output scope.

def Cslib.Logic.PL.CSP.Blossom.oldPort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : F.Occurrence) (ho : o.var ∉ vs) : (contract f vs).Occurrence

Map a surviving original occurrence to its new scope position. Its original constraint index is preserved, and its new argument index is found in the actual finite outside list.

theorem Cslib.Logic.PL.CSP.Blossom.oldPort_var {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : F.Occurrence) (ho : o.var ∉ vs) : (oldPort f vs o ho).var = o.var

Surviving occurrence transport preserves the original binary variable name.

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

The old reference buffer is the ordered outside projection, followed by a zero precisely at touched constraints. Untouched constraints need no extra connector bit.

theorem Cslib.Logic.PL.CSP.Blossom.reference_oldPort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : F.Occurrence) (ho : o.var ∉ vs) : reference f vs (oldPort f vs o ho) = f o

The explicit finite contracted reference retains every old outside occurrence value.

theorem Cslib.Logic.PL.CSP.Blossom.scope_constraint_touched {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) {i : Fin (List.length F)} (hi : i ∈ touched F vs) : (constraint f vs i).2 = List.map (fun (j : ℕ) => F[↑i].2.getD j 0) (Table.outsidePositions F[↑i].2.length (positions vs F[↑i].2)) ++ [connector F i]

The gathered outside list followed by the fresh port is the actual touched scope.

def Cslib.Logic.PL.CSP.Blossom.connectorPort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) (hi : i ∈ touched F vs) : (contract f vs).Occurrence

The new terminal port of a touched original constraint.

def Cslib.Logic.PL.CSP.Blossom.centralPort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (k : Fin (connectors F vs).length) : (contract f vs).Occurrence

The central port at an actual connector-scope position.

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.connectorPort_var {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) (hi : i ∈ touched F vs) : (connectorPort f vs i hi).var = connector F i

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.centralPort_var {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (k : Fin (connectors F vs).length) : (centralPort f vs k).var = (connectors F vs)[↑k]

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.reference_connectorPort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) (hi : i ∈ touched F vs) : reference f vs (connectorPort f vs i hi) = false

The touched-constraint end of every connector is honestly zero in the reference.

@[simp]

theorem Cslib.Logic.PL.CSP.Blossom.reference_centralPort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (k : Fin (connectors F vs).length) : reference f vs (centralPort f vs k) = decide (0 = ↑k)

The central end of exactly the first connector is one.

theorem Cslib.Logic.PL.CSP.Blossom.inconsistent_reference_old {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : F.Occurrence) (ho : o.var ∉ vs) : Inconsistent (reference f vs) o.var ↔ Inconsistent f o.var

Every old outside variable retains its exact defect status under reference transport.

theorem Cslib.Logic.PL.CSP.Blossom.inconsistent_reference_connector {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (k : Fin (touched F vs).length) : Inconsistent (reference f vs) (connector F (touched F vs)[↑k]) ↔ ↑k = 0

The connector at central scope position k is defective exactly when k = 0.

def Cslib.Logic.PL.CSP.Blossom.baseConnector (F : CSP Table ℕ) (vs : List ℕ) (hne : touched F vs ≠ []) : ℕ

The first connector is the unique new defect of the honest contracted reference.

theorem Cslib.Logic.PL.CSP.Blossom.defects_reference {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (hne : touched F vs ≠ []) : defects (reference f vs) = defects f \ vs.toFinset ∪ {baseConnector F vs hne}

Exact reference-defect transport: old outside defects survive and the single central one-hot entry contributes exactly one fresh connector defect.

theorem Cslib.Logic.PL.CSP.Blossom.card_defects_reference {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (hne : touched F vs ≠ []) : (defects (reference f vs)).card + (defects f ∩ vs.toFinset).card = (defects f).card + 1

The finite reference defect count deletes all old internal defects and inserts one. A blossom supplies exactly one old internal defect, yielding count preservation.

theorem Cslib.Logic.PL.CSP.Blossom.card_defects_reference_blossom {F : CSP Table ℕ} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} {w : F.Walk} (hb : Walk.IsBlossom Table.sem f w) : (defects (reference f (internal w))).card = (defects f).card

Observation 26's exact defect-count relation for the actual prepared blossom reference.