From c3a5e6b60b1579b552c9478b673f6fe9eb0c0789 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 7 Jul 2026 09:19:13 -0500
Subject: [PATCH] fix(lean): remove dead code hp_sq_ne_zero in
 C_finite_zero_eq_one

Leftover from a previous proof iteration. The hx block proves nonzeroness via positivity arguments alone.
---
 formal/SilverSight/BlockCoprimeDensity.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/formal/SilverSight/BlockCoprimeDensity.lean b/formal/SilverSight/BlockCoprimeDensity.lean
index 768d37e1..3d53e8ba 100644
--- a/formal/SilverSight/BlockCoprimeDensity.lean
+++ b/formal/SilverSight/BlockCoprimeDensity.lean
@@ -227,7 +227,6 @@ 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_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