Abstract threshold step: main-term crossing forces two primes in one translate

import Mathlib
open Classical

theorem gpy_exists_two_primes_of_mainTerm_crossing {k : ℕ} (h : Fin k → ℕ) (R : ℕ) (lam : (Fin k → ℕ) → ℝ) {x y : ℕ} (A B E1 E2 : ℝ) (hS1 : abs ((∑ n ∈ Finset.Ioc x y, ((∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), if (∀ i, d i ∣ n + h i) then lam d else 0) ^ 2)) - A) ≤ E1) (hS2 : abs ((∑ n ∈ Finset.Ioc x y, (∑ i, (if Nat.Prime (n + h i) then (1 : ℝ) else 0)) * ((∑ d ∈ ((Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 R)).filter (fun d => ∏ i, d i ≤ R)), if (∀ i, d i ∣ n + h i) then lam d else 0) ^ 2)) - B) ≤ E2) (hcross : A + E1 < B - E2) : ∃ n ∈ Finset.Ioc x y, ∃ i j, i ≠ j ∧ Nat.Prime (n + h i) ∧ Nat.Prime (n + h j) := by sorry