Tatuzawa exceptional uniqueness and the Landau--Siegel lower bound

This module formalizes the logical core of the Tatuzawa route. For a fixed power η, an effective lower bound and a conductor threshold define the set of primitive nonprincipal quadratic characters where that bound fails. If this set has at most one member, strict positivity of the one possible exceptional L(1, χ) absorbs it into an ineffective constant. The already established finite-conductor bridge then supplies the raw Landau--Siegel lower bound.

The final source below is deliberately not exceptional uniqueness itself. It is the quantitative two-character value-product separation which implies uniqueness. Proving that separation by Euler-product positivity / zero repulsion remains the analytic frontier; no such theorem is assumed to have been completed here.

structure AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum : Type

A primitive nonprincipal quadratic Dirichlet character, with its conductor stored in the same object so exceptional characters at different conductors can be compared.

• modulus : ℕ
• modulus_ne : self.modulus ≠ 0
• character : DirichletCharacter ℂ self.modulus
• isPrimitive : self.character.IsPrimitive
• square_eq_one : self.character ^ 2 = 1
• ne_one : self.character ≠ 1

noncomputable def AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.value (x : PrimitiveQuadraticDatum) : ℝ

The real value L(1, χ) attached to a quadratic datum.

Equations

• x.value = (DirichletCharacter.LFunction x.character 1).re

noncomputable def AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale (η : ℝ) (x : PrimitiveQuadraticDatum) : ℝ

The conductor power occurring in a Siegel lower bound.

Equations

• AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale η x = ↑x.modulus ^ (-η)

theorem AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.modulus_pos (x : PrimitiveQuadraticDatum) : 0 < x.modulus

theorem AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale_pos (η : ℝ) (x : PrimitiveQuadraticDatum) : 0 < powerScale η x

theorem AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.value_pos (x : PrimitiveQuadraticDatum) : 0 < x.value

def AnalyticNumberTheory.LargeSieve.tatuzawaEffectiveFailureSet (η c : ℝ) (Q : ℕ) : Set PrimitiveQuadraticDatum

The literal set of large-conductor characters where the proposed effective c q⁻η lower bound fails.

Equations

• AnalyticNumberTheory.LargeSieve.tatuzawaEffectiveFailureSet η c Q = {x : AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum | Q ≤ x.modulus ∧ x.value < c * AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale η x}

def AnalyticNumberTheory.LargeSieve.AtMostOneEventualEffectiveException : Prop

Quantifier-level Tatuzawa uniqueness: for every positive exponent there is an effective threshold and effective positive coefficient for which at most one large-conductor primitive quadratic character fails the lower bound.

Equations

• AnalyticNumberTheory.LargeSieve.AtMostOneEventualEffectiveException = ∀ (η : ℝ), 0 < η → ∃ (Q : ℕ) (c : ℝ), 0 < c ∧ (AnalyticNumberTheory.LargeSieve.tatuzawaEffectiveFailureSet η c Q).Subsingleton

def AnalyticNumberTheory.LargeSieve.EventualTatuzawaValueProductSeparation : Prop

A quantitative two-character separation interface. Its lower side is the product of the two proposed effective thresholds, so two distinct failures would contradict it immediately. This is the analytic, value-product-shaped frontier intended for an Euler-product positivity or Deuring--Heilbronn proof.

Equations

• AnalyticNumberTheory.LargeSieve.EventualTatuzawaValueProductSeparation = ∀ (η : ℝ), 0 < η → ∃ (Q : ℕ) (c : ℝ), 0 < c ∧ ∀ (x y : AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum), Q ≤ x.modulus → Q ≤ y.modulus → x ≠ y → c * AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale η x * (c * AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale η y) ≤ x.value * y.value

def AnalyticNumberTheory.LargeSieve.EventualTatuzawaValueProductPowerLowerBound : Prop

Source-faithful value-product power lower bound. Unlike the failure-set statement, this predicate does not mention exceptions or uniqueness: it asks for a direct positive lower bound for the product of two distinct quadratic L(1) values at the product of their two conductor-power scales.

Equations

• AnalyticNumberTheory.LargeSieve.EventualTatuzawaValueProductPowerLowerBound = ∀ (η : ℝ), 0 < η → ∃ (Q : ℕ) (κ : ℝ), 0 < κ ∧ ∀ (x y : AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum), Q ≤ x.modulus → Q ≤ y.modulus → x ≠ y → κ * AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale η x * AnalyticNumberTheory.LargeSieve.PrimitiveQuadraticDatum.powerScale η y ≤ x.value * y.value

theorem AnalyticNumberTheory.LargeSieve.eventualTatuzawaValueProductSeparation_of_powerLowerBound (hprod : EventualTatuzawaValueProductPowerLowerBound) : EventualTatuzawaValueProductSeparation

A direct product lower bound supplies the threshold-form separation by choosing the effective one-character coefficient sqrt κ.

theorem AnalyticNumberTheory.LargeSieve.atMostOneEventualEffectiveException_of_valueProductSeparation (hsep : EventualTatuzawaValueProductSeparation) : AtMostOneEventualEffectiveException

The quantitative value-product separation makes the effective failure set subsingleton. Positivity of both actual values is used before multiplying the two strict failure inequalities.

theorem AnalyticNumberTheory.LargeSieve.rawLandauSiegelLowerBound_of_atMostOneEventualEffectiveException (hunique : AtMostOneEventualEffectiveException) : RawLandauSiegelLowerBound

At most one eventual effective exception implies the raw Landau--Siegel lower bound. If an exception exists, its strictly positive value defines one additional coefficient; otherwise the effective coefficient already works. The possible exception is absorbed before the finite-conductor bridge is invoked.

theorem AnalyticNumberTheory.LargeSieve.rawLandauSiegelLowerBound_of_eventualTatuzawaValueProductSeparation (hsep : EventualTatuzawaValueProductSeparation) : RawLandauSiegelLowerBound

The Tatuzawa route to the raw Landau--Siegel lower bound with a genuinely analytic final source: quantitative separation of the values of any two distinct primitive quadratic characters.

theorem AnalyticNumberTheory.LargeSieve.rawLandauSiegelLowerBound_of_eventualTatuzawaValueProductPowerLowerBound (hprod : EventualTatuzawaValueProductPowerLowerBound) : RawLandauSiegelLowerBound

Final Tatuzawa reduction with no uniqueness-shaped source: the remaining input is the direct two-character value-product power lower bound.