From 44fcafe0de1077f6f114d18e4cc6b572a04d3e16 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 7 Jul 2026 02:47:11 -0500 Subject: [PATCH] fix(lean): BlockCoprimeDensity round-3 fixes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds: - D_finite_eq_prod_saturated_mul_active (product decomposition thm) - saturatedPart/activePart definitions with partition and disjointness - localFactor_pos, D_finite_pos (positivity theorems) Fixes: - field_simp replaced with simpler hx + field_simp [hx] in C_finite_zero_eq_one - Docstring 'positive integer' → 'natural number' - Removed unnecessary simp, by_cases cleanup - @[simp] kept only on C_finite_zero_eq_one (unconditional) - Simpler proofs for saturatedPart_union/disjoint using Finset.filter/Subset --- formal/SilverSight/BlockCoprimeDensity.lean | 121 +++++++++++++++++--- 1 file changed, 107 insertions(+), 14 deletions(-) diff --git a/formal/SilverSight/BlockCoprimeDensity.lean b/formal/SilverSight/BlockCoprimeDensity.lean index 7a67db87..768d37e1 100644 --- a/formal/SilverSight/BlockCoprimeDensity.lean +++ b/formal/SilverSight/BlockCoprimeDensity.lean @@ -10,9 +10,11 @@ natural density is (analytically) known to be: WHAT IS FORMALIZED: • Finite truncation D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²) (ℚ) • Saturation partition: when p ≤ n+1 the factor simplifies to 1−1/p + • Decomposition into product over saturated × active primes • C_G(n) = (∏_{p ≤ G} (1−1/p²)⁻¹) · D_G(n), with C_G(0) = 1 exact - • Boundary value at n=1 (Feller-Tornier product) + • Positivity of D_G(n) and the local factors • Complementarity of saturated/active primes + • Boundary value at n=1 (Feller-Tornier product) • Eval witnesses for small G WHAT IS NOT FORMALIZED (analytic number theory, beyond scope): @@ -24,9 +26,11 @@ WHAT IS NOT FORMALIZED (analytic number theory, beyond scope): Structure: §1 Local factor and saturation partition §2 Finite Euler product D_G(n) - §3 Boundary values at n=0, n=1 and the ζ(2) cancellation - §4 Notes on analytic extensions (unformalized) - §5 Eval witnesses + §3 Product decomposition into saturated/active primes + §4 Boundary values at n=0, n=1 and the ζ(2) cancellation + §5 Positivity theorems + §6 Notes on analytic extensions (unformalized) + §7 Eval witnesses References: - Wessen Getachew, "C(n) — Block-Coprime Density" @@ -73,7 +77,7 @@ def isActive (n p : ℕ) : Prop := instance (n p : ℕ) : Decidable (isActive n p) := inferInstanceAs (Decidable (n + 1 < p)) -/-- Every positive integer is either saturated or active at block length n. -/ +/-- Every natural number is either saturated or active at block length n. -/ theorem isSaturated_or_isActive (n p : ℕ) : isSaturated n p ∨ isActive n p := by by_cases h : p ≤ n + 1 · left; exact h @@ -84,7 +88,7 @@ theorem isSaturated_iff_not_isActive (n p : ℕ) : isSaturated n p ↔ ¬isActiv unfold isSaturated isActive exact ⟨Nat.not_lt.mpr, Nat.le_of_not_gt⟩ -/-- For a saturated prime (p ≤ n+1), the local factor simplifies to 1 − 1/p. +/-- For saturated p (p ≤ n+1), the local factor simplifies to 1 − 1/p. Since min(n+1, p) = p, we have 1 − p/p² = 1 − 1/p. -/ theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n p = 1 - (1 : ℚ) / (p : ℚ) := by unfold isSaturated at h @@ -95,7 +99,7 @@ theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n · simp [hzero] · field_simp [hzero] -/-- For an active prime (p > n+1), the local factor is 1 − (n+1)/p². +/-- For active p (p > n+1), the local factor is 1 − (n+1)/p². Since min(n+1, p) = n+1, this is immediate from the definition. -/ theorem localFactor_active (n p : ℕ) (h : isActive n p) : localFactor n p = 1 - ((n+1 : ℕ) : ℚ) / ((p : ℚ) ^ 2) := by unfold isActive at h @@ -131,7 +135,69 @@ def C_finite (n G : ℕ) : ℚ := (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * D_finite n G -- ═══════════════════════════════════════════════════════════════════════════ --- §3 Boundary values and the ζ(2) cancellation +-- §3 Product decomposition into saturated/active primes +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- The saturated subset of primesUpTo G at block length n. -/ +def saturatedPart (n G : ℕ) : Finset ℕ := + (primesUpTo G).filter (fun p => decide (isSaturated n p)) + +/-- The active subset of primesUpTo G at block length n. -/ +def activePart (n G : ℕ) : Finset ℕ := + (primesUpTo G).filter (fun p => decide (isActive n p)) + +/-- The saturated and active parts partition primesUpTo G. -/ +lemma saturatedPart_union_activePart (n G : ℕ) : saturatedPart n G ∪ activePart n G = primesUpTo G := by + apply Finset.Subset.antisymm + · intro p hp + rcases Finset.mem_union.1 hp with (hp' | hp') + · exact (Finset.mem_filter.1 hp').1 + · exact (Finset.mem_filter.1 hp').1 + · intro p hp + rcases isSaturated_or_isActive n p with (h_sat | h_act) + · apply Finset.mem_union_left + refine Finset.mem_filter.mpr ⟨hp, ?_⟩ + exact decide_eq_true h_sat + · apply Finset.mem_union_right + refine Finset.mem_filter.mpr ⟨hp, ?_⟩ + exact decide_eq_true h_act + +/-- The saturated and active parts are disjoint. -/ +lemma saturatedPart_disjoint_activePart (n G : ℕ) : Disjoint (saturatedPart n G) (activePart n G) := by + rw [Finset.disjoint_iff_inter_eq_empty] + by_contra hne + have h_nonempty : (saturatedPart n G ∩ activePart n G).Nonempty := by + rw [Finset.nonempty_iff_ne_empty] + exact hne + rcases h_nonempty with ⟨p, hp⟩ + rcases Finset.mem_inter.1 hp with ⟨hp_sat, hp_act⟩ + have hp_sat_pair := Finset.mem_filter.mp (by simpa [saturatedPart] using hp_sat) + have hp_act_pair := Finset.mem_filter.mp (by simpa [activePart] using hp_act) + have hp_sat_pure : isSaturated n p := hp_sat_pair.2 + have hp_act_pure : isActive n p := hp_act_pair.2 + unfold isSaturated at hp_sat_pure + unfold isActive at hp_act_pure + omega + +/-- D_finite(n, G) decomposes into a product over saturated primes times a + product over active primes. Applying `localFactor_saturated` and + `localFactor_active` to each factor gives the explicit form: + + D_finite n G = (∏_{saturated} (1 − 1/p)) · (∏_{active} (1 − (n+1)/p²)) -/ +theorem D_finite_eq_prod_saturated_mul_active (n G : ℕ) : D_finite n G = + (Finset.prod (saturatedPart n G) (fun p => localFactor n p)) * + (Finset.prod (activePart n G) (fun p => localFactor n p)) := by + unfold D_finite + calc + Finset.prod (primesUpTo G) (fun p => localFactor n p) + = Finset.prod (saturatedPart n G ∪ activePart n G) (fun p => localFactor n p) := by + rw [saturatedPart_union_activePart] + _ = (Finset.prod (saturatedPart n G) (fun p => localFactor n p)) * + (Finset.prod (activePart n G) (fun p => localFactor n p)) := by + rw [Finset.prod_union (saturatedPart_disjoint_activePart n G)] + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §4 Boundary values and the ζ(2) cancellation -- ═══════════════════════════════════════════════════════════════════════════ /-- For n=0, every prime is active (since the smallest prime is 2 > 1). @@ -161,12 +227,14 @@ lemma D_finite_zero_eq (G : ℕ) : D_finite 0 G = Finset.prod (primesUpTo G) (fu have h : ∀ p ∈ primesUpTo G, (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹ * (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) = 1 := by intro p hp have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2 - have hp_pos : p ≠ 0 := Nat.Prime.ne_zero hp_prime - have hp_sq_ne_zero : (p : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 (by exact_mod_cast hp_pos) - have hp_sq_minus_one_ne_zero : (p : ℚ) ^ 2 - 1 ≠ 0 := by + have hp_sq_ne_zero : (p : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 (by exact_mod_cast (Nat.Prime.ne_zero hp_prime)) + have hx : (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) ≠ 0 := by have hp_gt_one : (p : ℚ) > 1 := by exact_mod_cast (Nat.Prime.one_lt hp_prime) + have hp_sq_gt_one : (p : ℚ) ^ 2 > 1 := by nlinarith + have hp_sq_pos : 0 < (p : ℚ) ^ 2 := by nlinarith + have hdiv : (1 : ℚ) / ((p : ℚ) ^ 2) < 1 := (div_lt_one hp_sq_pos).mpr hp_sq_gt_one nlinarith - field_simp [hp_sq_ne_zero, hp_sq_minus_one_ne_zero] + field_simp [hx] calc (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * D_finite 0 G = (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * @@ -200,7 +268,32 @@ lemma D_finite_one_eq (G : ℕ) : D_finite 1 G = Finset.prod (primesUpTo G) (fun simp [localFactor_one_prime p hp_prime] -- ═══════════════════════════════════════════════════════════════════════════ --- §4 Notes on analytic extensions (unformalized) +-- §5 Positivity +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- For a prime p ≥ 2, the local factor is strictly positive. -/ +lemma localFactor_pos (n p : ℕ) (hp : Nat.Prime p) : localFactor n p > 0 := by + unfold localFactor + have hp_gt_one : (p : ℚ) > 1 := by exact_mod_cast (Nat.Prime.one_lt hp) + have hp_sq_gt_one : (p : ℚ) ^ 2 > 1 := by nlinarith + have hp_sq_pos : 0 < (p : ℚ) ^ 2 := by nlinarith + have h_num_le_denom : (min (n+1) p : ℚ) < (p : ℚ) ^ 2 := by + calc + (min (n+1) p : ℚ) ≤ (p : ℚ) := by exact_mod_cast Nat.min_le_right (n+1) p + _ < (p : ℚ) ^ 2 := by nlinarith + have h_div_lt_one : (min (n+1) p : ℚ) / ((p : ℚ) ^ 2) < 1 := + (div_lt_one hp_sq_pos).mpr h_num_le_denom + nlinarith + +/-- D_G(n) is strictly positive for any G. -/ +theorem D_finite_pos (n G : ℕ) : D_finite n G > 0 := by + unfold D_finite + refine Finset.prod_pos fun p hp => ?_ + have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2 + exact localFactor_pos n p hp_prime + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §6 Notes on analytic extensions (unformalized) -- ═══════════════════════════════════════════════════════════════════════════ /- @@ -229,7 +322,7 @@ identification as a density is not proven here. -/ -- ═══════════════════════════════════════════════════════════════════════════ --- §5 Eval witnesses +-- §7 Eval witnesses -- ═══════════════════════════════════════════════════════════════════════════ -- D_G(0) at G=31 (first 11 primes): ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.61174