ModFiveLowZeros.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact-height completion of the fixed-modulus zero-free strip. The compactness step is simultaneous for the finite family of characters, using nonvanishing on the line Re s = 1.

lemma OAI.TwoPointCorrelations.modFive_compact_height_zero_free line 16
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLowZeros.lean:16 (same declaration text).
theorem OAI.TwoPointCorrelations.modFive_nonprincipal_zero_free line 59
Source documentation
The full fixed-modulus logarithmic zero-free region, including bounded heights. Its constant is uniform across the three nonprincipal characters.
Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLowZeros.lean:59 (same declaration text).
```
theorem modFive_nonprincipal_zero_free : ∃ c : ℝ, 0 < c ∧
    ∀ (χ : DirichletCharacter ℂ 5), χ ≠ 1 → ∀ (t β : ℝ),
      1 - c / Real.log (|t| + 2) ≤ β →
      DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) ≠ 0 := by
…
```