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 8d6de37e7b

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)	573
Mathlib.Combinatorics.SimpleGraph.Connectivity.VertexConnectivity (new file)	775

---

Declarations diff

+ Adj.isVertexReachable
+ IsVertexConnected
+ IsVertexConnected.anti
+ IsVertexConnected.mono
+ IsVertexConnected.zero
+ IsVertexPreconnected
+ IsVertexPreconnected.anti
+ IsVertexPreconnected.mono
+ IsVertexPreconnected.top
+ IsVertexPreconnected.zero
+ IsVertexReachable
+ IsVertexReachable.anti
+ IsVertexReachable.mono
+ IsVertexReachable.of_adj
+ IsVertexReachable.reachable
+ IsVertexReachable.refl
+ IsVertexReachable.symm
+ IsVertexReachable.zero
+ Preconnected.isVertexConnected_one
+ Preconnected.isVertexPreconnected_one
+ isVertexConnected_one
+ isVertexConnected_top
+ isVertexConnected_zero
+ isVertexPreconnected_one
+ isVertexReachable_comm
+ isVertexReachable_one_iff
+ isolateVerts
+ isolateVerts_bot
+ isolateVerts_empty
+ isolateVerts_le
+ isolateVerts_singleton

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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]

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).

[0xTerencePrime]

-awaiting-author

Addressed the latest feedback. (Sorry for the delay, was away for the Lunar New Year break!)

[SnirBroshi]

Suggested change

	Iff.mpr SimpleGraph.isVertexConnected_one ⟨‹_›, h⟩
	isVertexConnected_one.mpr ⟨‹_›, h⟩

[0xTerencePrime]

Done, but kept the SimpleGraph. prefix. Without it, Lean attempts name resolution to the lemma currently being defined, resulting in a recursive call error.

[SproutSeeds]

Hi @0xTerencePrime, thank you for all the work here. I realized my later PR #36063 overlapped with this one, that was my mistake. I have closed #36063 so review can stay focused here. If useful, I would be very happy to co-own and help with follow-up commits in your preferred shape, or take a specific TODO you pick.

[YaelDillies]

Will isolateVerts be useful anywhere else? I suspect not. My preference would be to instead wait for the simple graph support refactor to land and subsequently use induce instead of isolateVerts. This is the approach I have taken in ProofBench.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[0xTerencePrime]

I apologize for being MIA over the last two months! I got caught up in busyness on my end and just didn't have the bandwidth to come back to this until now.

@YaelDillies Regarding isolateVerts, I totally agree that it will become redundant once induce is added. As the graph-on-a-set refactor is still to be done, I have added a nice big TODO to isolateVerts.lean pointing out that it will be dropped in favour of induce, and the file later deleted. Can this be okay as a short-term helper so we can get these vertex-connectivity preliminaries in now?

In the most recent commits, I have also merged in the latest master changes, included the missing isVertexConnected_top lemma, corrected the docstring indentation, and eliminated the GRewrite tactic dependency from the proof of IsVertexConnected.anti.

Thanks for your additional patience and reviews again, @SnirBroshi!

[0xTerencePrime]

-awaiting-author

applied all suggestions from the latest review. removed the redundant GRewrite import too

[SnirBroshi]

Thanks!