Projecting unchanged or singly changed internal labels

The two forward constructions in Lemma 42 of [KKR18], arXiv:1602.03124v6, printed p. 20, use either zero changed internal ports or one changed internal port. The central row is respectively the reference one-hot row or the exact touched-constraint indicator of that port. These are executable projections of actual labels.

theorem Cslib.Logic.PL.CSP.Blossom.deviations_zero_of_agree {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (h : ∀ (o : F.Occurrence), o.var ∈ vs → g o = f o) (i : Fin (List.length F)) : Table.deviations (localTuple f i) (localTuple g i) (positions vs F[↑i].2) = 0

Internal agreement gives zero local deviations at every actual constraint.

theorem Cslib.Logic.PL.CSP.Blossom.deviations_of_one_flip {F : CSP Table ℕ} (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (e : F.Occurrence) (hev : e.var ∈ vs) (h : ∀ (o : F.Occurrence), o.var ∈ vs → g o = if o = e then !f o else f o) (i : Fin (List.length F)) : Table.deviations (localTuple f i) (localTuple g i) (positions vs F[↑i].2) = if i = e.fst then 1 else 0

One changed internal occurrence contributes one deviation at its original constraint and zero at all other original constraints, regardless of repeated copied visits or table arity.

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

Projection with the honest reference connector row.

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

Projection retaining exactly the touched constraint that owns one internal changed port.

theorem Cslib.Logic.PL.CSP.Blossom.connectorDefects_matches {F : CSP Table ℕ} (vs : List ℕ) (bits : Fin (List.length F) → Bool) : connectorDefects F vs bits (List.map bits (touched F vs)) = []

Matching endpoint rows create no new connector defects.

theorem Cslib.Logic.PL.CSP.Blossom.sem_touched_indicator {F : CSP Table ℕ} (vs : List ℕ) (i : Fin (List.length F)) (hi : i ∈ touched F vs) : (Table.exactlyOne (connectors F vs)).sem (List.map (fun (j : Fin (List.length F)) => decide (j = i)) (touched F vs)) = true

The indicated touched constraint supplies an actual accepted central exactly-one row.

theorem Cslib.Logic.PL.CSP.Blossom.valid_projectZero {F : CSP Table ℕ} {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (hg : ValidLabeling Table.sem g) (vs : List ℕ) (hne : touched F vs ≠ []) (h : ∀ (o : F.Occurrence), o.var ∈ vs → g o = f o) : ValidLabeling Table.sem (projectZero f vs g)

Zero internal changes project to a valid actual contracted labeling.

theorem Cslib.Logic.PL.CSP.Blossom.valid_projectOne {F : CSP Table ℕ} {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (hg : ValidLabeling Table.sem g) (vs : List ℕ) (e : F.Occurrence) (hev : e.var ∈ vs) (h : ∀ (o : F.Occurrence), o.var ∈ vs → g o = if o = e then !f o else f o) : ValidLabeling Table.sem (projectOne f vs g e.fst)

A single changed internal port projects to a valid contracted labeling whose fresh connector endpoints all agree. The original outside labels may be arbitrary.

theorem Cslib.Logic.PL.CSP.Blossom.defects_projectOne {F : CSP Table ℕ} (hF : F.EdgeInstance) (f g : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : defects (projectOne f vs g i) = defects g \ vs.toFinset

The single-port projection creates no fresh defects; all surviving old defect values are taken from the changed original labeling.