An actual connector entry yields an original local exchange

The first-connector step in Lemma 44 of [KKR18], arXiv:1602.03124v6, printed p. 21, reads a stored row of the simultaneous whole-constraint contraction. Its single internal deviation identifies an actual original port, even at repeated constraints.

theorem Cslib.Logic.PL.CSP.Blossom.exchange_of_connector {F : CSP Table ℕ} (hF : F.EdgeInstance) {f current : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (hcurrent : ValidLabeling Table.sem current) (vs : List ℕ) (hinside : ∀ (o : F.Occurrence), o.var ∈ vs → current o = f o) (o : F.Occurrence) (ho : o.var ∉ vs) (ht : o.fst ∈ touched F vs) (central : List Bool) (hnew : ValidLabeling Table.sem (DAG.pairFlip (transport f vs current (fun (x : Fin (List.length F)) => false) central) (oldPort f vs o ho) (connectorPort f vs o.fst ht))) : ∃ (e : F.Occurrence), e.fst = o.fst ∧ e.var ∈ vs ∧ ValidLabeling Table.sem (DAG.pairFlip current o e)

A feasible first connector move identifies a feasible original two-port move. The current original labels may have arbitrary changed outside values; their internal bits are the reference.