The lower prime-root logarithmic bound for irreducible polynomials

theorem NairTenenbaum.exists_irreducible_rootPrimePowerSum_lower_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (C : ℝ) (b : ℝ), 1 < b ∧ ∀ (σ : ℝ), 1 < σ → σ < b → -Real.log (σ - 1) - C ≤ rootPrimePowerSum Q σ