feat(Combinatorics/SimpleGraph/Connectivity): add edge reachability and connectivity numbers

[JadAbouHawili]

Define edge reachability and connectivity numbers with some basic API

Partially solves #34961

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary aa9e05e6db

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity	799	811	+12 (+1.50%)

Import changes for all files

Files	Import difference
3 files Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Star	1
Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity Mathlib.Combinatorics.SimpleGraph.Hamiltonian	12

---

Declarations diff (regex)

+ IsEdgeConnected.le_edgeConnectivity
+ IsEdgeConnected.le_minDegree
+ IsEdgeReachable.le_edgeReachability
+ Reachable.edgeReachability_ne_zero
+ edgeConnectivity
+ edgeConnectivity_eq_top_of_subsingleton
+ edgeConnectivity_le_edgeReachability
+ edgeConnectivity_le_minDegree
+ edgeReachability
+ edgeReachability_comm
+ edgeReachability_eq_top_of_subsingleton
+ edgeReachability_le_degree_left
+ edgeReachability_le_degree_right
+ edgeReachability_self

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit aa9e05e).

• +14 new declarations
• −0 removed declarations

+SimpleGraph.IsEdgeConnected.le_edgeConnectivity
+SimpleGraph.IsEdgeConnected.le_minDegree
+SimpleGraph.IsEdgeReachable.le_edgeReachability
+SimpleGraph.Reachable.edgeReachability_ne_zero
+SimpleGraph.edgeConnectivity
+SimpleGraph.edgeConnectivity_eq_top_of_subsingleton
+SimpleGraph.edgeConnectivity_le_edgeReachability
+SimpleGraph.edgeConnectivity_le_minDegree
+SimpleGraph.edgeReachability
+SimpleGraph.edgeReachability_comm
+SimpleGraph.edgeReachability_eq_top_of_subsingleton
+SimpleGraph.edgeReachability_le_degree_left
+SimpleGraph.edgeReachability_le_degree_right
+SimpleGraph.edgeReachability_self

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit aa9e05e6db
Reference commit a7cadaedd7

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

[SnirBroshi]

Welcome!

Could you disclose if and how you're using LLMs, per the AI guidelines?

Also this PR contains a bunch of unrelated changes to docstrings; could you remove them or move them into separate PRs?

[JadAbouHawili]

No LLMS used , I'll move the docstring changes to separate PRs

[JadAbouHawili]

Should I go for that at this point or would that be in another PR after this one gets merged?

I think it should be separate, but it could be independent from this PR, no?

At first I thought it might cause merge conflicts with this PR but that's not the case. So i would change IsEdgeReachable and IsEdgeConnected to take k : ENat and that wouldn't affect anything in this PR (edgeReachability and edgeConnectivity would work as is). It would be independent without the theorems you just added to #34961 , I'll make a dependent PR working on that

btw I think we should also have theorems relating homomorphisms & isomorphisms to these numbers (e.g. isomorphic graphs have the same edge connectivity), but they could be added in a later PR.

sounds like another dependent PR I'll work on.

Regarding the work in this PR towards resolving #34961 , I've proved all the things I could handle and don't have anything to add. I wasn't able to figure out edgeConnectivity_eq_iInf₂ , exists_edgeReachability_eq_edgeConnectivity. If you know how to prove them , I don't know if there's a way for you to push them to this PR and then we would share the credit somehow.

Regardless , I'm going to move onto working on the dependent PRs.

Thanks for the reviews , I learned alot and hopefully future contributions will go smoother and with lesser mistakes.

future work:
#42839

[grunweg]

but didn't find docs explaining it

Unfortunately it seems that there aren't any, other than this but it's not very illuminating.

Basically a [DecidableEq α] hypothesis is asking for an algorithm to determine when two values of type α are equal. However since we're using classical logic, every type has such an algorithm. If the statement of your theorem doesn't use the algorithm, but the proof does, there's no reason to ask the user of the theorem to provide such an algorithm; of course they could also use classical logic to conjure up any algorithm, but that should be the responsibility of your proof.

On the other hand, if you have a statement which does use the algorithm, for example Finset.mem_union which needs an equality algorithm in order to compute the union of two sets (to discard duplicates), then you might ask why not also use classical logic to conjure up an algorithm and use it in the statement?

open scoped Classical in -- this automatically uses classical logic whenever `DecidableEq` is needed
theorem Finset.mem_union' {α : Type*} {s t : Finset α} {a : α} : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t := by
  simp

The answer is that users might have their own custom DecidableEq α for their type (e.g. Nat & Bool have one) and they might want to use your theorem, but you've only proven it for Finset unions that use the other algorithm and not "for any DecidableEq α algorithm, ...".

See also diamonds.

Did this help? Maybe we can refine this into docs

By the way: I think such an explanation is great, and I would like to strongly encourage you to write this up somewhere. (Even "anywhere reasonable" and then linking to it from the docs overview would be an improvement.)

[SnirBroshi]

Thanks! I've posted on #mathlib4 > Mathlib: the Missing Manuals @ 💬 and hopefully things will take off from there