Complete unweighted matching correctness

Maximum output is optimal against every actual Mathlib matching, with no supplied solver, model or runtime hypothesis. Successful perfect search returns exactly the original edge pairs of a perfect Mathlib subgraph; decision is equivalent to existence of a perfect matching. All claims use the normalized existing Graph.induced convention on every raw graph.

theorem Cslib.Complexity.Graph.isMaximumMatching_positionsOfLabeling {G : Graph} {f : G.matchingInstance.OccurrenceLabeling Bool} (hf : Logic.PL.CSP.IsOptimalLabeling Logic.PL.CSP.Table.sem f) : (G.matchingOfPositions (G.positionsOfLabeling f)).IsMaximumMatching

Minimum defect is maximum cardinality among all actual graph matchings.

theorem Cslib.Complexity.Graph.matchingPositions_toFinset (G : Graph) (bits : List Bool) : (G.matchingPositions bits).toFinset = G.positionsOfLabeling (CSP.EdgeAugmenting.labeling G.matchingInstance bits)

The executable position scan is exactly the semantic mutually selected edge set.

theorem Cslib.Complexity.Graph.maximumMatchingSubgraph_isMaximumMatching (G : Graph) : G.maximumMatchingSubgraph.IsMaximumMatching

The total algorithm returns a Mathlib maximum matching on every raw input.

theorem Cslib.Complexity.Graph.maximumMatchingPositions_lt {G : Graph} {i : ℕ} (hi : i ∈ G.maximumMatchingPositions) : i < G.edgeList.length

Every returned position names an actual normalized original edge.

theorem Cslib.Complexity.Graph.nodup_maximumMatchingPositions (G : Graph) : G.maximumMatchingPositions.Nodup

Returned canonical positions never repeat.

theorem Cslib.Complexity.Graph.of_mem_maximumMatching {G : Graph} {e : ℕ × ℕ} (he : e ∈ G.maximumMatching) : e ∈ G.edges ∧ e.1 ≠ e.2 ∧ e.1 ∈ G.vertices ∧ e.2 ∈ G.vertices

Every returned edge is an original edge between distinct declared vertices.

theorem Cslib.Complexity.Graph.maximumMatching_eq_edgesAtPositions (G : Graph) : G.maximumMatching = G.edgesAtPositions G.maximumMatchingPositions

The public edge pairs are precisely the executable conversion of returned positions.

theorem Cslib.Complexity.Graph.length_maximumMatching (G : Graph) : G.maximumMatching.length = G.maximumMatchingSubgraph.edgeSet.ncard

The number of returned original edge pairs is the actual subgraph's edge cardinality.

theorem Cslib.Complexity.Graph.maximumMatching_cardinality (G : Graph) (M : G.induced.Subgraph) (hM : M.IsMatching) : M.edgeSet.ncard ≤ G.maximumMatching.length

Maximum output is as large as every actual matching, including matchings with no extension of the particular returned edges.

theorem Cslib.Complexity.Graph.mem_verts_matchingOfPositions_iff {G : Graph} {S : Finset ℕ} (hS : ∀ i ∈ S, i < G.edgeList.length) (v : ℕ) (hv : v ∈ G.vertices) : ⟨v, hv⟩ ∈ (G.matchingOfPositions S).verts ↔ ∃ i ∈ S, incident (G.edgeList.getD i (0, 0)) v = true

Covered vertices of valid position sets are exactly the endpoints of selected original edges.

theorem Cslib.Complexity.Graph.coversVertices_maximumMatching (G : Graph) : G.coversVertices G.maximumMatching = true ↔ G.maximumMatchingSubgraph.IsSpanning

The executable coverage scan is exactly spanning of the returned Mathlib subgraph.

theorem Cslib.Complexity.Graph.maximumMatchingSubgraph_isSpanning_iff (G : Graph) : G.maximumMatchingSubgraph.IsSpanning ↔ ∃ (M : G.induced.Subgraph), M.IsPerfectMatching

A maximum matching spans exactly when any perfect matching exists.

theorem Cslib.Complexity.Graph.perfectMatching_spec {G : Graph} {edges : List (ℕ × ℕ)} (h : G.perfectMatching = some edges) : edges = G.maximumMatching ∧ G.maximumMatchingSubgraph.IsPerfectMatching

Complete successful perfect-search specification in the existing Mathlib subgraph model.

theorem Cslib.Complexity.Graph.decidePerfectMatching_eq_true (G : Graph) : G.decidePerfectMatching = true ↔ ∃ (M : G.induced.Subgraph), M.IsPerfectMatching

Complete perfect decision, including normalization, empty graphs and isolates.

theorem Cslib.Complexity.Graph.perfectMatching_eq_none_iff (G : Graph) : G.perfectMatching = none ↔ ¬∃ (M : G.induced.Subgraph), M.IsPerfectMatching

Search fails exactly when the actual induced graph has no perfect matching.

theorem Cslib.Complexity.Graph.maximumMatchingSubgraph_adj_iff (G : Graph) (u v : { v : ℕ // v ∈ G.vertices }) : G.maximumMatchingSubgraph.Adj u v ↔ (↑u, ↑v) ∈ G.maximumMatching ∨ (↑v, ↑u) ∈ G.maximumMatching

The returned original endpoint pairs are exactly the edges of the certified subgraph.