Feasibility boundary for the Standard-BV high-conductor Vaughan source

The unconditional Type-I/II physical inputs are full-conductor estimates with an N + Q^2 sqrt N (and, for Type II, Q N / sqrt (u+1)) scale. Restricting the nonnegative conductor sum to d > log(N)^C preserves that same upper bound; it does not manufacture an inverse-logarithmic saving.

This file records (1) the scalar obstruction, (2) a finite delta-mass witness showing that deletion of low conductors alone has no 1/R gain, and (3) the narrow exact high-conductor contract, with moving Vaughan cutoffs, which the existing Standard-BV consumer really needs. No inhabitant of that analytic contract is asserted here.

theorem AnalyticNumberTheory.LargeSieve.positive_N_lane_not_paid_by_modulus_cutoff (N L K logPow _Q _B : ℝ) (hN : 0 < N) (_hL : 0 < L) (hlogPow : 0 < logPow) (hgap : K < L * logPow) : K * N / logPow < L * N

A positive L*N lane cannot fit inside K*N/logPow once K < L*logPow. The modulus data Q,B are deliberately present but absent from the hypotheses and conclusion: changing them cannot alter this lane.

theorem AnalyticNumberTheory.LargeSieve.physical_majorant_with_positive_N_lane_obstructed (N L K logPow Q B physical : ℝ) (hN : 0 < N) (hL : 0 < L) (hlogPow : 0 < logPow) (hgap : K < L * logPow) (hNlane : L * N ≤ physical) (hbudget : physical ≤ K * N / logPow) : False

Formal contradiction certificate for any physical majorant which retains a positive multiple of N but is advertised at inverse-logarithmic scale.

def AnalyticNumberTheory.LargeSieve.topConductorDelta (Q d : ℕ) : ℝ

A delta mass at the top conductor. It is the generic obstruction to extracting an R^{-1} gain merely by deleting d ≤ R.

Equations

• AnalyticNumberTheory.LargeSieve.topConductorDelta Q d = if d = Q then 1 else 0

theorem AnalyticNumberTheory.LargeSieve.topConductorDelta_nonneg (Q d : ℕ) : 0 ≤ topConductorDelta Q d

theorem AnalyticNumberTheory.LargeSieve.sum_topConductorDelta_high (Q R : ℕ) (hRQ : R < Q) : ∑ d ∈ Finset.Icc (R + 1) Q, topConductorDelta Q d = 1

If the high interval is nonempty, a nonnegative lane can be concentrated entirely at its top conductor, so its high-conductor mass is still exactly one.

theorem AnalyticNumberTheory.LargeSieve.no_inverse_cutoff_gain_from_restriction (Q R : ℕ) (hR : 1 < R) (hRQ : R < Q) : ¬∑ d ∈ Finset.Icc (R + 1) Q, topConductorDelta Q d ≤ 1 / ↑R

Consequently no universal high mass ≤ full mass / R inequality follows from positivity and the cutoff alone when R>1.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIMean_le_full (N Q C u v : ℕ) : highConductorVaughanTypeIMean N Q C u v ≤ apNormalizedVaughanTypeIMean N Q u v

Restricting Type I to high conductors uses only positivity and therefore retains the full-conductor right-hand side.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean_le_full (N Q C u v : ℕ) : highConductorVaughanTypeIIMean N Q C u v ≤ apNormalizedVaughanTypeIIMean N Q u v

The identical monotonicity restriction for Type II. This is the strongest automatic bridge from the current full-range physical producer; it gives no factor depending on the lower conductor cutoff.

def AnalyticNumberTheory.LargeSieve.StandardBVHighTypeITypeIIHybridMovingSource : Prop

Narrowest honest missing analytic contract. It asks only for the exact post-conductor-transport high Vaughan hybrid, not for a BV conclusion. The Vaughan cutoffs may vary with N; fixing them before N would leave the Q*N/sqrt(u+1) lane quantitatively unusable.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVHighTypeITypeIIHybridMovingSource = ∀ (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 N) (v N) + AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean N Q C (u N) (v N) + AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean N Q C (v N)) ≤ K * ↑N / Real.log ↑N ^ A

def AnalyticNumberTheory.LargeSieve.StandardBVHighTypeITypeIIHybridChosenSource : Prop

Source-faithful chosen-cutoff high-conductor interface. For each requested A, the source first chooses the Pan exponent B and separator exponent C; only then does it choose moving Vaughan cutoffs and the implicit constant. Unlike the legacy all-B,C interface, this does not demand estimates for irrelevant choices such as B = 0.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVHighTypeITypeIIHybridChosenSource = ∀ (A : ℕ), ∃ (B : ℕ) (C : ℕ), A + 3 ≤ 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 N) (v N) + AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIMean N Q C (u N) (v N) + AnalyticNumberTheory.LargeSieve.highConductorVaughanSmallMean N Q C (v N)) ≤ K * ↑N / Real.log ↑N ^ A

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_legacy (hhigh : StandardBVHighTypeITypeIIHybridMovingSource) : StandardBVHighTypeITypeIIHybridChosenSource

Compatibility adapter from the legacy uniformly quantified interface.

theorem AnalyticNumberTheory.LargeSieve.standardBV_of_lowSW_highTypeITypeII_chosen (hlow : StandardBVLowSiegelWalfiszSource) (hhigh : StandardBVHighTypeITypeIIHybridChosenSource) (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

Canonical sufficient assembly. It consumes the chosen-cutoff high source and specializes the low source only after B,C have been selected.

theorem AnalyticNumberTheory.LargeSieve.standardBV_of_lowSW_highTypeITypeII_moving (hlow : StandardBVLowSiegelWalfiszSource) (hhigh : StandardBVHighTypeITypeIIHybridMovingSource) (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

Real consumer for the moving-cutoff high-conductor contract. All finite connectors and elementary lanes remain internal, exactly as in the fixed-cutoff consumer; only the pointwise Vaughan cutoffs are instantiated after N.