Block-L¹ weighted primitive consumers for the production Vaughan rows

The analytic hypotheses in this file are block-local first-moment estimates for exactly the production Type-I and Type-II coefficients. The finite consumer converts d / φ(d) to the AP normalization on each block, reindexes a disjoint finite block partition exactly, and then uses only the two scalar geometric ledgers. The small lane is the production coefficient at standardBVBalancedSmallCutoff, hence is retained and paid through its square ledger plus high-conductor Cauchy. The former v = min N 1 path remains only as an explicitly named compatibility wrapper.

noncomputable def AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean (a : ℤ → ℂ) (N : ℕ) (S : Finset ℕ) : ℝ

The block-local d / φ(d) first moment, with the exact production prefix amplitude.

Equations

• AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean a N S = ∑ d ∈ S, ↑d / ↑d.totient * ∑ ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude a N d ψ

theorem AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean_nonneg (a : ℤ → ℂ) (N : ℕ) (S : Finset ℕ) : 0 ≤ blockWeightedPrimitiveMean a N S

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_le_inv_mul_blockWeighted (a : ℤ → ℂ) (N L : ℕ) (S : Finset ℕ) (hL : 0 < L) (hlevels : ∀ d ∈ S, L ≤ d) : apNormalizedPrimitiveMeanOn a N S ≤ 1 / ↑L * blockWeightedPrimitiveMean a N S

Exact pointwise normalization payment on a positive conductor block.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_eq_sum_blocks (a : ℤ → ℂ) (N Q C : ℕ) (G : ProductionConductorBlockGeometry N Q C) : apNormalizedPrimitiveMeanOn a N (highConductorSet N Q C) = ∑ i ∈ G.index, apNormalizedPrimitiveMeanOn a N (G.cell i)

Exact finite reindexing through a disjoint block partition.

theorem AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean_to_highMean (a : ℤ → ℂ) (N Q C loss : ℕ) (P K : ℝ) (G : ProductionConductorBlockGeometry N Q C) (hP : 0 ≤ P) (hK : 0 ≤ K) (hblock : ∀ i ∈ G.index, P * blockWeightedPrimitiveMean a N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)) : P * apNormalizedPrimitiveMeanOn a N (highConductorSet N Q C) ≤ K * Real.log ↑N ^ loss * (2 * ↑N / ↑(logConductorThreshold N C) + 8 * ↑Q * √↑N)

The complete finite block-L¹ consumer. A block estimate at the classical N + (2i)²√N scale pays the AP mean by 1/i; summing uses exactly the two geometric ledgers and nothing analytic.

theorem AnalyticNumberTheory.LargeSieve.productionTypeI_blockWeighted_to_highMean (N Q C u v loss : ℕ) (P K : ℝ) (G : ProductionConductorBlockGeometry N Q C) (hP : 0 ≤ P) (hK : 0 ≤ K) (hblock : ∀ i ∈ G.index, P * blockWeightedPrimitiveMean (vaughanTypeICoeff vaughanUnitIntegerCoeff u v) N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)) : P * highConductorVaughanTypeIMean N Q C u v ≤ K * Real.log ↑N ^ loss * (2 * ↑N / ↑(logConductorThreshold N C) + 8 * ↑Q * √↑N)

Exact production Type-I specialization of the generic finite consumer.

theorem AnalyticNumberTheory.LargeSieve.productionTypeII_blockWeighted_to_highMean (N Q C u v loss : ℕ) (P K : ℝ) (G : ProductionConductorBlockGeometry N Q C) (hP : 0 ≤ P) (hK : 0 ≤ K) (hblock : ∀ i ∈ G.index, P * blockWeightedPrimitiveMean (vaughanTypeIICoeff vaughanUnitIntegerCoeff u v) N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)) : P * highConductorVaughanTypeIIMean N Q C u v ≤ K * Real.log ↑N ^ loss * (2 * ↑N / ↑(logConductorThreshold N C) + 8 * ↑Q * √↑N)

Exact production Type-II specialization, retaining the production hyperbolic Vaughan coefficient.

def AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent (A loss : ℕ) : ℕ

Chosen exponents for paying a fixed block/shell logarithmic loss.

Equations

• AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent A loss = 2 * (A + loss + 1)

def AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent (A loss : ℕ) : ℕ

Equations

• AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent A loss = max (A + 3) (A + loss)

