Matching as minimum-defect edge CSP

Each distinct declared vertex chooses exactly one incident edge or its private unmatched port. Original edges use the even names 2 * i, where i is their normalized edge-list position; the private port of a vertex named v uses 2 * v + 1. A second unary constraint pins each private port false. Every scope is nonempty, including isolated vertices. Names are retained in binary; no interval below a raw vertex name is enumerated.

Mutually true original edges form a matching. Counting true endpoints gives 2 * matched edges + defects = distinct vertices, so minimizing defects maximizes matching cardinality. The solver is the even-delta-matroid algorithm of [KKR18].

def Cslib.Complexity.Graph.matchingScope (G : Graph) (v : ℕ) : List ℕ

Nonempty choice scope: one private unmatched port and the incident normalized edges.

def Cslib.Complexity.Graph.matchingInstance (G : Graph) : Logic.PL.CSP Logic.PL.CSP.Table ℕ

An exactly-one choice at every vertex, with every private unmatched port pinned false. This instance always has a valid local labeling; consistency is not required by optimization.

theorem Cslib.Complexity.Graph.mem_matchingScope_even (G : Graph) (v i : ℕ) : 2 * i ∈ G.matchingScope v ↔ i < G.edgeList.length ∧ incident (G.edgeList.getD i (0, 0)) v = true

An original edge belongs to a choice scope precisely at its two original endpoints.

theorem Cslib.Complexity.Graph.mem_matchingScope_odd (G : Graph) (v w : ℕ) : 2 * w + 1 ∈ G.matchingScope v ↔ w = v

An unmatched port appears in exactly its own vertex's choice scope.

theorem Cslib.Complexity.Graph.nodup_matchingScope (G : Graph) (v : ℕ) : (G.matchingScope v).Nodup

All generated choice scopes are duplicate-free, for arbitrary raw graph data.

theorem Cslib.Complexity.Graph.count_vars_matchingInstance_even (G : Graph) (i : ℕ) : List.count (2 * i) G.matchingInstance.vars = List.count i G.perfectMatchingInstance.vars

Original edge positions have the same occurrence count under even tagging.

theorem Cslib.Complexity.Graph.count_vars_matchingInstance_odd (G : Graph) (w : ℕ) : List.count (2 * w + 1) G.matchingInstance.vars = if w ∈ G.vertices then 2 else 0

Each declared vertex's private port occurs exactly twice.

theorem Cslib.Complexity.Graph.mem_vars_matchingInstance (G : Graph) {x : ℕ} : x ∈ G.matchingInstance.vars ↔ (∃ i < G.edgeList.length, x = 2 * i) ∨ ∃ v ∈ G.vertices, x = 2 * v + 1

Every generated variable is an original edge position or a declared private port.

theorem Cslib.Complexity.Graph.edgeInstance_matchingInstance (G : Graph) : G.matchingInstance.EdgeInstance

The optimizer's two-occurrence guard follows internally on every raw graph.

theorem Cslib.Complexity.Graph.evenConstraints_matchingInstance (G : Graph) : Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem G.matchingInstance

Each generated relation is a nonempty even delta-matroid on its actual scope positions.