The two actual ports of an edge variable

Two distinct original incidences naming the same variable exhaust its occurrences. This packages the existing partner API for positional transports that already exhibit both ends.

theorem Cslib.Logic.PL.CSP.EdgeInstance.eq_or_eq_of_two {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) {o p q : F.Occurrence} (hp : o.var = p.var) (hq : q.var = p.var) (hne : q ≠ p) : o = p ∨ o = q

Two distinct displayed ports exhaust every occurrence of their edge variable.

theorem Cslib.Logic.PL.CSP.EdgeInstance.inconsistent_iff_of_two {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (l : F.OccurrenceLabeling Bool) (p q : F.Occurrence) (hv : q.var = p.var) (hn : q ≠ p) : Inconsistent l p.var ↔ l p ≠ l q

A variable's defect is the disagreement of any displayed pair of its distinct ports.

theorem Cslib.Logic.PL.CSP.inconsistent_congr {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {f g : F.OccurrenceLabeling Bool} {v : V} (h : ∀ (o : F.Occurrence), o.var = v → f o = g o) : Inconsistent f v ↔ Inconsistent g v

Agreement at all actual ports of one variable preserves its exact defect status.

theorem Cslib.Logic.PL.CSP.defects_inter_eq_of_eqOn {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {f g : F.OccurrenceLabeling Bool} (vs : Finset V) (h : ∀ (o : F.Occurrence), o.var ∈ vs → f o = g o) : defects f ∩ vs = defects g ∩ vs

Agreement on a finite variable set preserves exactly the defects in that set.