From 1b1dbc88f7dfacba68b856e8aadae639ede3ec8e Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 7 Jul 2026 02:28:54 -0500 Subject: [PATCH] =?UTF-8?q?fix(lean):=20adversarial=20review=20=E2=80=94?= =?UTF-8?q?=20correct=2011=20issues=20in=20BlockCoprimeDensity.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Critical fixes: - isSaturated doc: 1-1/p² → 1-1/p (contradicted its own theorem) - asymptoticBound/mertensConstant removed (formula was e^{-γ}/(n+2), not e^{-γ}/log(n+1) as claimed; unformalized analytic section) - densityBridgeNote replaced with honest claimBoundary scope note - C_finite doc clarified as finite truncation, not ζ(2) itself - Header explicitly lists WHAT IS FORMALIZED vs WHAT IS NOT Style: - Added @[simp] to 5 key theorems (AGENTS.md requirement) - Cleaned up p=0 vacuous edge case note - §4 asymptotic moved to honest prose-only section --- formal/SilverSight/BlockCoprimeDensity.lean | 155 +++++++++++++------- 1 file changed, 98 insertions(+), 57 deletions(-) diff --git a/formal/SilverSight/BlockCoprimeDensity.lean b/formal/SilverSight/BlockCoprimeDensity.lean index d35f0d29..c126564f 100644 --- a/formal/SilverSight/BlockCoprimeDensity.lean +++ b/formal/SilverSight/BlockCoprimeDensity.lean @@ -1,25 +1,37 @@ /- -BlockCoprimeDensity.lean — C(n) block-coprime density +BlockCoprimeDensity.lean — C(n) block-coprime density (finite Euler product) -Formalizes the Euler product for the natural density of pairs (r, M) ∈ ℕ² -satisfying the block-coprime condition gcd(r, M+j) = 1 for all j = 0..n. +Defines the finite Euler product that appears in the block-coprime density +problem. For (r, M) ∈ ℕ² satisfying gcd(r, M+j) = 1 for j = 0..n, the +natural density is expected to be: -C(n) = ζ(2) · ∏_{p prime} (1 − min(n+1, p) / p²) + C(n) = ζ(2) · ∏_{p prime} (1 − min(n+1, p) / p²) + +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 + • 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) + • Eval witnesses for small G + +WHAT IS NOT FORMALIZED (analytic number theory, beyond scope): + • The infinite product limit G → ∞ (convergence) + • The identification as a natural density of (r, M) pairs + • The Mertens asymptotic D(n) ∼ e^{-γ} / log(n+1) + • The connection to ζ(2) = π²/6 Structure: §1 Local factor and saturation partition - §2 Finite Euler product D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²) - §3 Boundary values at n=0, n=1 and the ζ(2) connection - §4 Asymptotic D(n) ∼ e^{-γ} / log(n+1) (Mertens) - §5 Bridge to SieveLemmas coprime-sieve reconstruction + §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 Conceptual connection to SieveLemmas (comment only) §6 Eval witnesses References: - Wessen Getachew, "C(n) — Block-Coprime Density" https://wessengetachew.github.io/smith/ - OEIS A013661 (ζ(2)), A065474 (∏(1-2/p²)), A065469 (C(1)) - - SilverSight.SieveLemmas (CRT coprime-sieve reconstruction) - - SilverSight.CRTSidon (CRT torus preserves Sidon property) -/ import Mathlib.Data.Nat.Prime.Defs @@ -40,13 +52,13 @@ namespace SilverSight.BlockCoprimeDensity /-- Local factor for prime p at block length n: 1 − min(n+1, p) / p² (in ℚ). - This is the contribution of prime p to the Euler product D(n). -/ + This is the contribution of prime p to the finite Euler product D_G(n). + Defined for any ℕ p, but meaningful only for primes p ≥ 2. -/ def localFactor (n p : ℕ) : ℚ := 1 - (min (n+1) p : ℚ) / ((p : ℚ) ^ 2) /-- A prime p is **saturated** at block length n when p ≤ n+1. - Saturated primes contribute their ζ(2) factor (1 − 1/p²) instead of - the active factor (1 − (n+1)/p²). -/ + Saturated primes contribute factor (1 − 1/p) instead of (1 − (n+1)/p²). -/ def isSaturated (n p : ℕ) : Prop := p ≤ n + 1 @@ -62,8 +74,8 @@ instance (n p : ℕ) : Decidable (isActive n p) := inferInstanceAs (Decidable (n + 1 < p)) /-- For a saturated prime (p ≤ n+1), the local factor simplifies to 1 − 1/p. - Since min(n+1, p) = p, the factor 1 − p/p² = 1 − 1/p. -/ -theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n p = 1 - (1 : ℚ) / (p : ℚ) := by + Since min(n+1, p) = p, we have 1 − p/p² = 1 − 1/p. -/ +@[simp] theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n p = 1 - (1 : ℚ) / (p : ℚ) := by unfold isSaturated at h unfold localFactor have hmin : (min (n+1) p : ℚ) = (p : ℚ) := by exact_mod_cast Nat.min_eq_right h @@ -72,8 +84,9 @@ 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². -/ -theorem localFactor_active (n p : ℕ) (h : isActive n p) : localFactor n p = 1 - ((n+1 : ℕ) : ℚ) / ((p : ℚ) ^ 2) := by +/-- For an active prime (p > n+1), the local factor is 1 − (n+1)/p². + Since min(n+1, p) = n+1, this is immediate from the definition. -/ +@[simp] theorem localFactor_active (n p : ℕ) (h : isActive n p) : localFactor n p = 1 - ((n+1 : ℕ) : ℚ) / ((p : ℚ) ^ 2) := by unfold isActive at h unfold localFactor have hmin : (min (n+1) p : ℚ) = ((n+1 : ℕ) : ℚ) := by @@ -89,42 +102,49 @@ def primesUpTo (G : ℕ) : Finset ℕ := (Finset.range (G+1)).filter Nat.Prime /-- D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²). - The finite Euler product truncation of the raw block-coprime density D(n). -/ + The finite Euler product truncation. This is rational for any finite G. + The infinite limit D(n) = lim_{G→∞} D_G(n) is the raw block-coprime + density (real, unformalized). -/ def D_finite (n G : ℕ) : ℚ := Finset.prod (primesUpTo G) (fun p => localFactor n p) -/-- C_G(n) = ζ(2) · D_G(n). - Uses the Euler product identity ζ(2) = ∏_p (1 − 1/p²)^{-1}: +/-- C_G(n) = (∏_{p ≤ G} (1−1/p²)⁻¹) · D_G(n). + This is the finite G-truncation of C(n). The product (∏ (1−1/p²)⁻¹) + is the G-truncated Euler factor of ζ(2); the full identity ζ(2) = + ∏_p (1−1/p²)⁻¹ is analytic and not proven here. - C_G(n) = (∏_{p ≤ G} (1-1/p²)^{-1}) · (∏_{p ≤ G} (1 − min(n+1, p)/p²)) - - For finite G this is rational; the infinite limit C(n) is real. -/ + For finite G this is rational; the infinite limit C(n) = ζ(2) · D(n) + is real and unformalized. -/ 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) connection +-- §3 Boundary values and the ζ(2) cancellation -- ═══════════════════════════════════════════════════════════════════════════ /-- For n=0, every prime is active (since the smallest prime is 2 > 1). The local factor at every prime is 1 − 1/p². -/ -lemma localFactor_zero (p : ℕ) (hp : p ≠ 0) : localFactor 0 p = 1 - (1 : ℚ) / ((p : ℚ) ^ 2) := by +@[simp] lemma localFactor_zero (p : ℕ) (hp : p ≠ 0) : localFactor 0 p = 1 - (1 : ℚ) / ((p : ℚ) ^ 2) := by unfold localFactor norm_num have hmin : (min 1 p : ℚ) = (1 : ℚ) := by exact_mod_cast Nat.min_eq_left (Nat.one_le_of_lt (Nat.pos_of_ne_zero hp)) rw [hmin]; simp -/-- D_finite(0, G) = ∏_{p ≤ G} (1 − 1/p²) — the Euler factor of ζ(2)^{-1}. -/ +/-- D_G(0) = ∏_{p ≤ G} (1 − 1/p²) — the G-truncated Euler factor of ζ(2)^{-1}. -/ lemma D_finite_zero_eq (G : ℕ) : D_finite 0 G = Finset.prod (primesUpTo G) (fun p => 1 - (1 : ℚ) / ((p : ℚ) ^ 2)) := by unfold D_finite refine Finset.prod_congr rfl fun p hp => ?_ have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2 simp [localFactor_zero p (Nat.Prime.ne_zero hp_prime)] -/-- C_G(0) = 1 exactly: at n=0, each factor (1 − 1/p²) cancels its own inverse - from the ζ(2) expansion. -/ -theorem C_finite_zero_eq_one (G : ℕ) : C_finite 0 G = 1 := by +/-- C_G(0) = 1 exactly for any G: at n=0, each factor (1 − 1/p²) + cancels its own inverse from the ζ(2) expansion, regardless of G. + + This is an algebraic identity that holds for every finite truncation. + The infinite limit C(0) = 1 also holds, but is a corollary of this + finite identity, not an independent analytic statement. -/ +@[simp] theorem C_finite_zero_eq_one (G : ℕ) : C_finite 0 G = 1 := by unfold C_finite have h : ∀ p ∈ primesUpTo G, (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹ * (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) = 1 := by intro p hp @@ -147,8 +167,8 @@ theorem C_finite_zero_eq_one (G : ℕ) : C_finite 0 G = 1 := by _ = 1 := by simp /-- For n=1, every prime p ≥ 2 has min(2, p) = 2. - The local factor is 1 − 2/p² for all primes. -/ -lemma localFactor_one_eq (p : ℕ) (hp : 2 ≤ p) : localFactor 1 p = 1 - (2 : ℚ) / ((p : ℚ) ^ 2) := by + The local factor simplifies to 1 − 2/p². -/ +@[simp] lemma localFactor_one_eq (p : ℕ) (hp : 2 ≤ p) : localFactor 1 p = 1 - (2 : ℚ) / ((p : ℚ) ^ 2) := by unfold localFactor norm_num have hmin : (min 2 p : ℚ) = (2 : ℚ) := by exact_mod_cast Nat.min_eq_left hp @@ -157,7 +177,8 @@ lemma localFactor_one_eq (p : ℕ) (hp : 2 ≤ p) : localFactor 1 p = 1 - (2 : theorem localFactor_one_prime (p : ℕ) (hp : Nat.Prime p) : localFactor 1 p = 1 - (2 : ℚ) / ((p : ℚ) ^ 2) := localFactor_one_eq p (Nat.Prime.two_le hp) -/-- D_finite(1, G) = ∏_{p ≤ G} (1 − 2/p²) — the Feller-Tornier Euler product. -/ +/-- D_G(1) = ∏_{p ≤ G} (1 − 2/p²) — the G-truncated Feller-Tornier Euler product. + The infinite limit ∏_p (1−2/p²) ≈ 0.322634 is OEIS A065474. -/ lemma D_finite_one_eq (G : ℕ) : D_finite 1 G = Finset.prod (primesUpTo G) (fun p => 1 - (2 : ℚ) / ((p : ℚ) ^ 2)) := by unfold D_finite refine Finset.prod_congr rfl fun p hp => ?_ @@ -165,54 +186,74 @@ lemma D_finite_one_eq (G : ℕ) : D_finite 1 G = Finset.prod (primesUpTo G) (fun simp [localFactor_one_prime p hp_prime] -- ═══════════════════════════════════════════════════════════════════════════ --- §4 Asymptotic (Mertens theorem) +-- §4 Notes on analytic extensions (unformalized) -- ═══════════════════════════════════════════════════════════════════════════ /- Mertens' third theorem: ∏_{p ≤ x} (1 − 1/p) ∼ e^{-γ} / log x. -This implies: D(n) = C(n)/ζ(2) ∼ e^{-γ} / log(n+1). +If the limit D(n) = lim_{G→∞} D_G(n) exists, then Mertens implies: -The analytic proof is beyond the scope of this finite formalization. -The constant is documented here as a reference. + D(n) ∼ e^{-γ} / log(n+1) as n → ∞ + +because the product over active primes (p > n+1) is asymptotically +∏_{p > n+1} (1 − (n+1)/p²) → 1, and the saturated product +∏_{p ≤ n+1} (1 − 1/p) ∼ e^{-γ} / log(n+1) by Mertens. + +ANALYTIC BOUNDARY: Both the convergence lim_{G→∞} D_G(n) and the +Mertens asymptotic are analytic number theory results. They are +documented here for reference only; this module does not prove them. -/ -/-- Approximate Mertens constant e^{-γ} ≈ 0.561459483566885 as a ℚ fraction. -/ -def mertensConstant : ℚ := 561459483566885 / 1000000000000000 - -/-- Approximate asymptotic D(n) ∼ e^{-γ} / log(n+1). - The log(n+1) denominator is represented as the rational (n+1) for - the reciprocal scaling; the exact analytic formula is real-valued. -/ -def asymptoticBound (n : ℕ) : ℚ := - mertensConstant / ((n+1 : ℕ).succ : ℚ) - -- ═══════════════════════════════════════════════════════════════════════════ --- §5 Bridge to SieveLemmas +-- §5 Claim boundary -- ═══════════════════════════════════════════════════════════════════════════ /-- -SilverSight.SieveLemmas.depth_token_coprime_intersect proves the existence -and uniqueness side: two coprime sieve observers reconstruct the coordinate -modulo ℓ₁·ℓ₂. This module provides the density side: C(n) gives the asymptotic -frequency of (r, M) pairs satisfying the block-coprime condition. +A string describing what this module proves and what it does not. -SieveLemmas: coprime observers reconstruct the coordinate (quality) -This module: C(n) gives the density of coprime-block pairs (quantity) +This module proves algebraic identities about finite Euler product +truncations only. The following are NOT proven: + + 1. The infinite product D(n) = lim_{G→∞} D_G(n) converges. + 2. The limit equals the natural density of coprime-block pairs. + 3. D(n) ∼ e^{-γ} / log(n+1) (Mertens). + 4. ζ(2) = π²/6. + +For a formal proof of these statements, an analytic number theory +framework beyond the scope of this finite formalization is required. -/ -def densityBridgeNote : String := - "C(n) is the density analogue of SieveLemmas.depth_token_coprime_intersect" +def claimBoundary : String := + "finite-euler-product-only; convergence-not-proven; density-identification-not-proven; mertens-not-proven" + +/-- +Conceptual note (not a theorem): +SilverSight.SieveLemmas.depth_token_coprime_intersect proves the +existence/uniqueness of coprime-sieve CRT reconstruction (the "quality" +side). The density C(n) — if the limit exists — would be the asymptotic +frequency of such coprime-block pairs (the "quantity" side). + +This module provides the Euler product expression. The formal +identification of C(n) as the density of (r, M) pairs in the 2D coprime +lattice satisfying the block-coprime condition is not proven here; it +requires the analytic convergence result noted in §4. +-/ +def bridgeNote : String := + "conceptual; see claimBoundary for scope" -- ═══════════════════════════════════════════════════════════════════════════ -- §6 Eval witnesses -- ═══════════════════════════════════════════════════════════════════════════ --- D_finite(0, 31) = ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.607927 (as ℚ) +-- D_G(0) at G=31 (first 11 primes): ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.61174 +-- The infinite limit is 6/π² ≈ 0.607927. #eval D_finite 0 31 --- D_finite(1, 31) = ∏_{p ≤ 31} (1 − 2/p²) ≈ 0.322634 (Feller-Tornier) +-- D_G(1) at G=31: ∏_{p ≤ 31} (1 − 2/p²) ≈ 0.32666 +-- The infinite limit (Feller-Tornier) ≈ 0.322634 (OEIS A065474). #eval D_finite 1 31 --- C_finite(0, 31) = 1 exactly (ζ(2) cancels) +-- C_G(0) = 1 exactly for any G. #eval C_finite 0 31 -- Saturated primes at n=2: p ≤ 3 → {2, 3}