Nonvanishing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nonvanishing of Dirichlet L-functions to the right of seven eighths

The main result excludes zeros of Dirichlet L-functions in the half-plane 7 / 8 < re s, apart from the principal character's pole at s = 1. The corresponding nonvanishing statement for the Riemann zeta function follows.

theorem OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re line 19
Source documentation
Dirichlet L-functions do not vanish to the right of 7 / 8, away from the principal character's pole at 1.
Distinct definitions of this name: ComparatorChallenges/DirichletSevenEighths.lean:8 (same statement text; different proof or body). Qualify references as OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re@path.
Implications (curated claims about what follows, not dependencies: what these are)
- strengthens OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap kernel-checked (recorded) contract
```
theorem LFunction_ne_zero_of_seven_eighths_lt_re
    {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ}
    (hs : (7 / 8 : ℝ) < s.re) (hpole : ¬ (χ = 1 ∧ s = 1)) :
    _root_.DirichletCharacter.LFunction χ s ≠ 0 :=
…
```
theorem OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re line 29
Source documentation
The Riemann zeta function does not vanish to the right of 7 / 8.
Distinct definitions of this name: ComparatorChallenges/QuasiRiemannHypothesis.lean:5 (same statement text; different proof or body). Qualify references as OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re@path.
```
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 :=
…
```