Edge positions in framed graphs

Graph.edgeList enumerates the edges of the existing Graph.induced, discarding loops, undeclared endpoints and repeated edges in either orientation. positions and ofPositions relate edge positions to Mathlib subgraphs. The latter is spanning, so incomplete matchings must restrict its vertex set to their covered vertices.

These declarations and proofs were extracted from Graph.PerfectMatching for constructive matching algorithms, preserving the original public names and normalization conventions. cover_positions now also applies at each covered vertex of an incomplete matching. exists_getD_edgeList_of_adj supplies a valid edge position directly from adjacency, so coverage, edge-cardinality and legacy counting proofs share the same orientation witness.

def Cslib.Complexity.Graph.edgeList (G : Graph) : List (ℕ × ℕ)

The edges of G.induced, each listed once: the edges of G between distinct declared vertices, with repetitions in either orientation erased.

def Cslib.Complexity.Graph.incident (e : ℕ × ℕ) (v : ℕ) : Bool

Whether the vertex v is an end of the edge e.

The edge list

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

An entry of the edge list joins two distinct declared vertices by an edge of G.

theorem Cslib.Complexity.Graph.exists_mem_edgeList {G : Graph} {u v : { v : ℕ // v ∈ G.vertices }} (h : G.induced.Adj u v) : (↑u, ↑v) ∈ G.edgeList ∨ (↑v, ↑u) ∈ G.edgeList

Each edge of G.induced is in the edge list in one of its orientations.

theorem Cslib.Complexity.Graph.pairwise_edgeList (G : Graph) : List.Pairwise (fun (a b : ℕ × ℕ) => b ≠ a ∧ b ≠ a.swap) G.edgeList

No entry of the edge list repeats an earlier entry, in either orientation.

theorem Cslib.Complexity.Graph.eq_of_getD_edgeList {G : Graph} {i j : ℕ} (hi : i < G.edgeList.length) (hj : j < G.edgeList.length) (h : G.edgeList.getD i (0, 0) = G.edgeList.getD j (0, 0) ∨ G.edgeList.getD i (0, 0) = (G.edgeList.getD j (0, 0)).swap) : i = j

Distinct positions of the edge list hold distinct edges, in either orientation.

theorem Cslib.Complexity.Graph.getD_edgeList_mem {G : Graph} {i : ℕ} (hi : i < G.edgeList.length) : G.edgeList.getD i (0, 0) ∈ G.edgeList

An entry of the edge list, read at a position below its length.

theorem Cslib.Complexity.Graph.exists_getD_edgeList {G : Graph} {e : ℕ × ℕ} (he : e ∈ G.edgeList) : ∃ i < G.edgeList.length, G.edgeList.getD i (0, 0) = e

The position of an entry of the edge list.

theorem Cslib.Complexity.Graph.exists_getD_edgeList_of_adj {G : Graph} {u v : { v : ℕ // v ∈ G.vertices }} (h : G.induced.Adj u v) : ∃ i < G.edgeList.length, G.edgeList.getD i (0, 0) = (↑u, ↑v) ∨ G.edgeList.getD i (0, 0) = (↑v, ↑u)

Every actual adjacency has a retained edge position, in one of its two orientations.

def Cslib.Complexity.Graph.AdjNat {G : Graph} (M : G.induced.Subgraph) (u w : ℕ) : Prop

The adjacency of a subgraph of G.induced, read on natural numbers.

noncomputable def Cslib.Complexity.Graph.positions {G : Graph} (M : G.induced.Subgraph) : Finset ℕ

The positions of the edges of a subgraph.

theorem Cslib.Complexity.Graph.mem_positions {G : Graph} {M : G.induced.Subgraph} {i : ℕ} : i ∈ positions M ↔ i < G.edgeList.length ∧ AdjNat M (G.edgeList.getD i (0, 0)).1 (G.edgeList.getD i (0, 0)).2

Position membership is original subgraph adjacency at a valid normalized edge.

def Cslib.Complexity.Graph.ofPositions (G : Graph) (S : Finset ℕ) : G.induced.Subgraph

The subgraph spanned by the edges at a set of positions.

theorem Cslib.Complexity.Graph.exists_other_end {e : ℕ × ℕ} {v : ℕ} (hv : incident e v = true) : ∃ (w : ℕ), e = (v, w) ∨ e = (w, v)

The other end of an edge at a vertex v.

theorem Cslib.Complexity.Graph.isPerfectMatching_ofPositions {G : Graph} {S : Finset ℕ} (hS : ∀ i ∈ S, i < G.edgeList.length) (hcov : ∀ v ∈ G.vertices, ∃! i : ℕ, i < G.edgeList.length ∧ incident (G.edgeList.getD i (0, 0)) v = true ∧ i ∈ S) : (G.ofPositions S).IsPerfectMatching

Exactly one selected incident edge at every declared vertex gives a perfect matching.

theorem Cslib.Complexity.Graph.cover_positions {G : Graph} {M : G.induced.Subgraph} (hM : M.IsMatching) (v : ℕ) (hv : v ∈ G.vertices) : ⟨v, hv⟩ ∈ M.verts → ∃! i : ℕ, i < G.edgeList.length ∧ incident (G.edgeList.getD i (0, 0)) v = true ∧ i ∈ positions M

A covered vertex of any matching has exactly one incident original edge position.