feat(Combinatorics/SimpleGraph/Connectivity): define vertex connectivity

[0xTerencePrime]

This PR introduces the foundations of vertex connectivity for simple graphs, providing a counterpart to the edge connectivity theory in #32870.

Main definitions

• SimpleGraph.IsVertexReachable: vertices remain reachable after removing strictly fewer than k other vertices.
• SimpleGraph.IsVertexConnected: a graph is k-vertex-connected if its order is strictly greater than k and any two distinct vertices are k-vertex-reachable.

Includes basic characterizations for $k=0$ and $k=1$, along with monotonicity lemmas (anti and mono).

[github-actions]

PR summary 2131653357

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.SimpleGraph.IsolateVerts (new file)	353
Mathlib.Combinatorics.SimpleGraph.Connectivity.VertexConnectivity (new file)	592

---

Declarations diff

+ Adj.isVertexReachable
+ IsVertexConnected
+ IsVertexConnected.anti
+ IsVertexConnected.mono
+ IsVertexConnected.zero
+ IsVertexReachable
+ IsVertexReachable.anti
+ IsVertexReachable.mono
+ IsVertexReachable.of_adj
+ IsVertexReachable.reachable
+ IsVertexReachable.refl
+ IsVertexReachable.symm
+ IsVertexReachable.zero
+ isVertexConnected_one
+ isVertexConnected_top
+ isVertexConnected_zero
+ isVertexReachable_one_iff
+ isVertexReachable_symm
+ isolateVerts
+ isolateVerts_bot
+ isolateVerts_empty
+ isolateVerts_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vihdzp]

Thank you! Here's some suggestions.

[0xTerencePrime]

All suggestions implemented, thanks!

[SnirBroshi]

Thanks for doing this!

General question: Should we keep the condition on the number of vertices for IsVertexConnected? It agrees with Wikipedia but it feels like another case of #31690 where this requirement isn't particularly helpful

[0xTerencePrime]

Thanks for doing this!

General question: Should we keep the condition on the number of vertices for IsVertexConnected? It agrees with Wikipedia but it feels like another case of #31690 where this requirement isn't particularly helpful

Regarding the condition on the number of vertices, I followed your suggestion and implemented the refactor to use k + 1 ≤ ENat.card V. This aligns with the philosophy of #31690 by removing unnecessary restrictions and naturally supports infinite graphs.

[vihdzp]

I'm of the general idea that if a predicate "P and Q" still largely makes without Q, then it's easier to remove the condition and add it back when needed, than it is to keep it and try to awkwardly remove it later.

[SnirBroshi]

Please avoid force-pushing, I now have no idea what changed between the version I reviewed and the current version.
I don't see an easy way to view it on GitHub, I might be able to git diff locally somehow.

[0xTerencePrime]

sorry about the force-pushes. i've pushed new commits now addressing the review comments, including the refactors and the missing zero lemma.

[SnirBroshi]

Thanks!

[SnirBroshi]

Suggested change

	lemma isVertexReachable_one_iff :
	G.IsVertexReachable 1 u v ↔ G.Reachable u v := by
	constructor
	· exact fun h ↦ h.reachable (by simp)
	· rintro h s hs hu hv
	rw [ENat.lt_one_iff_eq_zero, Set.encard_eq_zero] at hs
	rw [hs, isolateVerts_empty]
	exact h
	@[simp]
	lemma isVertexReachable_one_iff : G.IsVertexReachable 1 u v ↔ G.Reachable u v := by
	refine ⟨(·.reachable one_ne_zero), fun h s hs hu hv ↦ ?_⟩
	rwa [Set.encard_eq_zero.mp <| ENat.lt_one_iff_eq_zero.mp hs, isolateVerts_empty]

[SnirBroshi]

