[Merged by Bors] - feat(Combinatorics/SimpleGraph): add SimpleGraph.ball (open metric ball)

[Fieldnote-Echo]

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.

---

[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 Title Formatted Correctly

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

[github-actions]

PR summary 92a49c2372

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.

[Fieldnote-Echo]

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.

[SnirBroshi]

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]

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

[SnirBroshi]

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

[Fieldnote-Echo]

@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]

@vlad902 Thanks for the nudge, all resolved.

[b-mehta]

Other than my comment above, this looks good to me. Thanks!

[b-mehta]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style