upstream: submit PathGraphDist.lean to Mathlib

[Fieldnote-Echo]

Context

PathGraphDist.lean proves that the graph-theoretic distance in a path graph equals the absolute difference of vertex indices:

pathGraph_dist (n : ℕ) (i j : Fin n) : (pathGraph n).dist i j = |i - j|

This fills a gap in Mathlib's SimpleGraph.Connectivity.PathGraph API, which defines path graph adjacency but not distance. The edist variant is also proved.

What needs to happen

1. Check Mathlib's current state — confirm pathGraph_dist doesn't exist yet (it didn't as of Lean 4.28.0)
2. Post to Zulip (#graph-theory) proposing the addition, linking to fd-formalization
3. Refactor to Mathlib style — the proof may need adjustments for Mathlib's naming conventions, docstrings, and universe polymorphism requirements
4. Submit PR to Mathlib.Combinatorics.SimpleGraph.Connectivity.PathGraph (or wherever reviewers suggest)
5. AI disclosure per Mathlib policy

Prior art

SimpleGraph.ball (PR #36443) followed this exact pipeline: develop in fd-formalization → Zulip discussion → Mathlib PR. PathGraphDist is the second upstream candidate.

Acceptance criteria

• Zulip thread opened with proposal
• Mathlib PR submitted and passing CI
• fd-formalization updated to import from Mathlib once merged (removing local copy)