Narrow sufficient assembly for Standard Bombieri--Vinogradov

The finite lambda/conductor connector and the elementary payload are consumed internally. The publication-facing theorem retains only a low-conductor Siegel--Walfisz/PNT source and the exact high-conductor Vaughan hybrid source. Neither source contains a Standard-BV conclusion.

def AnalyticNumberTheory.LargeSieve.StandardBVLowSiegelWalfiszSource : Prop

The genuine low-conductor analytic source after finite character and conductor bookkeeping. It consists only of the low primitive-conductor lane and the modulus-one PNT/partial-summation lane.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVLowSiegelWalfiszSource = ∀ (A C B : ℕ), ∃ (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; 2 * AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.lowConductorPhysical N Q C + AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.principalGlobalPhysical N Q + AnalyticNumberTheory.LargeSieve.chebyshevToLiPhysical N Q ≤ K * ↑N / Real.log ↑N ^ A

def AnalyticNumberTheory.LargeSieve.StandardBVHighTypeITypeIIHybridSource : Prop

The genuine high-conductor analytic source. Its left side is exactly the Vaughan Type-I/II/small hybrid on the high conductor Finset, multiplied only by the proved conductor transport and Abel factors. The small lane is elementary and may be bounded independently by highConductorVaughanSmallMean_le_explicit; no Standard-BV assertion occurs here.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVHighTypeITypeIIHybridSource = ∀ (A C B : ℕ), ∃ (u : ℕ) (v : ℕ) (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; 4 * AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q ^ 2 * (AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIMean N Q C u v + AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean N Q C u v + AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean N Q C v) ≤ K * ↑N / Real.log ↑N ^ A

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_vaughan_le (N : ℕ) (S : Finset ℕ) (u v : ℕ) : apNormalizedPrimitiveMeanOn vonMangoldtIntegerCoeff N S ≤ 2 * (apNormalizedPrimitiveMeanOn (vaughanTypeICoeff vaughanUnitIntegerCoeff u v) N S + apNormalizedPrimitiveMeanOn (vaughanTypeIICoeff vaughanUnitIntegerCoeff u v) N S + apNormalizedPrimitiveMeanOn (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N S)

Vaughan's exact prefix decomposition restricted to an arbitrary conductor Finset.

theorem AnalyticNumberTheory.LargeSieve.directConductorMeanOn_le_apNormalizedPrimitiveMeanOn (a : ℤ → ℂ) (N Q : ℕ) (S : Finset ℕ) : directConductorMeanOn a N Q S ≤ conductorHarmonicFactor Q ^ 2 * apNormalizedPrimitiveMeanOn a N S

Direct conductor weight on any subset is controlled by the AP-normalized primitive mean on that same subset.

theorem AnalyticNumberTheory.LargeSieve.highConductorPhysical_le_vaughanHybrid (N Q C u v : ℕ) : highConductorPhysical N Q C ≤ 2 * conductorHarmonicFactor Q ^ 2 * (highConductorVaughanTypeIMean N Q C u v + highConductorVaughanTypeIIMean N Q C u v + highConductorVaughanSmallMean N Q C v)

The exact high physical conductor lane is controlled by the exact Vaughan hybrid appearing in StandardBVHighTypeITypeIIHybridSource.

theorem AnalyticNumberTheory.LargeSieve.standardBV_sufficient_at_closed (A B C N Q u v : ℕ) (KL KH : ℝ) (hN : 2 ≤ N) (hQ : Q = MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B) (hlow : 2 * discreteAbelAmplifierPrefixMax N * lowConductorPhysical N Q C + discreteAbelAmplifierPrefixMax N * principalGlobalPhysical N Q + chebyshevToLiPhysical N Q ≤ KL * ↑N / Real.log ↑N ^ A) (hhigh : 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2 * (highConductorVaughanTypeIMean N Q C u v + highConductorVaughanTypeIIMean N Q C u v + highConductorVaughanSmallMean N Q C v) ≤ KH * ↑N / Real.log ↑N ^ A) (hpayload : StandardBVPayload N Q ≤ 180 * ↑N / Real.log ↑N ^ A) : ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B), MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ (KL + KH + 180) * ↑N / Real.log ↑N ^ A

Closed finite sufficient assembly. The connector is a theorem, and the only third budget is the already-proved StandardBVPayload.

theorem AnalyticNumberTheory.LargeSieve.standardBV_of_lowSW_highTypeITypeII (hlow : StandardBVLowSiegelWalfiszSource) (hhigh : StandardBVHighTypeITypeIIHybridSource) (A : ℕ) : ∃ (B : ℕ) (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B), MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ K * ↑N / Real.log ↑N ^ A

Narrow Standard-BV endpoint. Its only premises are the genuine low SW/PNT source and the genuine high Vaughan hybrid source; all finite connectors and all elementary payment premises have disappeared.