RationalZeroGap.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed rational-field zero gap

The final contradiction in odd-degree zero descent only needs a fixed neighborhood of one where the rational completed zeta function is nonzero. Continuity and its computed value at one supply that gap.

theorem OAI.DukePrimeDegree.rational_completedXi_nonzero_near_one line 22

Source documentation

The completed zeta function of the rational field is nonzero on a fixed real interval ending at one.

theorem rational_completedXi_nonzero_near_one
    (σ : OrderedEmbeddings 1 ℚ) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ β ∈ Icc (1 - δ) 1,
      completedThetaXi σ (by simp : Module.finrank ℚ ℚ = 1) β ≠ 0 := by
…

theorem OAI.DukePrimeDegree.rational_completedXi_nonzero_scaled line 40

Source documentation

A fixed rational-field zero gap contains every sufficiently narrow discriminant-scaled interval used in Stark descent.

theorem rational_completedXi_nonzero_scaled
    (σ : OrderedEmbeddings 1 ℚ) :
    ∃ a : ℝ, 0 < a ∧ ∀ L : ℝ, 4 ≤ L →
      ∀ β ∈ Icc (1 - a / L) 1,
        completedThetaXi σ (by simp : Module.finrank ℚ ℚ = 1) β ≠ 0 := by
…