feat: reshape SimpleGraph.ball to open balls per Zulip consensus

Redesign GraphBall.lean: definition uses strict `<` (matching
Metric.ball), giving ball_top = connectedComponent.supp. Core API
trimmed to 1 def + 7 lemmas for upstream PR; convenience lemmas
kept below section marker. Rename ball_comm → mem_ball_comm.
Submit Aristotle Batch 1 (flowerEdge_card, edgeSrc_ne_edgeTgt).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: Fieldnote-Echo

CLAUDE.md

@@ -170,8 +170,8 @@ copyright headers on all `.lean` files.
 | `FlowerLog.lean` | Log identities + squeeze bounds | Proved |
 | `FlowerDimension.lean` | Headline theorem (squeeze limit) | Proved |
 | `FlowerLogRatio.lean` | HasLogRatioDimension definition | Definition only |
-| `GraphBall.lean` | SimpleGraph.ball (upstream candidate, 12 lemmas) | Proved |
-| `PathGraphDist.lean` | pathGraph distance (F2 building block) | Sorry stubs |
+| `GraphBall.lean` | SimpleGraph.ball open metric balls (upstream candidate) | Proved |
+| `PathGraphDist.lean` | pathGraph distance (upstream candidate) | Proved |
 | `FlowerConstruction.lean` | F2 bridge sketch (structured gadgets) | Sorry stubs |
 | `Verify.lean` | Axiom dashboard | Proved |
 

FdFormal/GraphBall.lean

@@ -4,32 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nelson Spence
 -/
 import Mathlib.Combinatorics.SimpleGraph.Metric
-import Mathlib.Combinatorics.SimpleGraph.Finite
 
 set_option relaxedAutoImplicit false
 set_option autoImplicit false
 
 /-!
 # Metric balls for simple graphs
 
-This file defines the metric ball `SimpleGraph.ball` using the extended
-distance `SimpleGraph.edist`. Using `edist` (rather than `dist`) ensures
-that disconnected vertices, which are at distance `⊤`, are correctly
-excluded from finite-radius balls.
+This file defines the open metric ball `SimpleGraph.ball` using the extended
+distance `SimpleGraph.edist`, following the convention of `Metric.ball`.
+
+Using strict inequality (`<`) gives the natural property that `ball c ⊤`
+equals the support of the connected component containing `c`.
 
 ## Main definitions
 
-- `SimpleGraph.ball` — the set of vertices within extended distance `r`
-  of a center vertex
+- `SimpleGraph.ball` — the set of vertices within extended distance strictly
+  less than `r` of a center vertex
 
 ## Main statements
 
 - `SimpleGraph.mem_ball` — membership characterization
+- `SimpleGraph.ball_zero` — the zero-radius ball is empty
+- `SimpleGraph.ball_one` — the unit ball is `{c}`
+- `SimpleGraph.ball_top` — the `⊤`-radius ball is the connected component
 - `SimpleGraph.ball_mono` — monotonicity in radius
-- `SimpleGraph.ball_zero` — the zero-radius ball is `{c}`
-- `SimpleGraph.ball_top` — the `⊤`-radius ball is `Set.univ`
-- `SimpleGraph.ball_comm` — `v ∈ G.ball c r ↔ c ∈ G.ball v r`
-- `SimpleGraph.ball_anti` — supergraphs have larger balls
+- `SimpleGraph.center_mem_ball` — center belongs to any positive-radius ball
+- `SimpleGraph.mem_ball_comm` — membership is symmetric in center and point
+
+## Implementation notes
+
+The definition uses `ℕ∞` radius to match `SimpleGraph.edist`. For finite
+`n : ℕ`, `G.ball c (n + 1)` is the closed ball of radius `n` in the usual
+sense (vertices at distance `≤ n`), since `edist c v < n + 1 ↔ edist c v ≤ n`
+for natural numbers.
+
+## References
+
+* `Mathlib.Combinatorics.SimpleGraph.Metric`
 
 ## Tags
 
@@ -40,80 +52,104 @@ namespace SimpleGraph
 
 variable {V : Type*} (G : SimpleGraph V)
 
-/-! ### Definition and membership -/
-
-/-- The closed ball of radius `r` around vertex `c` in the graph extended metric. -/
+/-- The open ball of radius `r` around vertex `c` in the graph extended metric. -/
 def ball (c : V) (r : ℕ∞) : Set V :=
-  {v | G.edist c v ≤ r}
+  {v | G.edist c v < r}
 
 variable {G}
 
 @[simp]
 theorem mem_ball {c v : V} {r : ℕ∞} :
