allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): remove dead code hp_sq_ne_zero in C_finite_zero_eq_one

Browse source 
Leftover from a previous proof iteration. The hx block proves nonzeroness via positivity arguments alone.
This commit is contained in:
allaun 2026-07-07 09:19:13 -05:00
parent 44fcafe0de
commit c3a5e6b60b
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
formal/SilverSight/BlockCoprimeDensity.lean
View file

@ -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