Exact polynomial form of the unconditional twisted exponential factor
Provedgpy_twistedExp_eq_pownumber-theory
The exponential factor exp (2 (k+1)^2 (log Q + 2)) in the unconditional twisted absolute bound equals exp (4 (k+1)^2) * Q^(2 (k+1)^2): it is polynomial in Q, not polylogarithmic. This is an unconditional identity, and it is precisely why the unconditional bound cannot by itself show any sum is o(1) relative to a polylog-scale main term. No defect smallness is claimed.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_twistedExp_eq_pow {k : ℕ} {Q : ℕ} (hQ : 0 < Q) :
Real.exp (2 * ((k : ℝ) + 1) ^ 2 * (Real.log (Q : ℝ) + 2))
= Real.exp (4 * ((k : ℝ) + 1) ^ 2) * (Q : ℝ) ^ (2 * (k + 1) ^ 2) := by sorrySource
GPY defect smallness (GPYDefectSmall.lean), restated into Mathlib-only terms