diff --git a/formal/SilverSight/BlockCoprimeDensity.lean b/formal/SilverSight/BlockCoprimeDensity.lean
index c126564f..7a67db87 100644
--- a/formal/SilverSight/BlockCoprimeDensity.lean
+++ b/formal/SilverSight/BlockCoprimeDensity.lean
@@ -3,7 +3,7 @@ BlockCoprimeDensity.lean — C(n) block-coprime density (finite Euler product)
 
 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:
+natural density is (analytically) known to be:
 
   C(n) = ζ(2) · ∏_{p prime} (1 − min(n+1, p) / p²)
 
@@ -12,6 +12,7 @@ WHAT IS FORMALIZED:
   • 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)
+  • Complementarity of saturated/active primes
   • Eval witnesses for small G
 
 WHAT IS NOT FORMALIZED (analytic number theory, beyond scope):
@@ -25,8 +26,7 @@ Structure:
   §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
+  §5  Eval witnesses
 
 References:
   - Wessen Getachew, "C(n) — Block-Coprime Density"
@@ -73,9 +73,20 @@ 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. -/
+theorem isSaturated_or_isActive (n p : ℕ) : isSaturated n p ∨ isActive n p := by
+  by_cases h : p ≤ n + 1
+  · left; exact h
+  · right; exact Nat.lt_of_not_ge h
+
+/-- Saturated and active are complementary. -/
+theorem isSaturated_iff_not_isActive (n p : ℕ) : isSaturated n p ↔ ¬isActive n p := by
+  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.
     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
+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
@@ -86,7 +97,7 @@ instance (n p : ℕ) : Decidable (isActive n p) :=
 
 /-- 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
+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
@@ -97,7 +108,8 @@ instance (n p : ℕ) : Decidable (isActive n p) :=
 -- §2  Finite Euler product
 -- ═══════════════════════════════════════════════════════════════════════════
 
-/-- The set of primes ≤ G as a Finset ℕ. -/
+/-- The set of primes ≤ G as a Finset ℕ.
+    When G = 0 or G = 1 the result is empty (no primes ≤ 1). -/
 def primesUpTo (G : ℕ) : Finset ℕ :=
   (Finset.range (G+1)).filter Nat.Prime
 
@@ -124,7 +136,7 @@ def C_finite (n G : ℕ) : ℚ :=
 
 /-- For n=0, every prime is active (since the smallest prime is 2 > 1).
     The local factor at every prime is 1 − 1/p². -/
-@[simp] lemma localFactor_zero (p : ℕ) (hp : p ≠ 0) : localFactor 0 p = 1 - (1 : ℚ) / ((p : ℚ) ^ 2) := by
+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 : ℚ) :=
@@ -168,12 +180,14 @@ lemma D_finite_zero_eq (G : ℕ) : D_finite 0 G = Finset.prod (primesUpTo G) (fu
 
 /-- For n=1, every prime p ≥ 2 has min(2, p) = 2.
     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
+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
   rw [hmin]
 
+/-- Dedicated version of `localFactor_one_eq` for primes.
+    The hypothesis `Nat.Prime p` supplies `2 ≤ p` via `Nat.Prime.two_le`. -/
 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)
 
@@ -205,44 +219,17 @@ Mertens asymptotic are analytic number theory results.  They are
 documented here for reference only; this module does not prove them.
 -/
 
--- ═══════════════════════════════════════════════════════════════════════════
--- §5  Claim boundary
--- ═══════════════════════════════════════════════════════════════════════════
-
-/--
-A string describing what this module proves and what it does not.
-
-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.
+/-
+Conceptual note: 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 as a density is not proven here.
 -/
-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
+-- §5  Eval witnesses
 -- ═══════════════════════════════════════════════════════════════════════════
 
 -- D_G(0) at G=31 (first 11 primes): ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.61174