fix(lean): adversarial review — correct 11 issues in BlockCoprimeDensity.lean

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

@@ -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) ∈ ℕ²
+Defines the finite Euler product that appears in the block-coprime density
-satisfying the block-coprime condition gcd(r, M+j) = 1 for all j = 0..n.
+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²)
 
+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²)
+  §2  Finite Euler product D_G(n)
-  §3  Boundary values at n=0, n=1 and the ζ(2) connection
+  §3  Boundary values at n=0, n=1 and the ζ(2) cancellation
-  §4  Asymptotic D(n) ∼ e^{-γ} / log(n+1) (Mertens)
+  §4  Notes on analytic extensions (unformalized)
-  §5  Bridge to SieveLemmas coprime-sieve reconstruction
+  §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
+    Saturated primes contribute factor (1 − 1/p) instead of (1 − (n+1)/p²). -/
-    the active factor (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. -/
+    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
+@[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². -/
+/-- 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
+    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).
+/-- C_G(n) = (∏_{p ≤ G} (1−1/p²)⁻¹) · D_G(n).
-    Uses the Euler product identity ζ(2) = ∏_p (1 − 1/p²)^{-1}:
+    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) = ζ(2) · D(n)
-
+    is real and unformalized. -/
-    For finite G this is rational; the infinite limit C(n) is real. -/
 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
+/-- C_G(0) = 1 exactly for any G: at n=0, each factor (1 − 1/p²)
-    from the ζ(2) expansion. -/
+    cancels its own inverse from the ζ(2) expansion, regardless of G.
-theorem C_finite_zero_eq_one (G : ℕ) : C_finite 0 G = 1 := by
+
+    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. -/
+    The local factor simplifies to 1 − 2/p². -/
-lemma localFactor_one_eq (p : ℕ) (hp : 2 ≤ p) : localFactor 1 p = 1 - (2 : ℚ) / ((p : ℚ) ^ 2) := by
+@[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.
+  D(n) ∼ e^{-γ} / log(n+1)   as n → ∞
-The constant is documented here as a reference.
+
+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
+A string describing what this module proves and what it does not.
-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.
 
-SieveLemmas: coprime observers reconstruct the coordinate (quality)
+This module proves algebraic identities about finite Euler product
-This module:  C(n) gives the density of coprime-block pairs (quantity)
+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 :=
+def claimBoundary : String :=
-  "C(n) is the density analogue of SieveLemmas.depth_token_coprime_intersect"
+  "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}