-    v ∈ G.ball c r ↔ G.edist c v ≤ r :=
+    v ∈ G.ball c r ↔ G.edist c v < r :=
   Iff.rfl
 
-theorem edist_le_of_mem_ball {c v : V} {r : ℕ∞} (h : v ∈ G.ball c r) :
-    G.edist c v ≤ r :=
-  h
-
-/-! ### Radius extremes -/
+@[simp]
+theorem ball_zero {c : V} : G.ball c 0 = ∅ := by
+  ext v; simp [ball]
 
 @[simp]
-theorem ball_zero {c : V} : G.ball c 0 = {c} := by
+theorem ball_one {c : V} : G.ball c 1 = {c} := by
   ext v
-  simp [ball, nonpos_iff_eq_zero]
+  simp only [mem_ball, Set.mem_singleton_iff]
+  constructor
+  · intro h
+    have h0 : G.edist c v = 0 := by
+      have hne : G.edist c v ≠ ⊤ := ne_top_of_lt h
+      lift G.edist c v to ℕ using hne with d
+      have : d < 1 := by exact_mod_cast h
+      exact_mod_cast (show d = 0 from by omega)
+    exact (edist_eq_zero_iff.mp h0).symm
+  · rintro rfl; simp
 
 @[simp]
-theorem ball_top {c : V} : G.ball c ⊤ = Set.univ := by
+theorem ball_top {c : V} :
+    G.ball c ⊤ = (G.connectedComponentMk c).supp := by
   ext v
-  simp [ball]
-
-/-! ### Monotonicity -/
+  simp only [mem_ball, ConnectedComponent.mem_supp_iff]
+  constructor
+  · intro h
+    exact (ConnectedComponent.eq.mpr
+      (reachable_of_edist_ne_top (ne_top_of_lt h))).symm
+  · intro h
+    exact lt_top_iff_ne_top.mpr
+      (edist_ne_top_iff_reachable.mpr (ConnectedComponent.eq.mp h.symm))
 
 /-- Balls are monotone in the radius. -/
 theorem ball_mono {c : V} {r₁ r₂ : ℕ∞} (h : r₁ ≤ r₂) :
     G.ball c r₁ ⊆ G.ball c r₂ :=
-  fun _ hv ↦ le_trans hv h
-
-/-- Supergraphs have larger or equal balls. -/
-@[gcongr]
-theorem ball_anti {G' : SimpleGraph V} {c : V} {r : ℕ∞} (h : G ≤ G') :
-    G.ball c r ⊆ G'.ball c r :=
-  fun _ hv ↦ le_trans (edist_anti h) hv
+  fun _ hv ↦ lt_of_lt_of_le hv h
 
-/-! ### Center and symmetry -/
-
-/-- The center vertex belongs to any ball around it. -/
-theorem center_mem_ball {c : V} {r : ℕ∞} :
+/-- The center vertex belongs to any ball of positive radius. -/
+theorem center_mem_ball {c : V} {r : ℕ∞} (hr : 0 < r) :
     c ∈ G.ball c r := by
-  simp [ball]
-
-theorem ball_nonempty {c : V} {r : ℕ∞} : (G.ball c r).Nonempty :=
-  ⟨c, center_mem_ball⟩
+  simp [ball, hr]
 
 /-- Ball membership is symmetric in center and point. -/
-theorem ball_comm {c v : V} {r : ℕ∞} :
+theorem mem_ball_comm {c v : V} {r : ℕ∞} :
     v ∈ G.ball c r ↔ c ∈ G.ball v r := by
   simp [ball, edist_comm]
 
-/-! ### Adjacency -/
+/-! ### Convenience lemmas (not in first upstream PR) -/
 
-theorem ball_one_eq {c : V} :
-    G.ball c 1 = {v | G.edist c v ≤ 1} :=
-  rfl
+theorem edist_lt_of_mem_ball {c v : V} {r : ℕ∞} (h : v ∈ G.ball c r) :
+    G.edist c v < r :=
+  h
 
-theorem adj_of_mem_ball_one {c v : V} (h : v ∈ G.ball c 1) (hne : c ≠ v) :
-    G.Adj c v := by
-  rw [mem_ball] at h
-  exact (edist_le_one_iff_adj_or_eq.mp h).resolve_right hne
+theorem ball_nonempty {c : V} {r : ℕ∞} (hr : 0 < r) : (G.ball c r).Nonempty :=
+  ⟨c, center_mem_ball hr⟩
 
