[Merged by Bors] - feat(Combinatorics/SimpleGraph): define edge-connectivity by 0xTerencePrime · Pull Request #32870 · leanprover-community/mathlib4

0xTerencePrime · 2025-12-14T11:00:23Z

This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing #31691.

Summary

This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing #31691.

Main Changes

New file: Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

Definitions

IsEdgeReachable k u v: vertices remain reachable after removing < k edges
IsEdgeConnected k: graph is k-edge-connected

Lemmas

Basic properties: rfl, symm, trans, mono, zero
isEdgeReachable_one: equivalence with standard Reachable
isEdgeConnected_one: equivalence with Preconnected
isEdgeReachable_succ: inductive characterization
isEdgeConnected_succ: inductive characterization for graphs
isEdgeConnected_two: equivalence with Preconnected ∧ ¬∃ e, IsBridge e

Verification

lake build passes
lake exe runLinter passes

Closes #31691

github-actions · 2025-12-14T11:01:35Z

PR summary 0a5fe12b77

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity` (new file)	589

Declarations diff

+ IsEdgeConnected
+ IsEdgeConnected.connected
+ IsEdgeConnected.preconnected
+ IsEdgeConnected.zero
+ IsEdgeReachable
+ IsEdgeReachable.anti
+ IsEdgeReachable.mono
+ IsEdgeReachable.reachable
+ IsEdgeReachable.rfl
+ IsEdgeReachable.symm
+ IsEdgeReachable.trans
+ IsEdgeReachable.zero
+ isBridge_iff_adj_and_not_isEdgeConnected_two
+ isEdgeConnected_add_one
+ isEdgeConnected_one
+ isEdgeConnected_two
+ isEdgeReachable_add_one
+ isEdgeReachable_one

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

- Define IsEdgeReachable and IsEdgeConnected - Prove basic properties: reflexivity, symmetry, transitivity, monotonicity - Prove equivalence with standard reachability for k=1 - Prove inductive characterization for k+1 - Prove IsEdgeConnected 2 ↔ Preconnected ∧ no bridges Closes leanprover-community#31691

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

…-connectivity

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

SnirBroshi

Looks good!

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

SnirBroshi · 2025-12-20T21:09:46Z

@YaelDillies in the issue you said "possibly more lemmas relating G.IsEdgeConnected 2 and G.IsAcyclic", and I'm wondering what the relation is specifically.
It's not difficult to prove ¬G.IsAcyclic ↔ ∃ u v, G.Adj u v ∧ G.IsEdgeReachable 2 u v,
but do you know if ¬G.IsAcyclic ↔ ∃ u v, G.IsEdgeReachable 2 u v is true?
Perhaps even G.IsTree ↔ ¬G.IsEdgeConnected 2 assuming Nonempty V?

YaelDillies · 2025-12-20T21:17:35Z

do you know if ¬G.IsAcyclic ↔ ∃ u v, G.IsEdgeReachable 2 u v is true?

Yes, by (the local version of) edge Menger

G.IsTree ↔ ¬G.IsEdgeConnected 2 assuming Nonempty V?

That is very false. Not being two-edge connected is the same thing as having a bridge, while being a tree is the same as all edges being bridges.

0xTerencePrime · 2025-12-21T06:50:44Z

I've applied all the suggested improvements from @YaelDillies and @SnirBroshi, including the 'strictly fewer' terminology, theorem protection, dot notation golfs, and the characterization of bridges. The full lake build Mathlib now passes without any errors or warnings. Thank you both for the great feedback!

YaelDillies

Thanks!

maintainer delegate

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

github-actions · 2025-12-22T15:55:02Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

SnirBroshi

Thanks!

btw the current build will probably time out in 3.5 hours, there's some unknown bug there (see #mathlib4 > slow linting step CI? @ 💬), but retriggerring the build should fix it (click "Update branch" below)

0xTerencePrime · 2025-12-23T07:28:43Z

Thanks for the heads-up regarding the CI timeout bug, @SnirBroshi! I have updated the branch as suggested to re-trigger the build.

0xTerencePrime · 2025-12-23T08:40:26Z

I've noted the CI error. I'll re-trigger the build later today when I'm back at my computer. Thanks!

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

0xTerencePrime · 2025-12-23T16:55:58Z

Hi @YaelDillies and @SnirBroshi,

I have updated the code to incorporate the final golfs and address the remaining comments.

Resolved the nonempty assignment thread.
Cleaned up redundant {k : ℕ} variable declarations in the lemma headers.
I have kept the conversation regarding isEdgeConnected_add_one open. As discussed, I retained G.Preconnected to ensure the equivalence holds for discrete graphs where the RHS is vacuously true.

The build is now fully green. Ready for a final review!

0xTerencePrime · 2025-12-24T15:54:36Z

All remaining comments addressed and local build passes. Ready for review!

SnirBroshi

Nice! Here's a golf for the new result

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

jcommelin · 2025-12-26T18:02:56Z

I think I've already requested this on another PR: please reduce the AI generated commit messages. We don't need the "Verification" stuff at all. We have CI for that.
And the rest of the message is mostly directly readable from the diff.

The 1-line "Summary" is good.

jcommelin

Thanks 🎉

bors merge

This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing #31691. Co-authored-by: 0xTerencePrime <[email protected]> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Yaël Dillies <[email protected]>

mathlib-bors · 2025-12-26T19:27:43Z

Pull request successfully merged into master.

Build succeeded:

…-community#32870) This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing leanprover-community#31691. Co-authored-by: 0xTerencePrime <[email protected]> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Yaël Dillies <[email protected]>

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics labels Dec 14, 2025

0xTerencePrime and others added 5 commits December 14, 2025 07:46

[pre-commit.ci lite] apply automatic fixes

c9b0bbe

chore: regenerate import all files

9f810de

fix: add copyright header, fix variable scope, fix line length

90d495d

chore: sync with upstream master

5930d0e

0xTerencePrime force-pushed the edge-connectivity branch from 5e2b2ed to 5930d0e Compare December 14, 2025 15:48

0xTerencePrime added 2 commits December 14, 2025 08:22

fix: add module declaration

4e661d5

fix: use public imports and public declarations

d06002a

YaelDillies reviewed Dec 20, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Dec 20, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 20, 2025

0xTerencePrime mentioned this pull request Dec 20, 2025

Edge-connectivity #31691

Closed

0xTerencePrime added 3 commits December 20, 2025 07:48

feat(Combinatorics/SimpleGraph): define edge-connectivity

72c1eb4

refactor: ensure clean module structure for EdgeConnectivity

6b9f2f9

style: fix end of file whitespace

e36e3ab

0xTerencePrime force-pushed the edge-connectivity branch from 1db6caa to e36e3ab Compare December 20, 2025 16:08

0xTerencePrime added 4 commits December 20, 2025 08:20

fix: explicit import in Mathlib.lean and cleanup

433a500

chore: trigger CI build and update manifest

c856625

Merge branch 'master' of github.com:0xTerencePrime/mathlib4 into edge…

cf15d42

…-connectivity

feat: align with rc1 module system and fix private module warning

7adfd72

0xTerencePrime force-pushed the edge-connectivity branch from 08391fc to 7adfd72 Compare December 20, 2025 17:06

YaelDillies reviewed Dec 20, 2025

View reviewed changes

SnirBroshi reviewed Dec 20, 2025

View reviewed changes

feat: implement edge-connectivity with full reviewer suggestions

403a21c

YaelDillies approved these changes Dec 22, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Show resolved Hide resolved

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 22, 2025

feat: implement IsEdgeConnected.connected using where

2b9fc7b

SnirBroshi reviewed Dec 22, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated Show resolved Hide resolved

style: rename isEdgeConnected_succ to isEdgeConnected_add_one

9dfd0a7

SnirBroshi approved these changes Dec 23, 2025

View reviewed changes

YaelDillies reviewed Dec 23, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated Show resolved Hide resolved

style: golf connected lemma and clean up variable declarations

4963ae1

0xTerencePrime force-pushed the edge-connectivity branch from aaad30a to 4963ae1 Compare December 23, 2025 16:35

style: finalize isEdgeConnected_add_one logic and golf connected lemma

37281b9

SnirBroshi reviewed Dec 24, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean Outdated Show resolved Hide resolved

style: apply Snir's golf for isEdgeConnected_add_one

ec1552e

jcommelin reviewed Dec 26, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Dec 26, 2025

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph): define edge-connectivity~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph): define edge-connectivity Dec 26, 2025

mathlib-bors bot closed this Dec 26, 2025

SnirBroshi mentioned this pull request Dec 26, 2025

refactor(SimpleGraph): change bridges not to require the edge to be present #32583

Open

2 tasks

0xTerencePrime mentioned this pull request Dec 28, 2025

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

Open

SnirBroshi mentioned this pull request Feb 17, 2026

feat(SimpleGraph/Acyclic): the union of two trees that share exactly one vertex is a tree #35327

Open

Conversation

0xTerencePrime commented Dec 14, 2025 • edited by jcommelin Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Main Changes

Definitions

Lemmas

Verification

Uh oh!

github-actions bot commented Dec 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0a5fe12b77

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi commented Dec 20, 2025

Uh oh!

YaelDillies commented Dec 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

0xTerencePrime commented Dec 21, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Dec 22, 2025

Uh oh!

Uh oh!

SnirBroshi left a comment

Choose a reason for hiding this comment

Uh oh!

0xTerencePrime commented Dec 23, 2025

Uh oh!

0xTerencePrime commented Dec 23, 2025

Uh oh!

Uh oh!

0xTerencePrime commented Dec 23, 2025

Uh oh!

0xTerencePrime commented Dec 24, 2025

Uh oh!

SnirBroshi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jcommelin commented Dec 26, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Dec 26, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

0xTerencePrime commented Dec 14, 2025 •

edited by jcommelin

Loading

github-actions bot commented Dec 14, 2025 •

edited

Loading

YaelDillies commented Dec 20, 2025 •

edited

Loading