Defects of Boolean occurrence labelings

Defects are distinct occurring variables, rather than incidences. All indices retain constraint positions, including repeated identical constraints. These definitions specialize Definition 20 of [KKR18], arXiv v6, printed p. 8. Nullary constraints remain subject to ValidLabeling; variables absent from the CSP never contribute defects.

Main definitions

• Inconsistent, defects: distinct defective variables of an occurrence labeling.
• IsOptimalLabeling: minimum defect count among valid labelings.
• EdgeInstance.EvenConstraints: an even delta-matroid on each constraint's argument positions.

Main results

• satisfiable_iff_exists_zero_defects: exact agreement with the existing CSP semantics.
• EdgeInstance.exists_valid_exchange: a local exchange lifted to the occurrence labeling.
• EdgeInstance.card_defects_mod_two_eq: Observation 30, allowing odd local parity.

def Cslib.Logic.PL.CSP.Inconsistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) (v : V) : Prop

A variable has two occurrences carrying unequal Boolean labels.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.instDecidableInconsistent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (f : F.OccurrenceLabeling Bool) (v : V) : Decidable (Inconsistent f v)

def Cslib.Logic.PL.CSP.defects {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (f : F.OccurrenceLabeling Bool) : Finset V

The finite set of inconsistent variables, with each variable counted once.

@[simp]

theorem Cslib.Logic.PL.CSP.mem_defects {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {f : F.OccurrenceLabeling Bool} {v : V} : v ∈ defects f ↔ Inconsistent f v

Defect membership has no additional occurrence hypothesis.

theorem Cslib.Logic.PL.CSP.defects_eq_empty_iff {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (f : F.OccurrenceLabeling Bool) : defects f = ∅ ↔ ConsistentLabeling f

Zero defects is exactly consistency, for arbitrary CSP instances.

theorem Cslib.Logic.PL.CSP.satisfiable_iff_exists_zero_defects {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) : Satisfiable sem F ↔ ∃ (f : F.OccurrenceLabeling Bool), ValidLabeling sem f ∧ (defects f).card = 0

Valid occurrence labels with no defects are exactly models of the original CSP.

def Cslib.Logic.PL.CSP.IsOptimalLabeling {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) : Prop

A valid labeling is optimal when no valid labeling has fewer inconsistent variables. This is Definition 20 of [KKR18], arXiv v6, printed p. 8.

theorem Cslib.Logic.PL.CSP.EdgeInstance.inconsistent_iff {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (o : F.Occurrence) : Inconsistent f o.var ↔ f o ≠ f (h.partner o)

At an edge occurrence, inconsistency compares exactly its two endpoint labels.

theorem Cslib.Logic.PL.CSP.EdgeInstance.var_ne_of_constraint_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) {o p : F.Occurrence} (hc : o.fst = p.fst) (hne : o ≠ p) : o.var ≠ p.var

Distinct argument positions of one constraint name distinct variables.

theorem Cslib.Logic.PL.CSP.EdgeInstance.inconsistent_flipOn_iff {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (h : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (s : Finset F.Occurrence) (o : F.Occurrence) : Inconsistent (BitString.flipOn s f) o.var ↔ if o ∈ s ↔ h.partner o ∈ s then Inconsistent f o.var else ¬Inconsistent f o.var

A flip toggles a defect precisely when it flips exactly one endpoint.

theorem Cslib.Logic.PL.CSP.EdgeInstance.defects_flipOn_singleton {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (o : F.Occurrence) : defects (BitString.flipOn {o} f) = symmDiff (defects f) {o.var}

Flipping one occurrence toggles just its variable's defect status.

theorem Cslib.Logic.PL.CSP.EdgeInstance.defects_flipOn_pair {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) {o p : F.Occurrence} (hc : o.fst = p.fst) (hne : o ≠ p) : defects (BitString.flipOn {o, p} f) = symmDiff (defects f) {o.var, p.var}

A same-constraint two-coordinate flip toggles two different variable defects.

theorem Cslib.Logic.PL.CSP.EdgeInstance.card_defects_flipOn_pair_mod_two {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) {o p : F.Occurrence} (hne : o ≠ p) : (defects (BitString.flipOn {o, p} f)).card % 2 = (defects f).card % 2

Two-coordinate exchanges preserve the number of defects modulo two.

theorem Cslib.Logic.PL.CSP.EdgeInstance.card_defects_flipOn_pair_le {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) {o p : F.Occurrence} (hne : o ≠ p) (ho : Inconsistent f o.var) : (defects (BitString.flipOn {o, p} f)).card ≤ (defects f).card

Repairing a defect by a two-coordinate move cannot increase the defect count.

def Cslib.Logic.PL.CSP.EdgeInstance.EvenConstraints {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (F : CSP Rel V) : Prop

Each constraint relation, on its actual ordered argument positions, is an even delta-matroid. Common parity may be odd and may differ between constraints.

theorem Cslib.Logic.PL.CSP.EdgeInstance.validLabeling_flipOn_pair {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (i : Fin (List.length F)) (a b : Fin F[i].2.length) (hab : sem F[i].1 (List.ofFn (BitString.flipOn {a, b} fun (j : Fin F[i].2.length) => f ⟨i, j⟩)) = true) : ValidLabeling sem (BitString.flipOn {⟨i, a⟩, ⟨i, b⟩} f)

A two-coordinate move in one constraint preserves validity exactly when its new tuple does.

theorem Cslib.Logic.PL.CSP.EdgeInstance.exists_valid_exchange {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) (o : F.Occurrence) (ho : f o ≠ g o) : ∃ (p : F.Occurrence), o.fst = p.fst ∧ o ≠ p ∧ f p ≠ g p ∧ ValidLabeling sem (BitString.flipOn {o, p} f)

Symmetric exchange at the actual constraint position gives a valid global two-bit move.

theorem Cslib.Logic.PL.CSP.EdgeInstance.card_defects_mod_two_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) : (defects f).card % 2 = (defects g).card % 2

Observation 30 of [KKR18], printed p. 14: valid labelings have congruent defect counts modulo two. Local common parities need not be zero.