feat(Combinatorics/SimpleGraph): add SimpleGraph.ball (open metric ball) by Fieldnote-Echo · Pull Request #36443 · leanprover-community/mathlib4

Fieldnote-Echo · 2026-03-10T15:33:07Z

Add SimpleGraph.ball, the open ball in the graph extended metric.

Design decisions

Open ball (strict <, not ≤): ball c ⊤ coincides with the connected
component of c, whereas a closed ball would give closedBall c ⊤ = univ.
Named SimpleGraph.ball (not eball): since dist-valued balls are less
natural for disconnected graphs, the e prefix is unnecessary.
Graph-specific (not via PseudoEMetricSpace): avoids importing ℝ.

AI assistance: Claude (Opus 4.6) helped draft and iterate on the implementation. I reviewed the code line by line and vouch for the final contents.

Discussed on Zulip.

Add `SimpleGraph.ball`, the open ball in the graph extended metric. New declarations: `ball`, `mem_ball`, `ball_zero`, `ball_one`, `ball_top`, `ball_subset_ball`, `mem_ball_self`, `mem_ball_comm`.

github-actions · 2026-03-10T15:33:29Z

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-03-10T15:34:46Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

github-actions · 2026-03-10T15:36:32Z

PR summary 3f7b757f9e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ball
+ ball_mono
+ ball_one
+ ball_top
+ ball_two
+ ball_zero
+ mem_ball
+ mem_ball_comm
+ mem_ball_self
+ mem_ball_top

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

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

lauramonk

Thank you for the contribution, I think this should be added and it looks good to me (but I have little experience reviewing so it should definitely have several opinions, notably in terms of the name conventions and perhaps shortening some proofs).
Here are a few other lemmas that come in mind:

c and v are reachable iff there exists r such that v is in the ball of radius r centered at c
the ball of radius 2 is exactly {c} and its adjacent vertices
for later: lemmas about the interactions between balls and eccentricity / diameter.

Mathlib/Combinatorics/SimpleGraph/Metric.lean

- ball_two: ball of radius 2 = center ∪ neighbors (@[simp]) - mem_ball_top: reachability ↔ membership in ball of radius ⊤ - Docstrings on ball_zero, ball_one, ball_two, ball_top, mem_ball_top - Improved ball docstring wording - Inlined ball_zero to one-liner

Fieldnote-Echo · 2026-03-10T18:53:39Z

Thank you for the contribution, I think this should be added and it looks good to me (but I have little experience reviewing so it should definitely have several opinions, notably in terms of the name conventions and perhaps shortening some proofs). Here are a few other lemmas that come in mind:

c and v are reachable iff there exists r such that v is in the ball of radius r centered at c

the ball of radius 2 is exactly {c} and its adjacent vertices

for later: lemmas about the interactions between balls and eccentricity / diameter.

PR #36443 Review Response

To: @lauramonk

Thanks for the review and the suggestions!

Style fixes — done:

Better docstring on ball: "centered at the vertex c"
Added doc comments to ball_zero and ball_one
Inlined ball_zero to a one-liner

New lemmas — added:

ball_two : G.ball c 2 = insert c (G.neighborSet c) — the ball of radius
two is the center and its neighbors. Proof reduces to edist_le_one_iff_adj_or_eq
via ENat.lt_add_one_iff. Marked @[simp] to match ball_zero/ball_one.
mem_ball_top : v ∈ G.ball c ⊤ ↔ G.Reachable c v — the pointwise reachability
characterization. This is ball_top restated as membership; the existential version
("reachable iff ∃ r, v ∈ ball c r") follows from this + ball_subset_ball.
Not @[simp] because mem_ball already normalizes the LHS (simpNF linter caught it).

Deferred — eccentricity/diameter interactions feel like a separate PR once the
ball API settles.

Diff summary (10 new declarations)

Lemma	Type
`ball_two`	`@[simp]` — ball of radius 2 = center ∪ neighbors
`mem_ball_top`	reachability ↔ membership in ball of radius ⊤

Plus style: docstrings on ball, ball_zero, ball_one; ball_zero inlined.

Build status

lake build Mathlib.Combinatorics.SimpleGraph.Metric — ✓ (901 jobs)
lake exe runLinter Mathlib.Combinatorics.SimpleGraph.Metric — ✓ (0 errors)

lauramonk

The author has implemented my comments.

Mathlib/Combinatorics/SimpleGraph/Metric.lean

…ting - Renamed ball_subset_ball to ball_mono - Rewrote ball_top proof with refine and rw steps - Restored ball_zero two-line formatting

Mathlib/Combinatorics/SimpleGraph/Metric.lean

SnirBroshi · 2026-03-12T16:39:01Z

PR #36443 Review Response

@Fieldnote-Echo I understand you're using AI to code, but could you please avoid AI walls of text when responding to people?

