From e8c38b26b3e2bac1a2f76ead053ed00ced43a116 Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Wed, 13 May 2026 18:05:28 -0500 Subject: [PATCH] docs: mark SimpleGraph.ball upstreamed in Mathlib #36443 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first upstream candidate listed in the README — SimpleGraph.ball and its core lemmas — landed in Mathlib via bors on 2026-04-19. Update the upstream-candidates table status column and the project-structure note to reflect this. --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 521457f..b12d9b4 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,7 @@ This is the ground truth formula that [navi-fractal](https://github.com/Project- | Declaration | File | Topic | Mathlib status | |-------------|------|-------|----------------| -| `SimpleGraph.ball` + 7 core lemmas | `GraphBall` | Open metric ball via `edist` (8 core + 6 convenience lemmas) | No `SimpleGraph.ball` in Mathlib; PR ready to open | +| `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) | | `pathGraph_edist`, `pathGraph_dist` + 2 corollaries | `PathGraphDist` | Distance in path graphs = index difference | No distance lemmas for `pathGraph` in Mathlib | ## Axiom boundary @@ -71,7 +71,7 @@ lake build --wfail # fail on any sorry or warning ``` FdFormal/ - GraphBall.lean — SimpleGraph.ball (open ball via edist), 8 core + 6 convenience lemmas (upstream candidate) + GraphBall.lean — SimpleGraph.ball (open ball via edist), 8 core + 6 convenience lemmas (upstreamed: Mathlib #36443) FlowerGraph.lean — Hub vertices and structural helpers FlowerCounts.lean — Exact edge/vertex count formulas, bounds, monotonicity FlowerDiameter.lean — Hub-distance scaling L_g = u^g, cast identities