From 0fa9b0c99d5cc6e914468bd2c6f473411f259202 Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 29 Aug 2026 17:23:30 +0530 Subject: [PATCH 1/5] =?UTF-8?q?Exhibit=20infinite=20descents=20in=20?= =?UTF-8?q?=E2=84=A4=20and=20positive=20=E2=84=9A?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Negated naturals decrease unboundedly in ℤ; reciprocal naturals do so among positive rationals. --- Analysis/Section_4_4.lean | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean index 64c42e552..fca8be365 100644 --- a/Analysis/Section_4_4.lean +++ b/Analysis/Section_4_4.lean @@ -50,13 +50,23 @@ theorem Nat.no_infinite_descent : ¬ ∃ a:ℕ → ℕ, ∀ n, a (n+1) < a n := /-- Exercise 4.4.2 (b) -/ def Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) := by - -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. - sorry + apply isTrue + refine ⟨fun n ↦ - (n:ℤ), ?_⟩ + intro n + -- -(n+1) < -n + simp + exact Nat.cast_lt.mpr n.lt_succ_self /-- Exercise 4.4.2 (b') -/ def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n, a (n+1) < a n) := by - -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. - sorry + apply isTrue + refine ⟨fun n ↦ ⟨(1 : ℚ) / (n + 1), by positivity⟩, ?_⟩ + intro n + change (1 : ℚ) / (n + 1 + 1) < 1 / (n + 1) + have h1 : (0 : ℚ) < n + 1 := by positivity + have h2 : (0 : ℚ) < n + 2 := by positivity + rw [div_lt_div_iff₀ h2 h1] + linarith #check even_iff_exists_two_mul #check odd_iff_exists_bit1 From ef162a5778c947696d241f24406851dabda24257 Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 29 Aug 2026 18:42:53 +0530 Subject: [PATCH 2/5] fix integer and rational infinite descent proofs --- Analysis/Section_4_4.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean index fca8be365..83e435ed5 100644 --- a/Analysis/Section_4_4.lean +++ b/Analysis/Section_4_4.lean @@ -53,20 +53,20 @@ def Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) : apply isTrue refine ⟨fun n ↦ - (n:ℤ), ?_⟩ intro n - -- -(n+1) < -n + -- simp closes -(n+1) < -n simp - exact Nat.cast_lt.mpr n.lt_succ_self /-- Exercise 4.4.2 (b') -/ def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n, a (n+1) < a n) := by apply isTrue refine ⟨fun n ↦ ⟨(1 : ℚ) / (n + 1), by positivity⟩, ?_⟩ intro n - change (1 : ℚ) / (n + 1 + 1) < 1 / (n + 1) - have h1 : (0 : ℚ) < n + 1 := by positivity - have h2 : (0 : ℚ) < n + 2 := by positivity - rw [div_lt_div_iff₀ h2 h1] - linarith + have h1 : (0 : ℚ) < (n : ℚ) + 1 := by positivity + have h2 : (0 : ℚ) < (n : ℚ) + 2 := by positivity + have : (1 : ℚ) / ((n : ℚ) + 2) < 1 / ((n : ℚ) + 1) := by + rw [div_lt_div_iff₀ h2 h1] + linarith + simpa using this #check even_iff_exists_two_mul #check odd_iff_exists_bit1 From 42a40d4d8afd1a64247197c597148a4ea98ee19e Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 29 Aug 2026 19:08:51 +0530 Subject: [PATCH 3/5] match rational descent inequality to n+1+1 form --- Analysis/Section_4_4.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean index 83e435ed5..7215604f8 100644 --- a/Analysis/Section_4_4.lean +++ b/Analysis/Section_4_4.lean @@ -62,11 +62,11 @@ def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n refine ⟨fun n ↦ ⟨(1 : ℚ) / (n + 1), by positivity⟩, ?_⟩ intro n have h1 : (0 : ℚ) < (n : ℚ) + 1 := by positivity - have h2 : (0 : ℚ) < (n : ℚ) + 2 := by positivity - have : (1 : ℚ) / ((n : ℚ) + 2) < 1 / ((n : ℚ) + 1) := by + have h2 : (0 : ℚ) < (n : ℚ) + 1 + 1 := by positivity + have : (1 : ℚ) / ((n : ℚ) + 1 + 1) < 1 / ((n : ℚ) + 1) := by rw [div_lt_div_iff₀ h2 h1] linarith - simpa using this + exact this #check even_iff_exists_two_mul #check odd_iff_exists_bit1 From 3fc676ef5d597c30af9e1cb8b451a0ac23049c5f Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 29 Aug 2026 19:32:23 +0530 Subject: [PATCH 4/5] use Subtype.mk_lt_mk for positive rational descent --- Analysis/Section_4_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean index 7215604f8..ec82b7092 100644 --- a/Analysis/Section_4_4.lean +++ b/Analysis/Section_4_4.lean @@ -66,7 +66,7 @@ def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n have : (1 : ℚ) / ((n : ℚ) + 1 + 1) < 1 / ((n : ℚ) + 1) := by rw [div_lt_div_iff₀ h2 h1] linarith - exact this + exact Subtype.mk_lt_mk.mpr this #check even_iff_exists_two_mul #check odd_iff_exists_bit1 From ddac3ab7bfb5fda0cc5438e0766a46f5b8db5573 Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 29 Aug 2026 19:44:13 +0530 Subject: [PATCH 5/5] align rational descent cast with Nat.succ form --- Analysis/Section_4_4.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean index ec82b7092..5bbee7ed2 100644 --- a/Analysis/Section_4_4.lean +++ b/Analysis/Section_4_4.lean @@ -61,12 +61,13 @@ def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n apply isTrue refine ⟨fun n ↦ ⟨(1 : ℚ) / (n + 1), by positivity⟩, ?_⟩ intro n + simp only [Subtype.mk_lt_mk] + -- goal: 1 / (↑(n + 1) + 1) < 1 / (↑n + 1) have h1 : (0 : ℚ) < (n : ℚ) + 1 := by positivity - have h2 : (0 : ℚ) < (n : ℚ) + 1 + 1 := by positivity - have : (1 : ℚ) / ((n : ℚ) + 1 + 1) < 1 / ((n : ℚ) + 1) := by - rw [div_lt_div_iff₀ h2 h1] - linarith - exact Subtype.mk_lt_mk.mpr this + have h2 : (0 : ℚ) < ((n + 1 : ℕ) : ℚ) + 1 := by positivity + rw [div_lt_div_iff₀ h2 h1] + push_cast + linarith #check even_iff_exists_two_mul #check odd_iff_exists_bit1