Prime-indicator sum bound for a translate with at most one prime coordinate
Provedgpy_sum_primeInd_le_onenumber-theory
If at most one coordinate of a translate is prime, the sum of prime indicators over the tuple is at most 1. Pure Mathlib statement: the prime indicator is written out as an if-then-else.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_sum_primeInd_le_one {k : ℕ} (h : Fin k → ℕ) (n : ℕ) (hat : ∀ i j : Fin k, i ≠ j → ¬ Nat.Prime (n + h i) ∨ ¬ Nat.Prime (n + h j)) : (∑ i, (if Nat.Prime (n + h i) then (1 : ℝ) else 0)) ≤ 1 := by sorrySource
GPY ratio analysis: threshold, main-term approximations, and BV level cap