Constructive matching and minimum-defect correspondence

The choice constraints use the original normalized graph incidences. A valid local labeling selects at most one original edge at each vertex; mutually selected edges therefore give an actual Mathlib matching. Every Mathlib matching supplies a feasible comparison labeling, with private unmatched ports precisely at its uncovered vertices.

theorem Cslib.Complexity.Graph.getElem_matchingInstance_vertex {G : Graph} {v : ℕ} (hv : v ∈ G.vertices) : G.matchingInstance[List.idxOf v G.distinctVertices] = (Logic.PL.CSP.Table.exactlyOne (G.matchingScope v), G.matchingScope v)

A vertex's choice constraint is at its position in the distinct vertex list.

theorem Cslib.Complexity.Graph.getElem_matchingInstance_pin {G : Graph} {v : ℕ} (hv : v ∈ G.vertices) : G.matchingInstance[G.distinctVertices.length + List.idxOf v G.distinctVertices] = (Logic.PL.CSP.Table.pinTable false, [2 * v + 1])

The unary false pin follows all choice constraints in distinct vertex order.

def Cslib.Complexity.Graph.choiceOccurrence (G : Graph) (v : ℕ) (hv : v ∈ G.vertices) (x : ℕ) (hx : x ∈ G.matchingScope v) : G.matchingInstance.Occurrence

The actual choice incidence of the variable x at vertex v.

@[simp]

theorem Cslib.Complexity.Graph.var_choiceOccurrence {G : Graph} (v : ℕ) (hv : v ∈ G.vertices) (x : ℕ) (hx : x ∈ G.matchingScope v) : (G.choiceOccurrence v hv x hx).var = x

Choice incidence reads its supplied original variable.

def Cslib.Complexity.Graph.pinOccurrence (G : Graph) (v : ℕ) (hv : v ∈ G.vertices) : G.matchingInstance.Occurrence

The actual false-pin incidence for the private port of v.

@[simp]

theorem Cslib.Complexity.Graph.var_pinOccurrence {G : Graph} (v : ℕ) (hv : v ∈ G.vertices) : (G.pinOccurrence v hv).var = 2 * v + 1

theorem Cslib.Complexity.Graph.pinOccurrence_false {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (v : ℕ) (hv : v ∈ G.vertices) : f (G.pinOccurrence v hv) = false

Every valid generated labeling labels each private port's pin false.

theorem Cslib.Complexity.Graph.not_selected_private {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (v : ℕ) (hv : v ∈ G.vertices) : 2 * v + 1 ∉ Logic.PL.CSP.selectedVariables f

Unary pins prevent every private unmatched port from being mutually selected.

theorem Cslib.Complexity.Graph.choice_unique {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) (v : ℕ) (hv : v ∈ G.vertices) (x y : ℕ) (hx : x ∈ G.matchingScope v) (hy : y ∈ G.matchingScope v) (hfx : f (G.choiceOccurrence v hv x hx) = true) (hfy : f (G.choiceOccurrence v hv y hy) = true) : x = y

Two true ports in one choice constraint name the same variable.

def Cslib.Complexity.Graph.positionsOfLabeling (G : Graph) (f : G.matchingInstance.OccurrenceLabeling Bool) : Finset ℕ

Original positions with both endpoint labels true.

@[simp]

theorem Cslib.Complexity.Graph.mem_positionsOfLabeling {G : Graph} (f : G.matchingInstance.OccurrenceLabeling Bool) (i : ℕ) : i ∈ G.positionsOfLabeling f ↔ i < G.edgeList.length ∧ 2 * i ∈ Logic.PL.CSP.selectedVariables f

theorem Cslib.Complexity.Graph.isMatching_positionsOfLabeling {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) : (G.matchingOfPositions (G.positionsOfLabeling f)).IsMatching

Extracting mutually selected original edges gives an actual Mathlib matching.

theorem Cslib.Complexity.Graph.selectedVariables_eq_image {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) : Logic.PL.CSP.selectedVariables f = Finset.image (fun (x : ℕ) => 2 * x) (G.positionsOfLabeling f)

Mutual selection contains only original even-tagged edges; private pins never contribute.

theorem Cslib.Complexity.Graph.card_true_matchingInstance {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) : {o : G.matchingInstance.Occurrence | f o = true}.card = G.distinctVertices.length

Every feasible generated labeling has precisely one true incidence per declared vertex.

theorem Cslib.Complexity.Graph.defects_add_two_mul_positions {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem f) : (Logic.PL.CSP.defects f).card + 2 * (G.positionsOfLabeling f).card = G.distinctVertices.length

The exact objective identity, including isolates and empty graphs.