-/-! ### Triangle inequality -/
+/-- Supergraphs have larger or equal balls. -/
+@[gcongr]
+theorem ball_anti {G' : SimpleGraph V} {c : V} {r : ℕ∞} (h : G ≤ G') :
+    G.ball c r ⊆ G'.ball c r :=
+  fun _ hv ↦ lt_of_le_of_lt (edist_anti h) hv
+
+/-- Vertices adjacent to `c` are in the ball of radius 2. -/
+theorem mem_ball_of_adj {c v : V} (h : G.Adj c v) :
+    v ∈ G.ball c 2 := by
+  simp only [mem_ball]
+  have h1 : (1 : ℕ∞) < 2 := by exact_mod_cast (show (1 : ℕ) < 2 from by omega)
+  exact lt_of_le_of_lt (edist_le_one_iff_adj_or_eq.mpr (Or.inl h)) h1
+
+theorem adj_of_mem_ball_two {c v : V} (h : v ∈ G.ball c 2) (hne : c ≠ v) :
+    G.Adj c v := by
+  simp only [mem_ball] at h
+  have hle : G.edist c v ≤ 1 := by
+    have hne_top : G.edist c v ≠ ⊤ := ne_top_of_lt h
+    lift G.edist c v to ℕ using hne_top with d
+    have : d < 2 := by exact_mod_cast h
+    exact_mod_cast (show d ≤ 1 from by omega)
+  exact (edist_le_one_iff_adj_or_eq.mp hle).resolve_right hne
 
 /-- If `v ∈ ball c r₁` and `w ∈ ball v r₂`, then `w ∈ ball c (r₁ + r₂)`. -/
 theorem mem_ball_of_mem_ball_of_mem_ball {c v w : V} {r₁ r₂ : ℕ∞}
     (hv : v ∈ G.ball c r₁) (hw : w ∈ G.ball v r₂) :
-    w ∈ G.ball c (r₁ + r₂) :=
-  le_trans G.edist_triangle (add_le_add hv hw)
+    w ∈ G.ball c (r₁ + r₂) := by
+  simp only [mem_ball] at *
+  have hw_ne : G.edist v w ≠ ⊤ := ne_top_of_lt hw
+  calc G.edist c w
+    ≤ G.edist c v + G.edist v w := G.edist_triangle
+    _ < r₁ + G.edist v w := (ENat.add_lt_add_iff_right hw_ne).mpr hv
+    _ ≤ r₁ + r₂ := by gcongr
 
 end SimpleGraph

README.md

