upstream: track Mathlib integration status for all upstream candidates #9
Description
Purpose
Track which fd-formalization results are upstream-ready, in review, or merged into Mathlib. This is the meta-issue for the upstream pipeline.
Current status
| Declaration | File | Mathlib status | Notes |
|---|---|---|---|
SimpleGraph.ball + 7 lemmas |
GraphBall.lean |
PR #36443 — in review | Open ball via edist, ℕ∞-valued radius |
pathGraph_dist, pathGraph_edist |
PathGraphDist.lean |
Not yet submitted | Fills gap in pathGraph API — see #4 |
flowerDimension (F1) |
FlowerDimension.lean |
Not upstream candidate | Flower-specific, not general Mathlib material |
flowerGraph_dist_hubs (F2) |
FlowerConstruction.lean |
Not upstream candidate | Flower-specific |
HasLogRatioDimension (F3 bridge) |
FlowerLogRatio.lean |
Definition only, not yet instantiated | Depends on F1 + F2 |
Workflow
When a Mathlib PR is submitted:
- Add the PR link to this table
- Update status as it moves through review
- Once merged, update fd-formalization to import from Mathlib instead of maintaining a local copy
Why this matters
Theorems in Mathlib carry community-verified credibility that standalone proofs do not. The upstream pipeline is fd-formalization's primary strategic objective — expansion of new results is secondary to getting existing work accepted.