docs: mark SimpleGraph.ball upstreamed in Mathlib #36443

[Nelson Spence (Fieldnote-Echo)]

Summary

The first upstream candidate listed in the README — SimpleGraph.ball and its core lemmas — landed in Mathlib via bors on 2026-04-19.

Two README updates:

1. Upstream candidates table — status column changes from "No SimpleGraph.ball in Mathlib; PR ready to open" to a link to the merged Mathlib PR.
2. Project structure — the GraphBall.lean note changes from "upstream candidate" to "upstreamed: Mathlib #36443".

Mathlib PR: leanprover-community/mathlib4#36443

Scope

Docs only. No code changes. The local GraphBall.lean is retained as-is; downstream migration to the Mathlib version (Mathlib.Combinatorics.SimpleGraph.Metric) is a separate refactor.

Test plan

• Diff is two single-line changes to README.md
• No source files touched
• Pre-commit hooks pass (gitleaks, trailing whitespace, EOF newline, merge conflict checks)
• CI green

[qodo-code-review]

Review Summary by Qodo

Mark SimpleGraph.ball upstreamed in Mathlib #36443

📝 Documentation

Walkthroughs

Description

• Update README to mark SimpleGraph.ball as upstreamed to Mathlib
• Change upstream candidates table status to merged Mathlib PR link
• Update project structure note from candidate to upstreamed status

Diagram

flowchart LR
  A["SimpleGraph.ball<br/>Upstream Candidate"] -- "Merged via bors<br/>2026-04-19" --> B["Mathlib #36443<br/>Merged Status"]
  C["README.md<br/>Documentation"] -- "Update Status" --> D["Upstream Candidates<br/>Table & Project Structure"]

Loading

File Changes

1. README.md 📝 Documentation +2/-2

Mark SimpleGraph.ball upstreamed to Mathlib

• Updated upstream candidates table to mark SimpleGraph.ball as merged in Mathlib #36443 with
 merge date
• Changed project structure note for GraphBall.lean from "upstream candidate" to "upstreamed:
 Mathlib #36443"
• Added link to merged Mathlib PR in the status column

README.md

---

[qodo-code-review]

Code Review by Qodo

🐞 Bugs (1) 📘 Rule violations (1)

1. Mathlib PR link lacks citation 📘 Rule violation § Compliance

Description

README adds an external reference to Mathlib PR #36443 using a raw link without the required
standardized [AuthorYear] citation key anchored in docs/references.bib. This creates an
untracked, non-standard documentation reference that is harder to audit and maintain consistently.

Code

README.md[47]

+| `SimpleGraph.ball` + 7 core lemmas | `GraphBall` | Open metric ball via `edist` (8 core + 6 convenience lemmas) | Merged: [Mathlib #36443](https://github.com/leanprover-community/mathlib4/pull/36443) (2026-04-19, via bors) |

Evidence

PR Compliance ID 306646 requires documentation references to be made via [AuthorYear] citation
keys that correspond to entries in docs/references.bib. The cited README change introduces a
reference to Mathlib PR #36443 as a plain URL/link and does not include any [AuthorYear] key,
demonstrating non-compliance with the required citation format.

Rule 306646: Cite references with [AuthorYear] keys anchored in docs/references.bib
README.md[47-47]
README.md[74-74]

Agent prompt

The issue below was found during a code review. Follow the provided context and guidance below and implement a solution

## Issue description
The README references Mathlib PR #36443 using a raw link instead of the required standardized `[AuthorYear]` citation key format backed by an entry in `docs/references.bib`.

## Issue Context
PR Compliance ID 306646 requires documentation references to use `[AuthorYear]` keys and have matching BibTeX entries in `docs/references.bib`, so external references can be tracked and maintained consistently.

## Fix Focus Areas
- README.md[47-47]
- README.md[74-74]
- docs/references.bib[1-30]

ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools

---

2. Docs status contradiction 🐞 Bug ⚙ Maintainability

Description

README now says SimpleGraph.ball is upstreamed to Mathlib, but other repository docs still say it
does not exist / PR ready to open, leaving contributor guidance inconsistent. This will mislead
contributors about what work remains and where the authoritative implementation lives.

Code

README.md[47]

+| `SimpleGraph.ball` + 7 core lemmas | `GraphBall` | Open metric ball via `edist` (8 core + 6 convenience lemmas) | Merged: [Mathlib #36443](https://github.com/leanprover-community/mathlib4/pull/36443) (2026-04-19, via bors) |

Evidence

The new README text asserts the upstream merge, while multiple other docs in this repo still state
the opposite (not in Mathlib / PR ready), which is a direct contradiction.

README.md[43-48]
README.md[70-75]
CLAUDE.md[162-167]
CLAUDE.md[174-185]
ROADMAP.md[35-42]
debt.md[13-22]
docs/getting-started/quickstart.md[61-75]
docs/reference/roadmap.md[39-44]
docs/reference/theorems.md[182-191]

Agent prompt

The issue below was found during a code review. Follow the provided context and guidance below and implement a solution

### Issue description
`README.md` was updated to mark `SimpleGraph.ball` as merged upstream, but several other documentation sources in this repo still describe it as an upstream candidate / not in Mathlib / PR ready to open. This leaves contradictory guidance inside the repo.

### Issue Context
The PR explicitly targets docs; to keep docs coherent, all places that track upstream-candidate status should be updated together (or explicitly note that the repo still carries a local copy while pinned to an older Mathlib).

### Fix Focus Areas
- CLAUDE.md[162-167]
- CLAUDE.md[174-185]
- ROADMAP.md[35-42]
- debt.md[13-25]
- docs/getting-started/quickstart.md[61-75]
- docs/reference/roadmap.md[39-44]
- docs/reference/theorems.md[182-191]

### Expected change
- Replace statements like “does not exist in Mathlib”, “upstream candidate”, “PR ready to open” with “upstreamed (Mathlib #36443)” and optionally link the PR.
- In `debt.md`, move the `SimpleGraph.ball PR` item from Open to Resolved (or mark it checked), preserving any follow-up items that are still relevant (e.g., convenience lemmas kept in-repo).

ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools

---

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: e8c38b26b3

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "Codex (@codex) review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "Codex (@codex) address that feedback".