Reconstruction Conjecture — Separator/degree bridge lemmas

This module collects small bridge lemmas connecting the instance-free structural predicates of Reconstruction.Separator to the finite, degree-based vocabulary used by the deck-reconstruction machinery.

Main results

• SimpleGraph.IsUniversal.map — universal vertices are isomorphism invariants.
• SimpleGraph.minDegreeTwo_iff — the combinatorial MinDegreeTwo predicate is equivalent to "every vertex has degree at least 2".
• SimpleGraph.isUniversal_complete — every vertex of the complete graph is universal.

theorem SimpleGraph.IsUniversal.map {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) {v : V} (h : G.IsUniversal v) : H.IsUniversal (e v)

Universal vertices are isomorphism invariants. If v is adjacent to every other vertex of G and e : G ≃g H, then e v is adjacent to every other vertex of H. For y ≠ e v we have e.symm y ≠ v, so G.Adj v (e.symm y), which transports across e.

theorem SimpleGraph.minDegreeTwo_iff {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.MinDegreeTwo ↔ ∀ (v : V), 2 ≤ G.degree v

MinDegreeTwo is the degree-≥-2 condition. The instance-free predicate "every vertex has two distinct neighbours" is equivalent to "every vertex has degree at least 2", via the cardinality of the neighbour finset.

theorem SimpleGraph.isUniversal_complete {V : Type u_1} (v : V) : ⊤.IsUniversal v

Every vertex of the complete graph is universal. In ⊤, distinct vertices are always adjacent, so each vertex is adjacent to every other.

theorem SimpleGraph.minDegreeTwo_complete {V : Type u_1} [Fintype V] (hV : 3 ≤ Fintype.card V) : ⊤.MinDegreeTwo

The complete graph has minimum degree ≥ 2 once it has ≥ 3 vertices. Each vertex has every other vertex as a neighbour, so with at least three vertices in total there are two distinct neighbours.