Additionally, your PR description is formatted incorrectly - write a one-line description of what your PR contains, followed by a blank line, and then --- on its own line, and finally restore the "Build with Ona" button from the PR template.

Fieldnote-Echo · 2026-03-12T18:11:16Z

@SnirBroshi Heard. I understand you and the other maintainers are reviewing large amounts of text in service of the public good. I'll keep responses short and in-line where appropriate.

@vlad902 Your suggested edits have been implemented.

Mathlib/Combinatorics/SimpleGraph/Metric.lean

Co-authored-by: Vlad Tsyrklevich <[email protected]>

SnirBroshi · 2026-03-12T22:03:29Z

Thanks, looks good! Apologies but I forgot to mention: the "design decisions" section was pretty cool, can you bring it back?

Fieldnote-Echo · 2026-03-12T22:31:46Z

@SnirBroshi Restored. Thank you all, this contribution experience has been meaningful and I will do my best to learn/adhere to the mathlib standards.

vlad902

LGTM, there are two open comments on the PR that seem like they can be resolved. I would do so to make it clear that those comments are now addressed. (Normally the submitter of the PR does this instead of the people leaving the feedback.)

Fieldnote-Echo · 2026-03-14T12:41:37Z

@vlad902 Thanks for the nudge, all resolved.

feat(Combinatorics/SimpleGraph): add SimpleGraph.ball (open metric ball)

6b0acf5

Add `SimpleGraph.ball`, the open ball in the graph extended metric. New declarations: `ball`, `mem_ball`, `ball_zero`, `ball_one`, `ball_top`, `ball_subset_ball`, `mem_ball_self`, `mem_ball_comm`.

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 Mar 10, 2026

github-actions bot added the t-combinatorics Combinatorics label Mar 10, 2026

Fieldnote-Echo changed the title ~~Combinatorics/SimpleGraph: add SimpleGraph.ball (open metric ball)~~ feat(Combinatorics/SimpleGraph): add SimpleGraph.ball (open metric ball) Mar 10, 2026

Merge branch 'master' into NSpe/graph-ball

83dd9ee

lauramonk reviewed Mar 10, 2026

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Metric.lean Outdated Show resolved Hide resolved

Rida-Hamadani reviewed Mar 11, 2026

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Metric.lean Show resolved Hide resolved

Mathlib/Combinatorics/SimpleGraph/Metric.lean Outdated Show resolved Hide resolved

Address review: ball_mono rename, ball_top refactor, ball_zero format…

4987dd2

…ting - Renamed ball_subset_ball to ball_mono - Rewrote ball_top proof with refine and rw steps - Restored ball_zero two-line formatting

vlad902 reviewed Mar 12, 2026

View reviewed changes

Address review: flip ball def, simplify proofs

1ce95ec

Fieldnote-Echo force-pushed the NSpe/graph-ball branch from be8de0e to 1ce95ec Compare March 12, 2026 17:33

vlad902 reviewed Mar 12, 2026

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Metric.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/SimpleGraph/Metric.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/SimpleGraph/Metric.lean Outdated Show resolved Hide resolved

Fieldnote-Echo and others added 3 commits March 12, 2026 13:17

Update Mathlib/Combinatorics/SimpleGraph/Metric.lean

4c1fe64

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Combinatorics/SimpleGraph/Metric.lean

08fbd08

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Update Mathlib/Combinatorics/SimpleGraph/Metric.lean

845fae3

Co-authored-by: Vlad Tsyrklevich <[email protected]>

Fieldnote-Echo mentioned this pull request Mar 12, 2026

refactor: tighten proof style from Mathlib PR review feedback Project-Navi/fd-formalization#11

Merged

3 tasks

vlad902 approved these changes Mar 14, 2026

View reviewed changes

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 16, 2026

Conversation

Fieldnote-Echo commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Design decisions

Uh oh!

github-actions bot commented Mar 10, 2026

Welcome new contributor!

Uh oh!

github-actions bot commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

github-actions bot commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3f7b757f9e

Import changes for modified files

Declarations diff

Uh oh!

lauramonk left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Fieldnote-Echo commented Mar 10, 2026

PR #36443 Review Response

To: @lauramonk

Diff summary (10 new declarations)

Build status

Uh oh!

lauramonk 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 Mar 12, 2026

Uh oh!

Fieldnote-Echo commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi commented Mar 12, 2026

Uh oh!

Fieldnote-Echo commented Mar 12, 2026

Uh oh!

vlad902 left a comment

Choose a reason for hiding this comment

Uh oh!

Fieldnote-Echo commented Mar 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Fieldnote-Echo commented Mar 10, 2026 •

edited

Loading

github-actions bot commented Mar 10, 2026 •

edited

Loading

github-actions bot commented Mar 10, 2026 •

edited

Loading

Fieldnote-Echo commented Mar 12, 2026 •

edited

Loading