feat(Combinatorics/SimpleGraph/Connectivity): add edge reachability and connectivity numbers by JadAbouHawili · Pull Request #42494 · leanprover-community/mathlib4

JadAbouHawili · 2026-08-06T10:35:01Z

Define edge reachability and connectivity numbers with some basic API

Partially solves #34961

…nd connectivity numbers

github-actions · 2026-08-06T10:35:16Z

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 · 2026-08-06T10:36:35Z

PR summary 526af926b9

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

+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 526af926b9
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 · 2026-08-06T12:32:33Z

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 · 2026-08-06T14:34:57Z

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

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

into graph-theory

JadAbouHawili · 2026-08-13T17:56:09Z

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.

Having [DecidableEq V] in the theorem statement is like asking the user to provide an algorithm that determines equality of inhabitants of type V , this is what made it click for me.

JadAbouHawili · 2026-08-13T17:58:36Z

Did this help? Maybe we can refine this into docs

I read the docs you linked , it seems possible to weave in what you mention into that but I don't think I'm knowledgeable enough to do that.

JadAbouHawili · 2026-08-14T11:40:10Z

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.

Having [DecidableEq V] in the theorem statement is like asking the user to provide an algorithm that determines equality of inhabitants of type V , this is what made it click for me.

After lingering on this for a bit , my impression is that for constructs that output data then you would want [DecidableEq V] in the statement so the user would have to supply the algorithm(the difference in the algorithm might result in different output) but if it were a proof of a theorem then asking the user for that doesn't make sense

SnirBroshi · 2026-08-14T11:51:24Z

Yes! Except when the algorithm is used in the statement of the theorem, such as in the Finset union example.

JadAbouHawili · 2026-08-15T11:44:48Z

Yes! Except when the algorithm is used in the statement of the theorem, such as in the Finset union example.

I guess that's for the versatility where the theorem would work for any user defined type with DecidableEq where its type polymorphism for types that implement some functionality

JadAbouHawili · 2026-08-15T11:49:30Z

I just pushed a proof for edgeConnectivity_le_minDegree but I needed to add [Nontrivial V] to get there.

Is the current work done here enough to get it merged? Or is there more I need to do , the acceptable timeline and size of work in a PR is not clear to me.

Your issue also mentions

We should probably also change IsEdgeReachable/IsEdgeConnected to accept k : ℕ∞, so that we can talk about graphs which stay connected after removing any finite amount of edges.

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

SnirBroshi · 2026-08-16T09:41:01Z

I think the current size is great! (although I don't have any authority to get things merged)

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?

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.

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

JadAbouHawili · 2026-08-16T19:22:46Z

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

SnirBroshi · 2026-08-17T17:11:50Z

+theorem IsEdgeConnected.le_minDegree [Fintype V] [Nontrivial V]
+    [DecidableRel G.Adj] (h : G.IsEdgeConnected k) :
+    k ≤ G.minDegree := le_minDegree_of_forall_le_degree G k fun _ ↦ le_degree h


Spacing

Suggested change

theorem IsEdgeConnected.le_minDegree [Fintype V] [Nontrivial V]

[DecidableRel G.Adj] (h : G.IsEdgeConnected k) :

k ≤ G.minDegree := le_minDegree_of_forall_le_degree G k fun _ ↦ le_degree h

theorem IsEdgeConnected.le_minDegree [Fintype V] [Nontrivial V] [DecidableRel G.Adj]

(h : G.IsEdgeConnected k) : k ≤ G.minDegree :=

le_minDegree_of_forall_le_degree G k fun _ ↦ le_degree h

SnirBroshi · 2026-08-17T17:14:05Z

+theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u]
+    (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u :=


Spacing

Suggested change

theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u]

(huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u :=

theorem edgeReachability_le_degree_left [Fintype <| G.neighborSet u] (huv : u ≠ v) :

G.edgeReachability u v ≤ G.degree u :=

SnirBroshi · 2026-08-17T17:14:24Z

+theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v]
+    (huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by


Spacing

Suggested change

theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v]

(huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by

theorem edgeReachability_le_degree_right [Fintype <| G.neighborSet v] (huv : u ≠ v) :

G.edgeReachability u v ≤ G.degree v := by

SnirBroshi · 2026-08-17T17:16:12Z

+  exact edgeReachability_le_degree_left huv.symm
+
+theorem edgeConnectivity_le_minDegree [Fintype V] [Nontrivial V] [DecidableRel G.Adj] :
+    G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast (IsEdgeConnected.le_minDegree h)


Suggested change

G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast (IsEdgeConnected.le_minDegree h)

G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast h.le_minDegree

SnirBroshi · 2026-08-17T17:17:27Z

+theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by
+  simpa [edgeConnectivity, IsEdgeConnected, IsEdgeReachable] using ENat.iSup_natCast
+
+theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by


Suggested change

theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by

@[simp]

theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by

and then edgeReachability_eq_top_of_subsingleton could be just simp [Subsingleton.elim u v]

SnirBroshi · 2026-08-17T17:17:54Z

+theorem IsEdgeConnected.le_edgeConnectivity (h : G.IsEdgeConnected k) : k ≤ G.edgeConnectivity :=
+  le_iSup₂ (α := ℕ∞) k h
+
+theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by


Suggested change

theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by

@[simp]

theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by

SnirBroshi · 2026-08-17T17:18:11Z

+theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by
+  simp only [edgeReachability, IsEdgeReachable.rfl, iSup_pos, ENat.iSup_natCast]
+
+theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by


Suggested change

theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by

@[simp]

theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by

SnirBroshi · 2026-08-17T17:31:19Z

+  rw [Order.one_le_iff_ne_zero.symm]
+  have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h
+  simp only [le_iSup_iff, edgeReachability]
+  intro b h'
+  specialize h' 1
+  grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff]


