docs: update README and reference docs after proof golf PRs

README.md

@@ -40,11 +40,12 @@ This is the ground truth formula that [navi-fractal](https://github.com/Project-
 | Log identities | `log_flowerHubDist_eq` etc. | `FlowerLog` | `log L_g = g · log u` |
 | **Log-ratio limit** | **`flowerDimension`** | **`FlowerDimension`** | **`lim log N_g / log L_g = log(u+v) / log(u)`** |
 
-### Upstream candidate
+### Upstream candidates
 
 | Declaration | File | Topic | Mathlib status |
 |-------------|------|-------|----------------|
-| `SimpleGraph.ball` + 7 core lemmas | `GraphBall` | Open metric ball via `edist` (8 core + 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) | No `SimpleGraph.ball` in Mathlib; PR ready to open |
+| `pathGraph_edist`, `pathGraph_dist` + 2 corollaries | `PathGraphDist` | Distance in path graphs = index difference | No distance lemmas for `pathGraph` in Mathlib |
 
 ## Axiom boundary
 
@@ -70,7 +71,7 @@ lake build --wfail   # fail on any sorry or warning
 
 ```
 FdFormal/
-  GraphBall.lean         — SimpleGraph.ball (open ball via edist), 8 core + convenience lemmas (upstream candidate)
+  GraphBall.lean         — SimpleGraph.ball (open ball via edist), 8 core + 6 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
@@ -79,7 +80,7 @@ FdFormal/
   FlowerDimension.lean   — Headline theorem: log-ratio limit = log(u+v) / log(u)
   PathGraphDist.lean     — pathGraph distance lemmas (upstream candidate)
   FlowerConstruction.lean — F2 bridge: SimpleGraph construction + dist = u^g
-  Verify.lean            — #print axioms dashboard (20 declarations)
+  Verify.lean            — #print axioms dashboard (27 declarations)
 ```
 
 ## Mathematical background
@@ -108,9 +109,11 @@ the core contribution. The underlying mathematics is from Rozenfeld et al. 2007.
 
 **What AI tools did**: Claude Opus assisted with Lean 4 syntax, Mathlib API
 navigation, and proof term synthesis. Aristotle (Harmonic) independently proved
-leaf lemmas (positivity, monotonicity, cast identities) via automated proof search.
-These roles are analogous to `omega`, `aesop`, and other proof automation — the
-strategy is human, the term-level search is machine-assisted.
+leaf lemmas (positivity, monotonicity, cast identities) via automated proof search,
+and contributed proof simplification — eliminating intermediate bindings, converting
+tactic proofs to term mode, and inlining redundant variables. These roles are
+analogous to `omega`, `aesop`, and other proof automation — the strategy is human,
+the term-level search and cleanup is machine-assisted.
 
 **Verification**: The final arbiter is the Lean compiler:
 ```bash

docs/explanation/graph-construction.md

@@ -20,14 +20,14 @@ At generation \(g\), the flower has two hub vertices plus internal vertices cont
 
 ```lean
 def FlowerVert (u v : ℕ) (g : ℕ) : Type :=
-  Sum (Fin 2) (Σ (e : FlowerEdge u v g), GadgetPos u v)
+  Fin 2 ⊕ Σ (k : Fin g), FlowerEdge u v k.val × (Fin (u - 1) ⊕ Fin (v - 1))
 ```
 
-The left summand `Fin 2` gives the two hubs. The right summand pairs each edge index with a position within its replacement gadget.
+The left summand `Fin 2` gives the two hubs. The right summand indexes each internal vertex by three coordinates: the generation `k` at which it was created, the parent edge `e` that was replaced, and a position `Fin (u - 1) ⊕ Fin (v - 1)` within the replacement gadget (short or long path).
 
 ### Gadget positions
 
-Each edge is replaced by two parallel paths of lengths \(u\) and \(v\). The internal vertices of this replacement are:
+Each edge is replaced by two parallel paths of lengths \(u\) and \(v\). The positions within a replacement gadget are described by:
 
 ```lean
 inductive GadgetPos (u v : ℕ)
@@ -37,7 +37,7 @@ inductive GadgetPos (u v : ℕ)
   | long  (j : Fin (v-1))  -- internal vertices on the long path
 ```
 
-This gives \((u-1) + (v-1) = u+v-2\) internal vertices per gadget, matching the counting formula.
+`GadgetPos` is used by the endpoint resolution functions `localSrc` and `localTgt` to track adjacency within each gadget. The actual internal vertex positions in `FlowerVert` are stored as `Fin (u - 1) ⊕ Fin (v - 1)`, giving \((u-1) + (v-1) = u+v-2\) internal vertices per gadget, matching the counting formula.
 
 ### Edge indices
 

docs/reference/changelog.md

@@ -1,3 +1,34 @@
 # Changelog
 
 See [Releases](https://github.com/Project-Navi/fd-formalization/releases) on GitHub.
+
+---
+
+## 2026-03-28
+
+### [#12](https://github.com/Project-Navi/fd-formalization/pull/12) --- Aristotle proof golf
+
+Proof golf pass using Aristotle-discovered simplifications. Eliminates intermediate bindings and restores named squeeze waypoints in the headline theorem.
+
+**Changed files:** `FlowerConstruction.lean`, `FlowerCounts.lean`, `FlowerDiameter.lean`, `FlowerDimension.lean`, `FlowerLog.lean`, `GraphBall.lean`, `PathGraphDist.lean`
+
+Highlights:
+
+- `flowerVertCountReal_pos` and `flowerHubDistReal_pos` are now term-mode proofs (`Nat.cast_pos.mpr ...`)
+- `FlowerVert.hub0_ne_hub1` is now term-mode (`Sum.inl_injective.ne (by decide)`)
+- `hc₁_pos` in the headline theorem uses `sub_pos.mpr` pattern directly
+- Named squeeze waypoints (`h_lo`, `h_hi`, `h_res`) restored in `flowerDimension` for readability
+- Net reduction: 49 insertions, 104 deletions across 7 files
+
+### [#11](https://github.com/Project-Navi/fd-formalization/pull/11) --- Mathlib style cleanup
+
+Proof style tightening from Mathlib PR review feedback. Aligns proof idioms with upstream conventions.
+
+**Changed files:** `FlowerConstruction.lean`, `FlowerCounts.lean`, `FlowerDimension.lean`, `FlowerLog.lean`, `GraphBall.lean`, `PathGraphDist.lean`
+
+Highlights:
+
+- `flowerGraph'_adj_iff` now uses `.rfl` instead of tactic proof
+- `ball_one` and `ball_top` use `simp` proofs (leveraging `ENat.lt_one_iff_eq_zero` and `lt_top_iff_ne_top`)
+- Various `show ... from by` patterns replaced with `show ... by` (dropped deprecated `from`)
+- Net reduction: 50 insertions, 67 deletions across 7 files

docs/reference/theorems.md

@@ -150,7 +150,7 @@ def hub1 (u v g : ℕ) : Fin (flowerVertCount u v g)
 | `GadgetPos u v` | Position within a replacement gadget (src, tgt, short, long) |
 | `LocalEdge u v` | Edge index within a gadget: `Fin u ⊕ Fin v` |
 | `FlowerEdge u v g` | Recursive edge index type |
-| `FlowerVert u v g` | Vertex type: `Fin 2 ⊕ (Σ e, GadgetPos)` |
+| `FlowerVert u v g` | Vertex type: `Fin 2 ⊕ Σ (k : Fin g), FlowerEdge u v k.val × (Fin (u-1) ⊕ Fin (v-1))` |
 | `flowerGraph' u v g` | `SimpleGraph` on `FlowerVert` |
 
 ### Structural theorems