theorem AnalyticNumberTheory.LargeSieve.standardBVBlockL1_margin_B (A loss : ℕ) : A + 3 ≤ standardBVBlockL1ModulusExponent A loss

theorem AnalyticNumberTheory.LargeSieve.standardBVBlockL1_loss_le_C (A loss : ℕ) : A + loss ≤ standardBVBlockL1ConductorExponent A loss

theorem AnalyticNumberTheory.LargeSieve.standardBVBlockL1_loss_le_B (A loss : ℕ) : A + loss ≤ standardBVBlockL1ModulusExponent A loss

theorem AnalyticNumberTheory.LargeSieve.standardBVBlockL1_scales_payable (A loss : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, have C := standardBVBlockL1ConductorExponent A loss; have B := standardBVBlockL1ModulusExponent A loss; have R := logConductorThreshold N C; have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; Real.log ↑N ^ loss * (2 * ↑N / ↑R + 8 * ↑Q * √↑N) ≤ 10 * ↑N / Real.log ↑N ^ A

Scalar payment for the block analytic input. The choices satisfy both C ≥ A+loss and B ≥ A+loss; after the geometric block sum the two physical scales are bounded by 10 N/log(N)^A.

def AnalyticNumberTheory.LargeSieve.ProductionTypeIBlockMeanValueBare (N u v loss : ℕ) (K : ℝ) {Q C : ℕ} (G : ProductionConductorBlockGeometry N Q C) : Prop

Canonical envelope-free production Type-I block mean-value predicate. The analytic source controls the literal block mean; the elementary Abel/conductor envelope is paid only by the downstream consumer.

Equations

• AnalyticNumberTheory.LargeSieve.ProductionTypeIBlockMeanValueBare N u v loss K G = ∀ i ∈ G.index, AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)

def AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValueBare (N u v loss : ℕ) (K : ℝ) {Q C : ℕ} (G : ProductionConductorBlockGeometry N Q C) : Prop

Canonical envelope-free production Type-II block mean-value predicate.

Equations

• AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValueBare N u v loss K G = ∀ i ∈ G.index, AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)

def AnalyticNumberTheory.LargeSieve.ProductionTypeIBlockMeanValue (N u v loss : ℕ) (P K : ℝ) {Q C : ℕ} (G : ProductionConductorBlockGeometry N Q C) : Prop

Legacy compatibility predicate with the Abel/conductor envelope already multiplied into the analytic hypothesis.

Equations

• AnalyticNumberTheory.LargeSieve.ProductionTypeIBlockMeanValue N u v loss P K G = ∀ i ∈ G.index, P * AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)

def AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValue (N u v loss : ℕ) (P K : ℝ) {Q C : ℕ} (G : ProductionConductorBlockGeometry N Q C) : Prop

The parallel production Type-II block mean-value theorem, retaining the existing exact hyperbolic Vaughan coefficient.

Equations

• AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValue N u v loss P K G = ∀ i ∈ G.index, P * AnalyticNumberTheory.LargeSieve.blockWeightedPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (G.cell i) ≤ K * Real.log ↑N ^ loss * (↑N + (2 * ↑i) ^ 2 * √↑N)

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

Legacy v = min N 1 block source, retained only for compatibility with callers of the former degenerate small-lane assembler.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVProductionBlockL1WeightedLegacySource loss = ∀ (A : ℕ), have B := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent A loss; have C := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent A loss; ∃ (u : ℕ → ℕ) (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) (AnalyticNumberTheory.LargeSieve.standardBVChosenSmallCutoff N) loss P K₁ G ∧ AnalyticNumberTheory.LargeSieve.ProductionTypeIIBlockMeanValue N (u N) (AnalyticNumberTheory.LargeSieve.standardBVChosenSmallCutoff N) loss P K₂ G

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

