noncomputable def AnalyticNumberTheory.LargeSieve.standardBVAdaptiveSmallCutoff (Q N : ℕ) : ℕ

Faithful Vaughan small cutoff for a fixed global modulus cutoff Q. The explicit zero branch records the safe interpretation at Q = 0.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVAdaptiveSmallCutoff Q N = if Q = 0 then 0 else min (Q ^ 2) (min (AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff N) (N / Q ^ 2))

@[simp]

theorem AnalyticNumberTheory.LargeSieve.standardBVAdaptiveSmallCutoff_zero (N : ℕ) : standardBVAdaptiveSmallCutoff 0 N = 0

theorem AnalyticNumberTheory.LargeSieve.standardBVAdaptiveSmallCutoff_le_balanced (Q N : ℕ) : standardBVAdaptiveSmallCutoff Q N ≤ standardBVBalancedSmallCutoff N

theorem AnalyticNumberTheory.LargeSieve.standardBVAdaptiveSmallCutoff_le (Q N : ℕ) : standardBVAdaptiveSmallCutoff Q N ≤ N

theorem AnalyticNumberTheory.LargeSieve.standardBVSmall_squareLedger_le (N Q C v : ℕ) (hQ : 0 < Q) : primitivePrefixSquareLedgerOn (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N (highConductorSet N Q C) ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * (↑v * Real.log ↑(v + 1) ^ 2)

Ordinary primitive prefix-maximal large sieve for an arbitrary small cutoff. No comparison of coefficient values is used: the dependence on v enters only through the established small-coefficient energy bound.

theorem AnalyticNumberTheory.LargeSieve.standardBVSmall_squareLedger_payable_of_le_balanced (cutoff : ℕ → ℕ) (hcutoff : ∀ᶠ (N : ℕ) in Filter.atTop, cutoff N ≤ standardBVBalancedSmallCutoff N) (A κ B C : ℕ) : ∃ (K₀ : ℝ), 0 < K₀ ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have R := logConductorThreshold N C; have P := 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2; have X := ↑N / Real.log ↑N ^ (A + κ); P ^ 2 * (3 * highConductorHarmonicFactor Q R * primitivePrefixSquareLedgerOn (vaughanSmallCoeff vaughanUnitIntegerCoeff (cutoff N)) N (highConductorSet N Q C)) ≤ (K₀ * X) ^ 2

The complete weighted small square ledger is paid for any eventually balanced-bounded cutoff, with no coefficient zeroing.

def AnalyticNumberTheory.LargeSieve.StandardBVProductionAdaptiveBlockL1WeightedSource (loss : ℕ) : Prop

Weighted adaptive source used as the intermediate output of the five-log envelope payment. Its only cutoff restriction is the balanced upper bound.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVProductionAdaptiveBlockL1WeightedSource loss = ∀ (A : ℕ), have B := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent A loss; have C := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent A loss; ∃ (u : ℕ → ℕ) (v : ℕ → ℕ), (∀ (N : ℕ), v N ≤ AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff N) ∧ ∃ (K₁ : ℝ) (K₂ : ℝ), 0 < K₁ ∧ 0 < K₂ ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have P := 4 * AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q ^ 2; ∀ (hR : 0 < AnalyticNumberTheory.LargeSieve.logConductorThreshold N C), have G := AnalyticNumberTheory.LargeSieve.productionConductorBlockGeometry N Q C hR; AnalyticNumberTheory.LargeSieve.ProductionTypeIBlockMeanValue N (u N) (v N) loss P K₁ G ∧ AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValue N (u N) (v N) loss P K₂ G

def AnalyticNumberTheory.LargeSieve.StandardBVProductionAdaptiveBlockL1BareSource (loss : ℕ) : Prop

Adaptive bare block source. Since the existential pair is selected after A, both cutoffs may vary with A and N; no equality to a canonical cutoff is imposed, only v N ≤ the balanced cube-root cutoff.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVProductionAdaptiveBlockL1BareSource loss = ∀ (A : ℕ), have paidLoss := loss + 5; have B := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent A paidLoss; have C := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent A paidLoss; ∃ (u : ℕ → ℕ) (v : ℕ → ℕ), (∀ (N : ℕ), v N ≤ AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff N) ∧ ∃ (K₁ : ℝ) (K₂ : ℝ), 0 < K₁ ∧ 0 < K₂ ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; ∀ (hR : 0 < AnalyticNumberTheory.LargeSieve.logConductorThreshold N C), have G := AnalyticNumberTheory.LargeSieve.productionConductorBlockGeometry N Q C hR; AnalyticNumberTheory.LargeSieve.ProductionTypeIBlockMeanValueBare N (u N) (v N) loss K₁ G ∧ AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValueBare N (u N) (v N) loss K₂ G

theorem AnalyticNumberTheory.LargeSieve.standardBVProductionAdaptiveBlockL1WeightedSource_of_bare {loss : ℕ} (hbare : StandardBVProductionAdaptiveBlockL1BareSource loss) : StandardBVProductionAdaptiveBlockL1WeightedSource (loss + 5)

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_adaptiveBlockL1Weighted {loss : ℕ} (hblock : StandardBVProductionAdaptiveBlockL1WeightedSource loss) : StandardBVHighTypeITypeIIHybridChosenSource

Production block-L¹ chosen assembler. Type-I and Type-II use one shared pair u,v, with only v N ≤ standardBVBalancedSmallCutoff N; their block first moments are paid by the block geometry, while the retained small mean is paid by standardBVSmall_squareLedger_payable_of_le_balanced followed by the existing high-conductor weighted Cauchy inequality.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_adaptiveBlockL1Bare {loss : ℕ} (hbare : StandardBVProductionAdaptiveBlockL1BareSource loss) : StandardBVHighTypeITypeIIHybridChosenSource

Five-log envelope payment followed by the generalized small-lane payment.