Suggested change

rw [Order.one_le_iff_ne_zero.symm]

have : G.IsEdgeReachable 1 u v := isEdgeReachable_one.mpr h

simp only [le_iSup_iff, edgeReachability]

intro b h'

specialize h' 1

grind [isEdgeReachable_one, Nat.cast_one, iSup_le_iff]

simpa [← Order.one_le_iff_ne_zero] using isEdgeReachable_one.mpr h |>.le_edgeReachability

(requires moving this theorem below IsEdgeReachable.le_edgeReachability)

feat(Combinatorics/SimpleGraph/Connectivity): add edge reachability a…

4c562de

…nd connectivity numbers

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 6, 2026

[pre-commit.ci lite] apply automatic fixes

deb56a0

JadAbouHawili and others added 3 commits August 6, 2026 13:42

remove file from scripts

facdcae

Merge branch 'master' into graph-theory

92ce84a

Ring

a4a5e41

JadAbouHawili added 2 commits August 6, 2026 17:46

fix ci

56d3f93

remove docstring changes

8aede9b

SnirBroshi reviewed Aug 6, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 6, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 6, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

JadAbouHawili and others added 4 commits August 6, 2026 18:33

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivit…

78bffa5

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

golfed

87ac82c

Merge branch 'graph-theory' of https://github.com/JadAbouHawili/mathlib4

ca41347

into graph-theory

[pre-commit.ci lite] apply automatic fixes

4313ee3

SnirBroshi reviewed Aug 6, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

SnirBroshi reviewed Aug 6, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

JadAbouHawili added 4 commits August 7, 2026 23:22

simp suggestion

25576b7

Merge branch 'graph-theory' of https://github.com/JadAbouHawili/mathlib4

3ba9b38

into graph-theory

shorter proof

7e49347

fixed spacing

19af63a

SnirBroshi reviewed Aug 7, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 7, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

SnirBroshi reviewed Aug 7, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 7, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

new theorems and doc strings

7015c33

JadAbouHawili and others added 2 commits August 13, 2026 19:45

start ci

a0561a4

Merge branch 'master' into graph-theory

2a02712

edgeconnectivity_le_mindegree

3b6fd35

JadAbouHawili requested a review from SnirBroshi August 15, 2026 12:10

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

SnirBroshi reviewed Aug 16, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated

JadAbouHawili and others added 9 commits August 16, 2026 21:06

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivit…

9dd49c0

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivit…

af7a0ac

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

remove notedgereachable

62e56ff

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivit…

1801937

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivit…

cb2499b

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

Update Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivit…

07809f5

…y.lean Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>

extracting lemma

04a1172

lemma

1d0f6ac

todo solution moved to another PR

9eb8d62

Merge branch 'master' into graph-theory

526af92

SnirBroshi reviewed Aug 17, 2026

View reviewed changes

		theorem edgeReachability_le_degree_left [Fintype <\| G.neighborSet u]
		(huv : u ≠ v) : G.edgeReachability u v ≤ G.degree u :=

		theorem edgeReachability_le_degree_right [Fintype <\| G.neighborSet v]
		(huv : u ≠ v) : G.edgeReachability u v ≤ G.degree v := by

	G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast (IsEdgeConnected.le_minDegree h)
	G.edgeConnectivity ≤ G.minDegree := iSup₂_le fun _ h ↦ mod_cast h.le_minDegree

	theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by
	@[simp]
	theorem edgeReachability_self : G.edgeReachability v v = ⊤ := by

	theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by
	@[simp]
	theorem edgeConnectivity_eq_top_of_subsingleton [Subsingleton V] : G.edgeConnectivity = ⊤ := by

	theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by
	@[simp]
	theorem edgeReachability_eq_top_of_subsingleton [Subsingleton V] : G.edgeReachability u v = ⊤ := by

Uh oh!

Conversation

JadAbouHawili commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Aug 6, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 526af926b9

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

SnirBroshi commented Aug 6, 2026

Uh oh!

JadAbouHawili commented Aug 6, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

JadAbouHawili commented Aug 13, 2026

Uh oh!

JadAbouHawili commented Aug 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JadAbouHawili commented Aug 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SnirBroshi commented Aug 14, 2026

Uh oh!

JadAbouHawili commented Aug 15, 2026

Uh oh!

JadAbouHawili commented Aug 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SnirBroshi commented Aug 16, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

JadAbouHawili commented Aug 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

JadAbouHawili commented Aug 6, 2026 •

edited

Loading

github-actions Bot commented Aug 6, 2026 •

edited

Loading

JadAbouHawili commented Aug 13, 2026 •

edited

Loading

JadAbouHawili commented Aug 14, 2026 •

edited

Loading

JadAbouHawili commented Aug 15, 2026 •

edited

Loading

JadAbouHawili commented Aug 16, 2026 •

edited

Loading