Exact block analytic input on the canonical production dyadic geometry. Type-I and Type-II use the same moving u,v, and the production v is the balanced cube-root cutoff. No finite partition or geometric-ledger premise is exposed.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVProductionBlockL1WeightedSource loss = ∀ (A : ℕ), have B := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent A loss; have C := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent A loss; ∃ (u : ℕ → ℕ) (v : ℕ → ℕ), v = AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff ∧ ∃ (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

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_blockL1Weighted_legacy {loss : ℕ} (hblock : StandardBVProductionBlockL1WeightedLegacySource loss) : StandardBVHighTypeITypeIIHybridChosenSource

Compatibility assembler for the former degenerate v = min N 1 source. New production code must use standardBVHighTypeITypeIIHybridChosenSource_of_blockL1Weighted.

theorem AnalyticNumberTheory.LargeSieve.apNormalizedPrimitiveMeanOn_high_le_of_square_payment (a : ℤ → ℂ) (N Q C : ℕ) (P Z : ℝ) (hR : 1 ≤ logConductorThreshold N C) (hZ : 0 ≤ Z) (hpay : P ^ 2 * (3 * highConductorHarmonicFactor Q (logConductorThreshold N C) * primitivePrefixSquareLedgerOn a N (highConductorSet N Q C)) ≤ Z ^ 2) : P * apNormalizedPrimitiveMeanOn a N (highConductorSet N Q C) ≤ Z

Consume the actual high-conductor square payment for any coefficient. The factor three is the existing ledger reserve, not a new triangle bound. Only the target needs to be nonnegative; the multiplier may be signed.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_blockL1Weighted {loss : ℕ} (hblock : StandardBVProductionBlockL1WeightedSource loss) : StandardBVHighTypeITypeIIHybridChosenSource

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

theorem AnalyticNumberTheory.LargeSieve.productionAbelConductorEnvelope_le_logPow_two (B N : ℕ) (hN : 3 ≤ N) : have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2 ≤ 48 * Real.log ↑N ^ 2

The common quadratic envelope used by chosen Type-I/II payments and by bare block sources. The modulus is the actual Pan cutoff, including Q = 0.

theorem AnalyticNumberTheory.LargeSieve.productionAbelConductorEnvelope_le_logPow_five (B : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; 4 * discreteAbelAmplifierPrefixMax N * conductorHarmonicFactor Q ^ 2 ≤ 48 * Real.log ↑N ^ 5

The production Abel/conductor envelope costs at most five logarithms. The proof actually gives a quadratic logarithm; exponent five is frozen as a stable reserve for canonical bare block sources.

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

Canonical bare block source. Its analytic hypotheses contain no Abel/conductor factor. The selected exponents reserve the fixed five-log consumer payment.

Equations

• AnalyticNumberTheory.LargeSieve.StandardBVProductionBlockL1BareSource loss = ∀ (A : ℕ), have paidLoss := loss + 5; have B := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ModulusExponent A paidLoss; have C := AnalyticNumberTheory.LargeSieve.standardBVBlockL1ConductorExponent A paidLoss; ∃ (u : ℕ → ℕ) (v : ℕ → ℕ), v = AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff ∧ ∃ (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.productionTypeIBlockMeanValue_of_bare_logPow_five (N u v loss : ℕ) (P K : ℝ) {Q C : ℕ} (G : ProductionConductorBlockGeometry N Q C) (hP : P ≤ 48 * Real.log ↑N ^ 5) (hbare : ProductionTypeIBlockMeanValueBare N u v loss K G) : ProductionTypeIBlockMeanValue N u v (loss + 5) P (48 * K) G

Multiplying a bare Type-I block estimate by an envelope bounded by five logarithms shifts the loss by exactly five.

theorem AnalyticNumberTheory.LargeSieve.productionTypeIIBlockMeanValue_of_bare_logPow_five (N u v loss : ℕ) (P K : ℝ) {Q C : ℕ} (G : ProductionConductorBlockGeometry N Q C) (hP : P ≤ 48 * Real.log ↑N ^ 5) (hbare : ProductionTypeIIBlockMeanValueBare N u v loss K G) : ProductionTypeIIBlockMeanValue N u v (loss + 5) P (48 * K) G

Type-II version of the fixed five-log consumer payment.

theorem AnalyticNumberTheory.LargeSieve.standardBVProductionBlockL1WeightedSource_of_bare {loss : ℕ} (hbare : StandardBVProductionBlockL1BareSource loss) : StandardBVProductionBlockL1WeightedSource (loss + 5)

Consumer-side bridge: a canonical bare source becomes the balanced weighted source after the fixed loss translation.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_blockL1Bare {loss : ℕ} (hbare : StandardBVProductionBlockL1BareSource loss) : StandardBVHighTypeITypeIIHybridChosenSource

The canonical envelope-free block source is connected to the chosen high Standard-BV node; all envelope loss is paid in the consumer above.