@@ -34,7 +34,7 @@ This is the ground truth formula that [navi-fractal](https://github.com/Project-
 
 | Declaration | File | Topic | Mathlib status |
 |-------------|------|-------|----------------|
-| `SimpleGraph.ball` + 11 lemmas | `GraphBall` | Metric ball via `edist` (basic API, 12 lemmas) | No `SimpleGraph.ball` in Mathlib |
+| `SimpleGraph.ball` + 7 core lemmas | `GraphBall` | Open metric ball via `edist` (8 core + convenience lemmas) | No `SimpleGraph.ball` in Mathlib; PR ready to open |
 
 ## Axiom boundary
 
@@ -60,7 +60,7 @@ lake build --wfail   # fail on any sorry or warning
 
 ```
 FdFormal/
-  GraphBall.lean         — SimpleGraph.ball via edist, 12 lemmas (upstream candidate)
+  GraphBall.lean         — SimpleGraph.ball (open ball via edist), 8 core + convenience lemmas (upstream candidate)
   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

ROADMAP.md

@@ -24,12 +24,13 @@ Supporting infrastructure (monotonicity, cast identities, log helpers) is
 in `FlowerCounts`, `FlowerDiameter`, and `FlowerLog`. Leaf lemmas are proved
 via a combination of human authoring and Aristotle automated proof search.
 
-**Upstream contribution:** `GraphBall.lean` defines `SimpleGraph.ball` via
-`edist` and contains 12 proved lemmas (membership, monotonicity, radius
-extremes, center membership, symmetry, adjacency, triangle inequality).
-A draft Mathlib PR is prepared (`docs/internal/pr-mathlib-ball-draft.md`);
-must post to Zulip before opening. Need to check overlap with PR #33077
-(`SetRel.ball` by Yael Dillies).
+**Upstream contribution:** `GraphBall.lean` defines `SimpleGraph.ball` as an
+open ball via `edist` (strict `<`, not `≤`). Reshaped per Zulip discussion and
+auditor feedback: 1 def + 7 core lemmas (`mem_ball`, `ball_zero`, `ball_one`,
+`ball_top`, `ball_mono`, `center_mem_ball`, `mem_ball_comm`) form the upstream
+PR; convenience lemmas kept in-repo.
+Import simplified to `Mathlib.Combinatorics.SimpleGraph.Metric`.
+`ball_top` now gives connected-component support. PR ready to open.
 
 ### Next
 
@@ -49,7 +50,7 @@ construction sketch with five layers:
 - Layer 1: `FlowerEdge u v g` (recursive edge index type) and
   `FlowerVert u v g` (hubs + sigma of internal vertices by generation).
 - Layer 2: `edgeEndpoints` via recursive gadget resolution, plus
-  `edgeSrc_ne_edgeTgt` (sorry stub).
+  `edgeSrc_ne_edgeTgt` (sorry stub; submitted to Aristotle Batch 1).
 - Layer 3: `flowerGraph'` as a `SimpleGraph` on `FlowerVert`, with
   `flowerAdj'` defined by edge existence.
 - Layer 4: Distance proof via upper bound (exhibited walk of length `u^g`)
@@ -60,6 +61,9 @@ construction sketch with five layers:
   giving the final `flowerGraph_dist_hubs` bridge statement.
 - Projection map `FlowerVert.project` is defined (not sorry).
 
+**Aristotle Batch 1** submitted: `flowerEdge_card` and `edgeSrc_ne_edgeTgt`
+(running, results pending). These are leaf lemmas for Layers 1 and 2.
+
 Building block: `PathGraphDist.lean` provides fully proved lemmas for
 `SimpleGraph.pathGraph` distance (`pathGraph_dist`, `pathGraph_dist_zero_last`,
 `pathGraph_edist_zero_last`). These have no Mathlib counterpart and are a

debt.md

@@ -11,8 +11,10 @@
   `GadgetPos`, `LocalEdge`, recursive `FlowerEdge` edge indices,
   `edgeEndpoints` resolution, `FlowerVert` with hub embedding, `flowerGraph'`
   as `SimpleGraph`, projection map for lower bound, and `flowerGraph_dist_hubs`
-  as the F2 bridge target. Several sorry stubs remain (irreflexivity,
+  as the F2 bridge target. 8 sorry stubs remain (irreflexivity,
   connectivity, walk/distance bounds, vertex card, final transport).
+  Aristotle Batch 1 submitted for `flowerEdge_card` and `edgeSrc_ne_edgeTgt`
+  (running, results pending).
   *(FlowerConstruction.lean, FlowerGraph.lean)*
 
 - [ ] **Log-ratio dimension bridge** — Prove `HasLogRatioDimension` for the
@@ -22,13 +24,13 @@
 
 ### Upstream candidates
 
-- [ ] **SimpleGraph.ball PR** — Clean up GraphBall.lean for Mathlib PR.
-  Now has 12 lemmas (expanded API): `mem_ball`, `edist_le_of_mem_ball`,
-  `ball_zero`, `ball_top`, `ball_mono`, `ball_anti`, `center_mem_ball`,
-  `nonempty_ball`, `ball_comm`, `ball_one_eq`, `adj_of_mem_ball_one`,
-  `mem_ball_of_mem_ball_of_mem_ball`. Watch PR #33077 (Yael Dillies,
-  SetRel.ball) for potential overlap. Key reviewer: Rida Hamadani.
-  *(GraphBall.lean)*
+- [ ] **SimpleGraph.ball PR** — Reshaped per Zulip discussion and auditor
+  feedback: open ball (`<` not `≤`), 1 def + 7 core lemmas (`mem_ball`,
+  `ball_zero`, `ball_one`, `ball_top`, `ball_mono`, `center_mem_ball`,
+  `mem_ball_comm`). `ball_top` gives connected-component
+  support. Import simplified to `Mathlib.Combinatorics.SimpleGraph.Metric`.
+  Convenience lemmas kept in-repo for project use. **Ready to open PR.**
+  Key reviewer: Rida Hamadani. *(GraphBall.lean)*
 
 - [ ] **GraphBall finite cardinality lemmas** — `card_ball_mono` etc. require
   `[Fintype V]`. Separated from base definition by design. *(GraphBall.lean)*

docs/aristotle/batch1-edgeSrc_ne_edgeTgt.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+/-
+Aristotle Batch 1 — Leaf: edgeSrc_ne_edgeTgt
+Target: Source ≠ target for every edge in the flower construction.
+Strategy: induction on g, case analysis on local edge positions.
+Base case: hub0 ≠ hub1. Step: gadget resolution preserves distinctness.
+-/
+import Mathlib.Tactic
+
+set_option relaxedAutoImplicit false
+set_option autoImplicit false
+
+/-! ## Layer 0: Local replacement gadget -/
+
+inductive GadgetPos (u v : ℕ)
+  | src
+  | tgt
+  | short (i : Fin (u - 1))
+  | long  (j : Fin (v - 1))
+
+abbrev LocalEdge (u v : ℕ) := Fin u ⊕ Fin v
+
+def localSrc (u v : ℕ) : LocalEdge u v → GadgetPos u v
+  | .inl ⟨0, _⟩     => .src
+  | .inl ⟨i + 1, h⟩ => .short ⟨i, by omega⟩
+  | .inr ⟨0, _⟩     => .src
+  | .inr ⟨j + 1, h⟩ => .long ⟨j, by omega⟩
+
+def localTgt (u v : ℕ) : LocalEdge u v → GadgetPos u v
+  | .inl i => if h : i.val + 1 = u then .tgt else .short ⟨i.val, by omega⟩
+  | .inr j => if h : j.val + 1 = v then .tgt else .long ⟨j.val, by omega⟩
+
+/-! ## Layer 1: Types -/
+
+def FlowerEdge (u v : ℕ) : ℕ → Type
+  | 0     => Unit
+  | g + 1 => FlowerEdge u v g × LocalEdge u v
+
+instance instFintypeFlowerEdge (u v g : ℕ) : Fintype (FlowerEdge u v g) := by
+  induction g with
+  | zero => exact inferInstanceAs (Fintype Unit)
+  | succ g ih => exact inferInstanceAs (Fintype (_ × _))
+
+def FlowerVert (u v : ℕ) (g : ℕ) : Type :=
+  Fin 2 ⊕ Σ (k : Fin g), FlowerEdge u v k.val × (Fin (u - 1) ⊕ Fin (v - 1))
+
+def FlowerVert.hub0 (u v g : ℕ) : FlowerVert u v g := .inl 0
+def FlowerVert.hub1 (u v g : ℕ) : FlowerVert u v g := .inl 1
+
+def FlowerVert.embed (u v g : ℕ) : FlowerVert u v g → FlowerVert u v (g + 1)
+  | .inl h => .inl h
+  | .inr ⟨k, e, pos⟩ => .inr ⟨k.castSucc, e, pos⟩
+
+/-! ## Layer 2: Edge endpoints -/
+
+def edgeEndpoints (u v : ℕ) :
+    (g : ℕ) → FlowerEdge u v g → FlowerVert u v g × FlowerVert u v g
+  | 0, () => (.hub0 u v 0, .hub1 u v 0)
+  | g + 1, (parent, localE) =>
+    let (pSrc, pTgt) := edgeEndpoints u v g parent
+    let resolve : GadgetPos u v → FlowerVert u v (g + 1) := fun
+      | .src     => FlowerVert.embed u v g pSrc
+      | .tgt     => FlowerVert.embed u v g pTgt
+      | .short i => .inr ⟨⟨g, Nat.lt_succ_of_le le_rfl⟩, parent, .inl i⟩
+      | .long j  => .inr ⟨⟨g, Nat.lt_succ_of_le le_rfl⟩, parent, .inr j⟩
+    (resolve (localSrc u v localE), resolve (localTgt u v localE))
+
+def edgeSrc (u v g : ℕ) (e : FlowerEdge u v g) : FlowerVert u v g :=
+  (edgeEndpoints u v g e).1
+
+def edgeTgt (u v g : ℕ) (e : FlowerEdge u v g) : FlowerVert u v g :=
+  (edgeEndpoints u v g e).2
+
+/-! ## Helper: local source ≠ local target -/
+
+/-- Within a single gadget, source and target positions are always distinct
+when `1 < u`. This is the key inductive step helper. -/
+theorem localSrc_ne_localTgt (u v : ℕ) (hu : 1 < u) (e : LocalEdge u v) :
+    localSrc u v e ≠ localTgt u v e := by
+  sorry
+
+/-- Source ≠ target for every edge. -/
+theorem edgeSrc_ne_edgeTgt (u v g : ℕ) (hu : 1 < u) (e : FlowerEdge u v g) :
+    edgeSrc u v g e ≠ edgeTgt u v g e := by
+  sorry