Counting true endpoints in edge labelings

Each edge variable has two endpoint bits. It contributes two true endpoints when both bits are true, one precisely when it is a defect, and zero otherwise. This elementary accounting connects minimum-defect optimization to maximum-cardinality graph matching.

theorem Cslib.Logic.PL.CSP.card_true_eq_sum_count {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) : {o : F.Occurrence | f o = true}.card = ∑ i : Fin (List.length F), List.count true (localTuple f i)

Counting true incidences constraint by constraint preserves their total count.

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

Actual occurring variables whose every endpoint is labeled true.

@[simp]

theorem Cslib.Logic.PL.CSP.mem_selectedVariables {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} {f : F.OccurrenceLabeling Bool} {v : V} : v ∈ selectedVariables f ↔ v ∈ F.vars ∧ ∀ (o : F.Occurrence), o.var = v → f o = true

theorem Cslib.Logic.PL.CSP.EdgeInstance.mem_selectedVariables_iff {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (o : F.Occurrence) : o.var ∈ selectedVariables f ↔ f o = true ∧ f (hF.partner o) = true

An edge is mutually selected iff both its endpoint labels are true.

theorem Cslib.Logic.PL.CSP.EdgeInstance.card_true_eq {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) : {o : F.Occurrence | f o = true}.card = 2 * (selectedVariables f).card + (defects f).card

True endpoints split into twice the mutually selected edges and the defective edges.