Comparison labelings for every actual matching

A comparison witness chooses the incident matching edge at a covered vertex and the private unmatched port otherwise. Classical selection here is confined to the mathematical comparison with arbitrary Mathlib subgraphs. The executable endpoints use only the certified optimizer.

theorem Cslib.Complexity.Graph.mem_verts_of_incident_positions {G : Graph} {M : G.induced.Subgraph} {v i : ℕ} (hv : v ∈ G.vertices) (hi : i ∈ positions M) (hinc : incident (G.edgeList.getD i (0, 0)) v = true) : ⟨v, hv⟩ ∈ M.verts

An incident selected subgraph edge certifies that its endpoint belongs to the subgraph.

theorem Cslib.Complexity.Graph.positions_unique {G : Graph} {M : G.induced.Subgraph} (hM : M.IsMatching) (v : ℕ) (hv : v ∈ G.vertices) (i : ℕ) (hi : i ∈ positions M) (j : ℕ) (hj : j ∈ positions M) (hinc : incident (G.edgeList.getD i (0, 0)) v = true) (hinc' : incident (G.edgeList.getD j (0, 0)) v = true) : i = j

A Mathlib matching contains at most one incident edge position per vertex.

noncomputable def Cslib.Complexity.Graph.comparisonPort (G : Graph) (S : Finset ℕ) (v : ℕ) : ℕ

A proof-only comparison port: an incident position of S, or the private port at zero.

theorem Cslib.Complexity.Graph.comparisonPort_lt (G : Graph) (S : Finset ℕ) (v : ℕ) : G.comparisonPort S v < (G.matchingScope v).length

Every comparison port belongs to the nonempty actual choice scope.

theorem Cslib.Complexity.Graph.comparisonPort_eq {G : Graph} {M : G.induced.Subgraph} (hM : M.IsMatching) (v : ℕ) (hv : v ∈ G.vertices) (i : ℕ) (hi : i ∈ positions M) (hinc : incident (G.edgeList.getD i (0, 0)) v = true) : G.comparisonPort (positions M) v = List.idxOf (2 * i) (G.matchingScope v)

At an actual matching edge, uniqueness forces the comparison to choose that edge.

noncomputable def Cslib.Complexity.Graph.comparisonLabeling (G : Graph) (S : Finset ℕ) : G.matchingInstance.OccurrenceLabeling Bool

A feasible proof-only labeling, choosing exactly one port per vertex and false at pins.

theorem Cslib.Complexity.Graph.comparisonLabeling_valid (G : Graph) (S : Finset ℕ) : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (G.comparisonLabeling S)

Every comparison labeling is feasible, independently of consistency or cardinality.

theorem Cslib.Complexity.Graph.positions_subset_comparison {G : Graph} {M : G.induced.Subgraph} (hM : M.IsMatching) : positions M ⊆ G.positionsOfLabeling (G.comparisonLabeling (positions M))

The comparison for a matching selects each of its original graph edges at both endpoints.