Producer for the low-conductor Standard-BV source

This module reduces the low source to two genuinely one-dimensional inputs: the already isolated modulus-one PNT/partial-summation contract, and a pointwise primitive nonprincipal ψ(N,χ) Siegel--Walfisz estimate. All finite character multiplicities, conductor fibres and logarithmic losses are paid here.

def AnalyticNumberTheory.LargeSieve.NonprincipalPrimitivePsiSiegelWalfiszSource : Prop

The exact remaining low-conductor analytic theorem. It is pointwise in a primitive nonprincipal character and contains neither an AP average nor a BV conclusion. (For d ≥ 2, primitivity in fact forces nonprincipality; the explicit hypothesis records the intended mathematical lane.)

Equations

• AnalyticNumberTheory.LargeSieve.NonprincipalPrimitivePsiSiegelWalfiszSource = ∀ (C D : ℕ), ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∀ d ∈ Finset.Icc 2 (AnalyticNumberTheory.LargeSieve.logConductorThreshold N C), ∀ (ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d), ↑ψ ≠ 1 → AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude AnalyticNumberTheory.LargeSieve.vonMangoldtIntegerCoeff N d ψ ≤ K * ↑N / Real.log ↑N ^ D

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacter_ne_one_of_two_le {d : ℕ} (hd : 2 ≤ d) (ψ : PrimitiveCharacter d) : ↑ψ ≠ 1

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixSiegelWalfiszSource_of_nonprincipal (h : NonprincipalPrimitivePsiSiegelWalfiszSource) : PrimitivePrefixSiegelWalfiszSource

The explicitly nonprincipal formulation is equivalent to the older all-primitive pointwise formulation, since conductors in the low set start at 2.

theorem AnalyticNumberTheory.LargeSieve.lowConductorArithmeticMass_le_explicit (N Q C : ℕ) : lowConductorArithmeticMass N Q C ≤ ↑(logConductorThreshold N C) * conductorHarmonicFactor Q ^ 2

The complete finite arithmetic mass in the low conductor lane is at most R H(Q)^2, where R = floor(log(N)^C).

theorem AnalyticNumberTheory.LargeSieve.principalGlobal_add_chebyshevToLi_le_qOne (N Q : ℕ) : discreteAbelAmplifierPrefixMax N * principalGlobalPhysical N Q + chebyshevToLiPhysical N Q ≤ conductorHarmonicFactor Q ^ 2 * globalPartialSummationSource N

The two modulus-one terms, after summing 1/φ(q), cost only the proved finite reciprocal-totient mass.

theorem AnalyticNumberTheory.LargeSieve.standardBVLowSiegelWalfiszSource_of_nonprincipalPrimitivePsi (hSW : NonprincipalPrimitivePsiSiegelWalfiszSource) (hPNT : GlobalChebyshevToLiPrincipalPNTSourceContract) : StandardBVLowSiegelWalfiszSource

Producer for the former full low-source black box. Besides the existing one-dimensional modulus-one PNT contract, the only analytic premise is the pointwise nonprincipal primitive ψ(N,χ) Siegel--Walfisz theorem above.