PublishedStark.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The published analytic input for prime-degree packets

The conditional development uses Stark, Some effective cases of the Brauer–Siegel theorem, Invent. Math. 23 (1974), 135–152, Lemmas 3 and 8 and equation (9). StarkInput records only the consequence needed here: for fields with no quadratic subfield, the nontrivial zeros are separated from 1 on the scale 1 / log D, and their real Hadamard sum converges. The zeros are indexed with multiplicity. The archimedean term and Euler-product derivative estimate then give the uniform residue comparison.

def OAI.DukePrimeDegree.StarkInput line 29
Source documentation
The zero-free specialization of Stark's Lemmas 3 and 8, together with his real Hadamard identity (9). Only fields of the fixed degree and without quadratic subfields are used.
```
def StarkInput (n : ℕ) : Prop :=
…
```
theorem OAI.DukePrimeDegree.uniformZetaScaleBound_of_stark line 55
Source documentation
The manuscript's new uniform residue reduction, conditional on the precisely stated published zero input above.
```
theorem uniformZetaScaleBound_of_stark {n : ℕ} (hn : n.Prime) (hn3 : 3 ≤ n)
    (H : StarkInput.{u} n) : UniformZetaScaleBound.{u} n := by
…
```