Suggested change

	lemma isVertexConnected_one :
	G.IsVertexConnected 1 ↔ Nontrivial V ∧ G.Connected := by
	rw [IsVertexConnected, ENat.add_one_le_iff (by simp), ENat.one_lt_card_iff_nontrivial]
	constructor
	· rintro ⟨h_nt, h_reach⟩
	refine ⟨h_nt, ?_⟩
	haveI : Nontrivial V := h_nt
	exact {
	nonempty := inferInstance
	preconnected := fun u v ↦ (h_reach u v).reachable (by simp)
	}
	· rintro ⟨h_nt, h_conn⟩
	exact ⟨h_nt, fun u v ↦ isVertexReachable_one_iff.mpr (h_conn.preconnected u v)⟩
	lemma isVertexConnected_one : G.IsVertexConnected 1 ↔ Nontrivial V ∧ G.Connected := by
	rw [IsVertexConnected, ENat.add_one_le_iff ENat.one_ne_top, ENat.one_lt_card_iff_nontrivial]
	refine ⟨fun ⟨h_nt, h_reach⟩ ↦ ⟨h_nt, ⟨fun u v ↦ ?_⟩⟩, fun ⟨h_nt, h_conn⟩ ↦ ⟨h_nt, fun u v ↦ ?_⟩⟩
	exacts [isVertexReachable_one_iff.mp <| h_reach u v, isVertexReachable_one_iff.mpr <| h_conn u v]

[SnirBroshi]

Can you also add the right-to-left version with a weaker Perconnected hypothesis?

lemma Preconnected.isVertexConnected_one [Nontrivial V] (h : G.Preconnected) :
    G.IsVertexConnected 1 :=
  G.isVertexConnected_one.mpr ⟨‹_›, ⟨h⟩⟩

[SnirBroshi]

I don't see why add_le_add_left is problematic as you've said, it works for me locally

Suggested change

	lemma IsVertexConnected.anti (hkl : l ≤ k) (hc : G.IsVertexConnected k) :
	G.IsVertexConnected l :=
	⟨by exact (add_le_add hkl le_rfl).trans hc.1, fun u v ↦ (hc.2 u v).anti hkl⟩
	lemma IsVertexConnected.anti (hkl : l ≤ k) (hc : G.IsVertexConnected k) : G.IsVertexConnected l :=
	⟨(add_le_add_left hkl 1).trans hc.1, fun u v ↦ (hc.2 u v).anti hkl⟩

[SnirBroshi]

Suggested change

	lemma IsVertexConnected.mono (hGH : G ≤ H) (hc : G.IsVertexConnected k) :
	H.IsVertexConnected k :=
	lemma IsVertexConnected.mono (hGH : G ≤ H) (hc : G.IsVertexConnected k) : H.IsVertexConnected k :=

[SnirBroshi]

Suggested change

	lemma isVertexConnected_top [Fintype V] [Nonempty V] :
	(⊤ : SimpleGraph V).IsVertexConnected (Fintype.card V - 1) := by
	constructor
	· rw [ENat.card_eq_coe_fintype_card]
	norm_cast
	exact Nat.sub_add_cancel Fintype.card_pos |>.le
	· intro u v
	by_cases h : u = v
	· subst h; exact .refl _
	· exact IsVertexReachable.of_adj _ h
	lemma isVertexConnected_top [Fintype V] [Nonempty V] :
	(⊤ : SimpleGraph V).IsVertexConnected (Fintype.card V - 1) := by
	refine ⟨?_, fun u v ↦ ?_⟩
	· rw [ENat.card_eq_coe_fintype_card]
	exact_mod_cast Nat.sub_add_cancel Fintype.card_pos |>.le
	· by_cases h : u = v
	exacts [h ▸ .refl _, .of_adj _ h]

[SnirBroshi]

Continuing the discussion of whether to keep the condition on the number of vertices for IsVertexConnected, I found out that Wikipedia says this about a biconnected graph:

The property of being 2-connected is equivalent to biconnectivity, except that the complete graph of two vertices is usually not regarded as 2-connected.

So with the current version we'd need a separate definition for biconnectivity, but if we remove the first part of IsVertexConnected we'll have it as G.IsVertexConnected 2 (∀ u v, G.IsVertexReachable 2 u v isn't so bad, but the former is easier to loogle).