From bf4cf3d4f730e65750e6ee1175a58345e3ab938d Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Sat, 28 Mar 2026 21:00:49 -0500 Subject: [PATCH 1/2] =?UTF-8?q?refactor:=20proof=20golf=20from=20Aristotle?= =?UTF-8?q?=20=E2=80=94=20eliminate=20intermediate=20bindings?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cherry-pick proof simplifications from Aristotle 4.28.0 output, preserving all docstrings, imports, and module documentation. Key changes: - Inline named `have h1`/`have h2` into `zify [show ...]` patterns - Convert trivial tactic blocks to term-mode proofs - Remove unused `hlogw` binding in headline theorem - Inline intermediate variables in squeeze theorem bounds - `flowerGraph'_adj_iff` via `Iff.rfl` instead of id/id constructor - `flowerGraph'` definition in term-mode instead of tactic block - Eliminate redundant named intermediates across GraphBall, PathGraphDist Net: -75 lines across 7 files. Zero sorry, clean axioms, lint passes. --- FdFormal/FlowerConstruction.lean | 74 +++++++++++--------------------- FdFormal/FlowerCounts.lean | 27 ++++-------- FdFormal/FlowerDiameter.lean | 9 ++-- FdFormal/FlowerDimension.lean | 33 +++----------- FdFormal/FlowerLog.lean | 8 ++-- FdFormal/GraphBall.lean | 6 +-- FdFormal/PathGraphDist.lean | 7 +-- 7 files changed, 51 insertions(+), 113 deletions(-) diff --git a/FdFormal/FlowerConstruction.lean b/FdFormal/FlowerConstruction.lean index 0d80f29..25f7664 100644 --- a/FdFormal/FlowerConstruction.lean +++ b/FdFormal/FlowerConstruction.lean @@ -140,8 +140,8 @@ def FlowerVert.hub0 (u v g : ℕ) : FlowerVert u v g := .inl 0 def FlowerVert.hub1 (u v g : ℕ) : FlowerVert u v g := .inl 1 theorem FlowerVert.hub0_ne_hub1 (u v g : ℕ) : - FlowerVert.hub0 u v g ≠ FlowerVert.hub1 u v g := by - unfold hub0 hub1; exact Sum.inl_injective.ne (by decide) + FlowerVert.hub0 u v g ≠ FlowerVert.hub1 u v g := + Sum.inl_injective.ne (by decide) /-- Embed a vertex from generation `g` into generation `g+1`. Hubs stay hubs. Internal vertices keep their identity (the generation @@ -179,11 +179,8 @@ theorem FlowerVert.embed_ne_new {u v g : ℕ} (x : FlowerVert u v g) cases x with | inl _ => simp [embed] | inr val => - intro h - have h := Sum.inr_injective h - have hk := congr_arg (fun s => (Sigma.fst s).val) h - simp only [Fin.val_castSucc] at hk - omega + intro h; have hk := congr_arg (fun s => (Sigma.fst s).val) (Sum.inr_injective h) + simp only [Fin.val_castSucc] at hk; omega /-- Within a single gadget, source and target positions are always distinct when `1 < u`. -/ @@ -250,16 +247,10 @@ theorem edgeSrc_ne_edgeTgt (u v g : ℕ) (e : FlowerEdge u v g) : have hpar := ih parent have hloc := localSrc_ne_localTgt u v localE simp only [edgeEndpoints, edgeSrc, edgeTgt] at hpar ⊢ - -- Case-split on localSrc/localTgt values rcases hs : localSrc u v localE with src | tgt | ⟨i⟩ | ⟨j⟩ <;> rcases ht : localTgt u v localE with src | tgt | ⟨i'⟩ | ⟨j'⟩ <;> - simp only [hs, ht] at hloc ⊢ - -- 16 cases from (localSrc × localTgt). Four closure patterns: - -- 1. absurd rfl hloc: same position (src=src, tgt=tgt) contradicts hloc - -- 2. embed_injective.ne: both endpoints are embedded, use inductive hypothesis - -- 3. embed_ne_new: one endpoint is embedded, the other is a new vertex - -- 4. Sum.inr_injective + simp_all: both are new vertices, extract index equality - all_goals first + simp only [hs, ht] at hloc ⊢ <;> + first | exact absurd rfl hloc | exact FlowerVert.embed_injective.ne hpar | exact Ne.symm (FlowerVert.embed_injective.ne hpar) @@ -399,12 +390,10 @@ theorem gadget_adj_chain (u v g : ℕ) (hu : 1 < u) /-- The (u,v)-flower as a `SimpleGraph` on `FlowerVert`. Construction requires `edgeSrc_ne_edgeTgt` for irreflexivity. -/ noncomputable def flowerGraph' (u v g : ℕ) : - SimpleGraph (FlowerVert u v g) := by - refine SimpleGraph.mk (flowerAdj' u v g) ?_ ?_ - · -- symmetry - intro a b ⟨e, h⟩; exact ⟨e, h.symm⟩ - · -- irreflexivity - exact ⟨fun a ⟨e, h⟩ => by + SimpleGraph (FlowerVert u v g) := + SimpleGraph.mk (flowerAdj' u v g) + (fun _ _ ⟨e, h⟩ => ⟨e, h.symm⟩) + ⟨fun a ⟨e, h⟩ => by rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;> exact edgeSrc_ne_edgeTgt u v g e (h1 ▸ h2)⟩ @@ -434,9 +423,7 @@ theorem gadget_short_walk (u v g : ℕ) (hu : 1 < u) | zero => exact ⟨.nil, rfl⟩ | succ k ih => obtain ⟨w, hw⟩ := ih (by omega) - exact ⟨w.append (.cons (hadj ⟨k, by omega⟩) .nil), by - simp only [SimpleGraph.Walk.length_append, SimpleGraph.Walk.length_cons, - SimpleGraph.Walk.length_nil, hw]⟩ + exact ⟨w.append (.cons (hadj ⟨k, by omega⟩) .nil), by simp [hw]⟩ /-- Adjacent vertices in gen `g` are connected by a walk of length `u` in gen `g+1` (through the replacement gadget's short path). -/ @@ -467,8 +454,7 @@ theorem lift_walk (u v g : ℕ) (hu : 1 < u) {a b : FlowerVert u v g} obtain ⟨w_tail, hw_tail⟩ := ih exact ⟨w_step.append w_tail, by rw [SimpleGraph.Walk.length_append, hw_step, hw_tail, - SimpleGraph.Walk.length_cons, Nat.mul_succ] - omega⟩ + SimpleGraph.Walk.length_cons, Nat.mul_succ]; omega⟩ /-- **Upper bound**: there exists a walk of length `u^g` between hubs. @@ -480,8 +466,7 @@ theorem flowerGraph'_walk_hubs (u v g : ℕ) (hu : 1 < u) : w.length = u ^ g := by induction g with | zero => - exact ⟨.cons (⟨(), Or.inl ⟨rfl, rfl⟩⟩ : (flowerGraph' u v 0).Adj _ _) .nil, - by simp [SimpleGraph.Walk.length]⟩ + exact ⟨.cons (⟨(), Or.inl ⟨rfl, rfl⟩⟩ : (flowerGraph' u v 0).Adj _ _) .nil, by simp⟩ | succ g ih => obtain ⟨w, hw⟩ := ih obtain ⟨w', hw'⟩ := lift_walk u v g hu w @@ -640,8 +625,7 @@ def FlowerVert.rank (u v : ℕ) : (g : ℕ) → FlowerVert u v g → ℕ if hk : k.val < g then u * rank u v g (.inr ⟨⟨k.val, hk⟩, parent, pos⟩) else - have hkg : k.val = g := by omega - let parent' : FlowerEdge u v g := hkg ▸ parent + let parent' : FlowerEdge u v g := (show k.val = g by omega) ▸ parent let srcR := rank u v g (edgeSrc u v g parent') let tgtR := rank u v g (edgeTgt u v g parent') if srcR = tgtR then u * srcR @@ -794,8 +778,7 @@ theorem walk_length_ge_rank (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) | nil => omega | cons hab tail ih => have hadj := rank_adj_le u v g hu huv _ _ hab - simp only [SimpleGraph.Walk.length_cons] - omega + simp only [SimpleGraph.Walk.length_cons]; omega /-- **Lower bound**: hub distance ≥ u^g. @@ -803,13 +786,10 @@ Uses the rank function as a 1-Lipschitz potential: any walk from hub0 (rank 0) to hub1 (rank u^g) has length ≥ u^g. -/ theorem flowerGraph'_dist_ge (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : u ^ g ≤ (flowerGraph' u v g).dist (.hub0 u v g) (.hub1 u v g) := by - obtain ⟨w, hw⟩ := flowerGraph'_walk_hubs u v g hu - have hreach : (flowerGraph' u v g).Reachable (.hub0 u v g) (.hub1 u v g) := - ⟨w⟩ - obtain ⟨p, hp⟩ := hreach.exists_walk_length_eq_dist + obtain ⟨p, hp⟩ := + (flowerGraph'_walk_hubs u v g hu).choose.reachable.exists_walk_length_eq_dist have := walk_length_ge_rank u v g hu huv p - rw [rank_hub0, rank_hub1] at this - omega + rw [rank_hub0, rank_hub1] at this; omega /-- **F2 bridge on FlowerVert**: hub distance = u^g. -/ theorem flowerGraph'_dist_hubs (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : @@ -848,7 +828,7 @@ theorem flowerVert_card (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : /-- Equivalence to `Fin (flowerVertCount u v g)`. -/ noncomputable def flowerVertEquiv (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : FlowerVert u v g ≃ Fin (flowerVertCount u v g) := - (Fintype.equivFinOfCardEq (flowerVert_card u v g hu huv)) + Fintype.equivFinOfCardEq (flowerVert_card u v g hu huv) /-- The (u,v)-flower on `Fin`. -/ noncomputable def flowerGraph (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : @@ -876,23 +856,17 @@ theorem flowerGraph_dist_hubs (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : change G.Adj (e.symm (e a)) (e.symm (e b)) simp only [Equiv.symm_apply_apply]; exact h apply le_antisymm - · -- ≤: walk in G maps to walk in G' - obtain ⟨w, hw⟩ := (flowerGraph'_connected u v g hu huv).exists_walk_length_eq_dist + · obtain ⟨w, hw⟩ := (flowerGraph'_connected u v g hu huv).exists_walk_length_eq_dist (.hub0 u v g) (.hub1 u v g) calc G'.dist (e (.hub0 u v g)) (e (.hub1 u v g)) ≤ (w.map ⟨e, @hom_fwd⟩).length := SimpleGraph.dist_le _ - _ = w.length := SimpleGraph.Walk.length_map _ _ - _ = _ := hw - · -- ≥: walk in G' maps to walk in G (e.symm preserves adjacency) - have hreach : G'.Reachable (e (.hub0 u v g)) (e (.hub1 u v g)) := by - obtain ⟨w, _⟩ := flowerGraph'_walk_hubs u v g hu - exact (w.map ⟨e, @hom_fwd⟩).reachable + _ = _ := by rw [SimpleGraph.Walk.length_map, hw] + · have hreach : G'.Reachable (e (.hub0 u v g)) (e (.hub1 u v g)) := + ((flowerGraph'_walk_hubs u v g hu).choose.map ⟨e, @hom_fwd⟩).reachable obtain ⟨w', hw'⟩ := hreach.exists_walk_length_eq_dist calc G.dist _ _ ≤ ((w'.map ⟨e.symm, @hom_back⟩).copy (e.symm_apply_apply _) (e.symm_apply_apply _)).length := SimpleGraph.dist_le _ - _ = w'.length := by - rw [SimpleGraph.Walk.length_copy, SimpleGraph.Walk.length_map] - _ = G'.dist _ _ := hw' + _ = G'.dist _ _ := by rw [SimpleGraph.Walk.length_copy, SimpleGraph.Walk.length_map, hw'] /-! ## Projection map (for lower bound proof) diff --git a/FdFormal/FlowerCounts.lean b/FdFormal/FlowerCounts.lean index 5e8d579..7547ff2 100644 --- a/FdFormal/FlowerCounts.lean +++ b/FdFormal/FlowerCounts.lean @@ -107,10 +107,7 @@ theorem flowerVertCount_eq (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : omega | succ g ih => simp only [flowerVertCount_succ, flowerEdgeCount_eq_pow, pow_succ] - have h1 : 1 ≤ u + v := by omega - have h2 : 2 ≤ u + v := by omega - zify [h1, h2] at ih ⊢ - nlinarith [ih] + zify [show 1 ≤ u + v by omega, show 2 ≤ u + v by omega] at ih ⊢; nlinarith /-- The vertex count is always positive (holds for all `u`, `v`). -/ theorem flowerVertCount_pos (u v g : ℕ) : @@ -132,14 +129,10 @@ theorem flowerVertCount_lower (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : /-- Upper bound: `(w - 1) * N_g ≤ 2 * (w - 1) * w^g`. -/ theorem flowerVertCount_upper (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : - (u + v - 1) * flowerVertCount u v g ≤ - 2 * (u + v - 1) * (u + v) ^ g := by + (u + v - 1) * flowerVertCount u v g ≤ 2 * (u + v - 1) * (u + v) ^ g := by rw [flowerVertCount_eq u v g hu huv] - have h1 : 1 ≤ u + v := by omega - have h2 : 2 ≤ u + v := by omega have h_pow : 1 ≤ (u + v) ^ g := Nat.one_le_pow _ _ (by omega) - zify [h1, h2] at h_pow ⊢ - nlinarith [h_pow] + zify [show 1 ≤ u + v by omega, show 2 ≤ u + v by omega] at h_pow ⊢; nlinarith /-! ### Monotonicity -/ @@ -163,11 +156,10 @@ theorem flowerVertCount_cast_eq (u v g : ℕ) (hu : 1 < u) (huv : u ≤ v) : (↑(u + v) - 1 : ℝ) * (↑(flowerVertCount u v g) : ℝ) = (↑(u + v) - 2 : ℝ) * (↑(u + v) : ℝ) ^ g + (↑(u + v) : ℝ) := by have h := flowerVertCount_eq u v g hu huv - have h_cast := congr_arg (Nat.cast (R := ℝ)) h - simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_add] at h_cast - rw [Nat.cast_sub (by omega : 2 ≤ u + v), - Nat.cast_sub (by omega : 1 ≤ u + v)] at h_cast - exact_mod_cast h_cast + have := congr_arg (Nat.cast (R := ℝ)) h + simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_add] at this + rw [Nat.cast_sub (by omega), Nat.cast_sub (by omega)] at this + exact_mod_cast this /-! ### Real-valued wrappers -/ @@ -177,6 +169,5 @@ noncomputable def flowerVertCountReal (u v : ℕ) (g : ℕ) : ℝ := /-- The real-valued vertex count is positive. -/ theorem flowerVertCountReal_pos (u v g : ℕ) : - 0 < flowerVertCountReal u v g := by - simp only [flowerVertCountReal] - exact Nat.cast_pos.mpr (flowerVertCount_pos u v g) + 0 < flowerVertCountReal u v g := + Nat.cast_pos.mpr (flowerVertCount_pos u v g) diff --git a/FdFormal/FlowerDiameter.lean b/FdFormal/FlowerDiameter.lean index b1702c4..62a8e6d 100644 --- a/FdFormal/FlowerDiameter.lean +++ b/FdFormal/FlowerDiameter.lean @@ -78,8 +78,8 @@ theorem flowerHubDist_pos (u v g : ℕ) (hu : 1 < u) : /-- Hub distance grows strictly between generations. -/ theorem flowerHubDist_strict_mono (u v g : ℕ) (hu : 1 < u) : - flowerHubDist u v g < flowerHubDist u v (g + 1) := by - exact lt_mul_of_one_lt_left (flowerHubDist_pos u v g hu) hu + flowerHubDist u v g < flowerHubDist u v (g + 1) := + lt_mul_of_one_lt_left (flowerHubDist_pos u v g hu) hu /-! ### Cast identity -/ @@ -96,6 +96,5 @@ noncomputable def flowerHubDistReal (u v g : ℕ) : ℝ := /-- The real-valued hub distance is positive when `1 < u`. -/ theorem flowerHubDistReal_pos (u v g : ℕ) (hu : 1 < u) : - 0 < flowerHubDistReal u v g := by - simp only [flowerHubDistReal] - exact Nat.cast_pos.mpr (flowerHubDist_pos u v g hu) + 0 < flowerHubDistReal u v g := + Nat.cast_pos.mpr (flowerHubDist_pos u v g hu) diff --git a/FdFormal/FlowerDimension.lean b/FdFormal/FlowerDimension.lean index 6e03988..dc5ad14 100644 --- a/FdFormal/FlowerDimension.lean +++ b/FdFormal/FlowerDimension.lean @@ -105,7 +105,6 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) : log ↑(flowerHubDist u v g)) atTop (nhds (log ↑(u + v) / log ↑u)) := by - -- Positivity have hlogu : 0 < log (↑u : ℝ) := log_pos (by exact_mod_cast hu) have hlogw : 0 < log (↑(u + v) : ℝ) := @@ -129,29 +128,20 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) : filter_upwards [eventually_gt_atTop 0] with g hg rw [h_log_hub] -- Step 3: Decompose ratio = residual + constant - -- log(N_g)/(g*log u) = [log(N_g) - g*log w]/(g*log u) + log w/log u have h_decomp : ∀ g : ℕ, 0 < (↑g : ℝ) → log ↑(flowerVertCount u v g) / (↑g * log (↑u : ℝ)) = (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) / (↑g * log (↑u : ℝ)) + log ↑(u + v) / log (↑u : ℝ) := by - intro g hg - have hg_ne : (↑g : ℝ) ≠ 0 := ne_of_gt hg - have hlogu_ne : log (↑u : ℝ) ≠ 0 := ne_of_gt hlogu - field_simp - ring + intro g hg; field_simp; ring -- Step 4: Show residual → 0 - -- The residual is bounded between log(c₁)/(g*log u) and log(2)/(g*log u) - -- where c₁ = (w-2)/(w-1) > 0 set c₁ := (↑(u + v) - 2 : ℝ) / (↑(u + v) - 1) with hc₁_def have hc₁_pos : 0 < c₁ := div_pos (sub_pos.mpr (by exact_mod_cast (show 2 < u + v by omega))) (sub_pos.mpr (by exact_mod_cast (show 1 < u + v by omega))) - -- g * log(u) → ∞ have h_denom : Tendsto (fun g : ℕ ↦ (↑g : ℝ) * log (↑u : ℝ)) atTop atTop := Tendsto.atTop_mul_const hlogu (tendsto_natCast_atTop_atTop (R := ℝ)) - -- Lower bound: log(c₁) ≤ log(N_g) - g * log(w) have h_res_lower : ∀ᶠ g in atTop, log c₁ / (↑g * log (↑u : ℝ)) ≤ (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) / @@ -159,14 +149,11 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) : filter_upwards [eventually_gt_atTop 0] with g hg have hg_pos : (0 : ℝ) < ↑g := Nat.cast_pos.mpr hg rw [div_le_div_iff_of_pos_right (mul_pos hg_pos hlogu)] - have h_bound := flowerVertCount_ge_real u v g hu huv - have h_cw_pos : 0 < c₁ * (↑(u + v) : ℝ) ^ g := - mul_pos hc₁_pos (pow_pos hw_pos g) - have h_log := log_le_log h_cw_pos h_bound + have h_log := log_le_log (mul_pos hc₁_pos (pow_pos hw_pos g)) + (flowerVertCount_ge_real u v g hu huv) rw [log_mul (ne_of_gt hc₁_pos) (ne_of_gt (pow_pos hw_pos g)), log_pow] at h_log linarith - -- Upper bound: log(N_g) - g * log(w) ≤ log(2) have h_res_upper : ∀ᶠ g in atTop, (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) / (↑g * log (↑u : ℝ)) ≤ @@ -174,26 +161,18 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) : filter_upwards [eventually_gt_atTop 0] with g hg have hg_pos : (0 : ℝ) < ↑g := Nat.cast_pos.mpr hg rw [div_le_div_iff_of_pos_right (mul_pos hg_pos hlogu)] - have h_bound := flowerVertCount_le_real u v g hu huv - have h_log := log_le_log (hN_pos g) h_bound + have h_log := log_le_log (hN_pos g) (flowerVertCount_le_real u v g hu huv) rw [log_mul (by norm_num : (2 : ℝ) ≠ 0) (ne_of_gt (pow_pos hw_pos g)), log_pow] at h_log linarith - -- Both bounds → 0 - have h_lo : Tendsto (fun g : ℕ ↦ log c₁ / (↑g * log (↑u : ℝ))) - atTop (nhds 0) := - h_denom.const_div_atTop _ - have h_hi : Tendsto (fun g : ℕ ↦ log 2 / (↑g * log (↑u : ℝ))) - atTop (nhds 0) := - h_denom.const_div_atTop _ - -- Squeeze: residual → 0 have h_res : Tendsto (fun g : ℕ ↦ (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) / (↑g * log (↑u : ℝ))) atTop (nhds 0) := - h_lo.squeeze' h_hi h_res_lower h_res_upper + (h_denom.const_div_atTop _).squeeze' (h_denom.const_div_atTop _) + h_res_lower h_res_upper -- Step 5: residual + constant → 0 + constant = constant have h_sum := h_res.add (tendsto_const_nhds (x := log (↑(u + v) : ℝ) / log (↑u : ℝ))) diff --git a/FdFormal/FlowerLog.lean b/FdFormal/FlowerLog.lean index a06f76e..282d571 100644 --- a/FdFormal/FlowerLog.lean +++ b/FdFormal/FlowerLog.lean @@ -74,11 +74,11 @@ theorem log_flowerVertCount_residual_lower : have h_ge : (↑(u + v) - 2) / (↑(u + v) - 1) * (↑(u + v) : ℝ) ^ g ≤ ↑(flowerVertCount u v g) := by rw [div_mul_eq_mul_div, div_le_iff₀ hw1] - have h_cast := Nat.cast_le (α := ℝ) |>.mpr (flowerVertCount_lower u v g hu huv) - simp only [Nat.cast_mul, Nat.cast_pow] at h_cast + have := Nat.cast_le (α := ℝ) |>.mpr (flowerVertCount_lower u v g hu huv) + simp only [Nat.cast_mul, Nat.cast_pow] at this rw [Nat.cast_sub (by omega : 2 ≤ u + v), - Nat.cast_sub (by omega : 1 ≤ u + v)] at h_cast - simp only [Nat.cast_ofNat, Nat.cast_one] at h_cast + Nat.cast_sub (by omega : 1 ≤ u + v)] at this + simp only [Nat.cast_ofNat, Nat.cast_one] at this linarith [mul_comm (↑(u + v) - 1 : ℝ) (↑(flowerVertCount u v g) : ℝ)] have h_log := log_le_log (mul_pos hc (pow_pos hw_pos g)) h_ge rw [log_mul (ne_of_gt hc) (ne_of_gt (pow_pos hw_pos g)), log_pow] at h_log diff --git a/FdFormal/GraphBall.lean b/FdFormal/GraphBall.lean index 387d486..3a63756 100644 --- a/FdFormal/GraphBall.lean +++ b/FdFormal/GraphBall.lean @@ -129,10 +129,8 @@ 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₂) := 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 + 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 (ne_top_of_lt hw)).mpr hv _ ≤ r₁ + r₂ := by gcongr end SimpleGraph diff --git a/FdFormal/PathGraphDist.lean b/FdFormal/PathGraphDist.lean index 07ca96d..3ce16de 100644 --- a/FdFormal/PathGraphDist.lean +++ b/FdFormal/PathGraphDist.lean @@ -112,13 +112,10 @@ theorem pathGraph_edist {n : ℕ} (i j : Fin (n + 1)) : · obtain ⟨w', hw'⟩ := pathGraph_walk_le (show j.val ≤ i.val by omega) exact ⟨w'.reverse, by rw [Walk.length_reverse, hw']⟩ apply le_antisymm - · -- Upper: edist ≤ walk length = target - calc (pathGraph (n + 1)).edist i j + · calc (pathGraph (n + 1)).edist i j ≤ ↑w.length := edist_le w _ = _ := by exact_mod_cast hw - · -- Lower: target ≤ every walk length → target ≤ iInf - simp only [edist] - exact le_iInf fun w' ↦ by exact_mod_cast pathGraph_walk_length_ge w' + · exact le_iInf fun w' ↦ by exact_mod_cast pathGraph_walk_length_ge w' /-! ### Distance formula -/ From 5e32d8a94964203cb04a6737814b98e7e0adef9e Mon Sep 17 00:00:00 2001 From: Nelson Spence Date: Sat, 28 Mar 2026 21:04:49 -0500 Subject: [PATCH 2/2] refactor: restore named squeeze waypoints in headline theorem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Revert the h_lo/h_hi/h_res inlining in flowerDimension — the named intermediates are Mathlib-shaped and match the Route B squeeze narrative advertised in module docs. --- FdFormal/FlowerDimension.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/FdFormal/FlowerDimension.lean b/FdFormal/FlowerDimension.lean index dc5ad14..2f815dc 100644 --- a/FdFormal/FlowerDimension.lean +++ b/FdFormal/FlowerDimension.lean @@ -166,13 +166,20 @@ theorem flowerDimension (u v : ℕ) (hu : 1 < u) (huv : u ≤ v) : (ne_of_gt (pow_pos hw_pos g)), log_pow] at h_log linarith + -- Both bounds → 0 + have h_lo : Tendsto (fun g : ℕ ↦ log c₁ / (↑g * log (↑u : ℝ))) + atTop (nhds 0) := + h_denom.const_div_atTop _ + have h_hi : Tendsto (fun g : ℕ ↦ log 2 / (↑g * log (↑u : ℝ))) + atTop (nhds 0) := + h_denom.const_div_atTop _ + -- Squeeze: residual → 0 have h_res : Tendsto (fun g : ℕ ↦ (log ↑(flowerVertCount u v g) - ↑g * log ↑(u + v)) / (↑g * log (↑u : ℝ))) atTop (nhds 0) := - (h_denom.const_div_atTop _).squeeze' (h_denom.const_div_atTop _) - h_res_lower h_res_upper + h_lo.squeeze' h_hi h_res_lower h_res_upper -- Step 5: residual + constant → 0 + constant = constant have h_sum := h_res.add (tendsto_const_nhds (x := log (↑(u + v) : ℝ) / log (↑u : ℝ)))