AnalyticNumberTheory.Sieve.PanMainTerm

Polylogarithmic bounds for the pure main-term contribution

The coarse weighted Pan decomposition separates Type I (apV1), Type II (apV3), and a pure main-term piece after absorbing a into the residue class (Liu 2022 §III; Halberstam--Richert 1974 Ch. 10). This module supplies the reduction chain for the third piece, PanMainTermBound from PanMeanValueBody.lean §4.

Here li abbreviates the project's proxy logarithmicIntegral x = x/log x (BombieriVinogradov.lean), not the genuine logarithmic integral. For |f| ≤ 1, the unmaximized main term satisfies

|Σ_{(a,q)=1, a≤X} f(a)·li(⌊y/a⌋)/φ(q)|
  ≤ Σ_{1≤a≤X} |li(⌊y/a⌋)|/φ(q)
  ≤ (max_{y≤x} Σ_{1≤a≤X} |li(⌊y/a⌋)|)/φ(q).

Thus its weighted modulus sum is at most max_{y≤x} Σ_{1≤a≤X} |li(⌊y/a⌋)| · Σ_{q≤Q} μ²(q)·3^{ω(q)}/φ(q). PanMainTermBound.of_sieveBound reduces the bound to this product (PanMainTermSieveBound). The triangle inequality, |f| ≤ 1, both maxima, nonnegative weights, and the zero weight at q = 0 are all handled by finite algebra, parallel to the Type I reduction PanTypeICharacterMeanValue.of_sieveBound.

Elementary estimates for the two factors

• The (y,a) factor (§3): |li(m)| ≤ m/log 2 for every natural m, hence Σ_{1≤a≤X} |li(⌊y/a⌋)| ≤ (y/log 2)·(1 + log X). The maximum over y ≤ x is at most (x/log 2)·(1 + log X), by the harmonic-sum bound and ⌊y/a⌋ ≤ y/a.
• The q factor (§4): for squarefree q, μ²(q)·3^{ω(q)}/φ(q) = ∏_{p|q} 3/(p-1) (using goldbachNu_squarefree_eq_inv_totient). Subset expansion gives Σ_{q≤Q, squarefree} ∏_{p|q} c_p ≤ ∏_{p≤Q} (1+c_p). Combine 1+u ≤ exp u with Mertens' second theorem (mertensSecond_nat) to get Σ_{q≤Q} μ²(q)·3^{ω(q)}/φ(q) ≤ C·log⁶(Q+2).

Limitation: an absolute main term does not give a logarithmic saving

These estimates have product xX·polylog(xX). They cannot yield C·xX/log^A(xX): the term a = 1, q = 2, y = xX alone has size li(xX)/φ(2) ≈ xX/log(xX). The saving claim is already false for x X = X and A = 2; §6 also proves a counterexample to the corresponding absorption inequality.

The classical argument instead subtracts the sieve main term x/log x·∏(1-ν(p)) from the li contribution, leaving a signed error O(x/log^A x) (Liu §III; HR 1974 Ch. 10). That cancellation requires sieve-product and prime-distribution input, not an upper bound on the absolute main term. The signed-main-term requirements are discussed in PAN_PROOF_ATLAS.md and the main-term bridge in ROADMAP.

The results here have the provable polylogarithmic right side C·xX·(log xX)^{A+7}: panMainTotientWeightedSum_le_polylog bounds the q factor, panMainWeightedSum_polylog combines the elementary factors, and panMainSieveAbsorption_of_dom proves absorption into a larger log power under X ≤ x X. Finally, PanMainTermSieveBound.of_innerSumBound assembles the bound. These results belong to the coarse pure-main-term chain and do not establish the classical signed logarithmic-saving estimate.

1. Main-term inner sums and maximum reductions

noncomputable def AnalyticNumberTheory.Sieve.mainTermInnerSum (y X : ℕ) : ℝ

The pure main-term inner sum Σ_{1≤a≤X} |li(⌊y/a⌋)|. Its argument uses natural-number division, matching the truncation g (y / a) q ... in panPieceSum.

Equations

• AnalyticNumberTheory.Sieve.mainTermInnerSum y X = ∑ a ∈ Finset.Icc 1 X, |AnalyticNumberTheory.Sieve.logarithmicIntegral ↑(y / a)|

noncomputable def AnalyticNumberTheory.Sieve.mainTermInnerSumMax (X x : ℕ) : ℝ

Maximum of the inner sum over y ≤ x, mirroring panPieceMaxY.

Equations

• AnalyticNumberTheory.Sieve.mainTermInnerSumMax X x = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.mainTermInnerSum y X) (Finset.range (x + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.Sieve.panMainTotientWeightedSum (Q : ℕ) : ℝ

Weighted reciprocal-totient sum Σ_{q≤Q} μ²(q)·3^{ω(q)}/φ(q); the q = 0 term has zero weight.

Equations

• AnalyticNumberTheory.Sieve.panMainTotientWeightedSum Q = ∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card / ↑q.totient

theorem AnalyticNumberTheory.Sieve.mainTermInnerSum_nonneg (y X : ℕ) : 0 ≤ mainTermInnerSum y X

The inner sum is nonnegative.

theorem AnalyticNumberTheory.Sieve.mainTermInnerSumMax_nonneg (X x : ℕ) : 0 ≤ mainTermInnerSumMax X x

The maximum inner sum is nonnegative.

theorem AnalyticNumberTheory.Sieve.panMain_weight_nonneg (q : ℕ) : 0 ≤ ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card

Nonnegative weight: μ²(q)·3^{ω(q)} ≥ 0.

theorem AnalyticNumberTheory.Sieve.panMainPieceSum_abs_le (y X q : ℕ) (f : ℕ → ℝ) (l : ℕ) (hfb : ∀ (a : ℕ), |f a| ≤ 1) : |panPieceSum y X q l f fun (y' q' x : ℕ) => logarithmicIntegral ↑y' / ↑q'.totient| ≤ mainTermInnerSum y X / ↑q.totient

Pointwise main-term reduction: |panPieceSum| ≤ innerSum/φ(q) before taking maxima. The bound is uniform under |f| ≤ 1 and independent of l.

theorem AnalyticNumberTheory.Sieve.panMainPieceMaxL_le (y X q : ℕ) (f : ℕ → ℝ) (hfb : ∀ (a : ℕ), |f a| ≤ 1) : (panPieceMaxL y X q f fun (y' q' x : ℕ) => logarithmicIntegral ↑y' / ↑q'.totient) ≤ mainTermInnerSum y X / ↑q.totient

Residue-maximum reduction: panPieceMaxL ≤ innerSum/φ(q), since the bound is independent of l. For q = 0, the residue set is empty and nonnegativity gives the result.

theorem AnalyticNumberTheory.Sieve.panMainPieceMaxY_le (X q x : ℕ) (f : ℕ → ℝ) (hfb : ∀ (a : ℕ), |f a| ≤ 1) : (panPieceMaxY X q x f fun (y' q' x : ℕ) => logarithmicIntegral ↑y' / ↑q'.totient) ≤ mainTermInnerSumMax X x / ↑q.totient

Truncation-maximum reduction: panPieceMaxY ≤ innerSumMax/φ(q), by taking the maximum of the pointwise bounds panPieceMaxL ≤ innerSum/φ(q).

theorem AnalyticNumberTheory.Sieve.panMainWeightedSum_le (X Q x : ℕ) (f : ℕ → ℝ) (hfb : ∀ (a : ℕ), |f a| ≤ 1) : (∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * panPieceMaxY X q x f fun (y' q' x : ℕ) => logarithmicIntegral ↑y' / ↑q'.totient) ≤ mainTermInnerSumMax X x * ∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card / ↑q.totient

Weighted modulus-sum reduction: the main-term expression is at most innerSumMax · Σ_{q≤Q} μ²3^ω/φ(q). The q = 0 weight vanishes; for the other moduli use the pointwise bound and nonnegative weights.

1.1 Liu Section III: the non-decaying Selberg main term

The following finite identity models Liu's equation M₁: the li sum is multiplied by the Selberg quadratic factor. It is deliberately separate from the signed Pan remainder, whose inverse-log decay concerns π - li.

noncomputable def AnalyticNumberTheory.Sieve.panSelbergQuadraticFactor (D : Finset ℕ) (coeff : ℕ → ℝ) : ℝ

The Selberg quadratic factor Σ λ(d₁)λ(d₂)/φ([d₁,d₂]).

Equations

• AnalyticNumberTheory.Sieve.panSelbergQuadraticFactor D coeff = ∑ d₁ ∈ D, ∑ d₂ ∈ D, coeff d₁ * coeff d₂ / ↑(d₁.lcm d₂).totient

noncomputable def AnalyticNumberTheory.Sieve.panLiWeightSum (A : Finset ℕ) (f : ℕ → ℝ) (N : ℕ) : ℝ

Liu's weighted logarithmic-integral sum Σ f(a) li(N/a).

Equations

• AnalyticNumberTheory.Sieve.panLiWeightSum A f N = ∑ a ∈ A, f a * AnalyticNumberTheory.Sieve.logarithmicIntegral (↑N / ↑a)

noncomputable def AnalyticNumberTheory.Sieve.panSelbergLiMainTerm (D A : Finset ℕ) (coeff f : ℕ → ℝ) (N : ℕ) : ℝ

The unfactored finite Selberg–li main term.

Equations

• AnalyticNumberTheory.Sieve.panSelbergLiMainTerm D A coeff f N = ∑ d₁ ∈ D, ∑ d₂ ∈ D, coeff d₁ * coeff d₂ * ∑ a ∈ A, f a * (AnalyticNumberTheory.Sieve.logarithmicIntegral (↑N / ↑a) / ↑(d₁.lcm d₂).totient)

theorem AnalyticNumberTheory.Sieve.panSelbergLiMainTerm_eq_factor_mul (D A : Finset ℕ) (coeff f : ℕ → ℝ) (N : ℕ) : panSelbergLiMainTerm D A coeff f N = panSelbergQuadraticFactor D coeff * panLiWeightSum A f N

Finite main-term factorization (Liu §III, equation eqn-m1): the Selberg quadratic factor and the weighted li sum separate exactly.

2. Analytic input and reduction theorem

def AnalyticNumberTheory.Sieve.PanMainTermSieveBound (x f : ℕ → ℝ) : Prop

Pure main-term bound, polylogarithmic form: for each A > 0, there exist C > 0, B, and x₀ such that for all X ≥ x₀, with Q = (xX)^{1/2}/log^B(xX), innerSumMax(X, ⌊xX⌋) · Σ_{q≤Q} μ²(q)·3^{ω(q)}/φ(q) ≤ C·xX·(log xX)^{A+7}. Here innerSumMax(X,x) = max_{y≤x} Σ_{1≤a≤X} |li(⌊y/a⌋)|.

A right side C·xX/log^A(xX) would be false for the pure main-term piece: for x X = X and A = 2, its left side is at least li(X)·1 ~ X/log X, exceeding C·X/log²X eventually. The classical saving comes from subtracting the sieve main term x/log x·∏(1-ν(p)) (Liu 2022 §III; HR 1974 Ch. 10), requiring a sieve-product object and signed main-term analysis (see PAN_PROOF_ATLAS.md and the main-term bridge in ROADMAP).

The elementary factors in §§3--4 instead give xX·(1+log X)·log⁶(xX+2), of total logarithmic degree 7. PanMainSieveAbsorption in §6 bounds this by the larger power C·xX·(log xX)^{A+7} under domination of X by x X.

Equations

• AnalyticNumberTheory.Sieve.PanMainTermSieveBound x f = ((∀ (a : ℕ), |f a| ≤ 1) ∧ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → AnalyticNumberTheory.Sieve.mainTermInnerSumMax X ⌊x X⌋₊ * ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card / ↑q.totient ≤ C * x X * Real.log (x X) ^ (A + 7))

theorem AnalyticNumberTheory.Sieve.PanMainTermBound.of_sieveBound {x f : ℕ → ℝ} (hS : PanMainTermSieveBound x f) : PanMainTermBound x f

Main-term reduction theorem: PanMainTermSieveBound implies PanMainTermBound. The triangle inequality, |f| ≤ 1, both maximum reductions, nonnegative weights, and zero weight at q = 0 are finite algebra; the only analytic hypothesis is the supplied sieve bound.

3. Elementary li-proxy bounds and the (y,a) factor

For every natural m, |li(m)| ≤ m/log 2: if m ≥ 2, li(m) = m/log m ≤ m/log 2, while li(0) = li(1) = 0. The harmonic bound Σ_{1≤a≤X} 1/a ≤ 1+log X and ⌊y/a⌋ ≤ y/a then give Σ_{1≤a≤X} |li(⌊y/a⌋)| ≤ (y/log 2)·(1+log X). Taking the maximum over y ≤ x yields mainTermInnerSumMax ≤ (x/log 2)·(1+log X).

This bounds the (y,a) factor in PanMainTermSieveBound. More refined classical estimates use sums such as Σ 1/(a·log(y/a)) ≪ log log X in the appropriate ranges (see Mertens partial summation); the coarse log X bound is sufficient here, where the exact polylogarithmic exponent is inessential.

theorem AnalyticNumberTheory.Sieve.logIntegral_nat_abs_le (m : ℕ) : |logarithmicIntegral ↑m| ≤ ↑m / Real.log 2

Uniform elementary proxy bound: |li(m)| ≤ m/log 2 for natural m. li(0) = li(1) = 0; for m ≥ 2, li(m) = m/log m ≤ m/log 2.

theorem AnalyticNumberTheory.Sieve.mainTermInnerSum_le (X y : ℕ) : mainTermInnerSum y X ≤ ↑y / Real.log 2 * (1 + Real.log ↑X)

Main-term inner-sum bound: Σ_{1≤a≤X} |li(⌊y/a⌋)| ≤ (y/log 2)·(1+log X). This controls the (y,a) factor under |f| ≤ 1, by the harmonic sum, the floor bound, and |li(m)| ≤ m/log 2.

theorem AnalyticNumberTheory.Sieve.mainTermInnerSumMax_le (X x : ℕ) : mainTermInnerSumMax X x ≤ ↑x / Real.log 2 * (1 + Real.log ↑X)

Maximum inner-sum bound: max_{y≤x} Σ_{1≤a≤X} |li(⌊y/a⌋)| ≤ (x/log 2)·(1+log X).

4. The q factor: weighted reciprocal-totient sum

For squarefree q, μ²(q)·3^{ω(q)}/φ(q) = ∏_{p|q} 3/(p-1). Subset expansion gives Σ_{q≤Q, squarefree} ∏_{p|q} c_p ≤ ∏_{p≤Q} (1+c_p). Using ∏(1+u) ≤ exp(Σu) and Mertens' second theorem (mertensSecond_nat) yields Σ_{q≤Q} μ²(q)·3^{ω(q)}/φ(q) ≤ C·log⁶(Q+2).

The ingredients are elementary: μ² is 1 on squarefree integers and 0 otherwise; squarefree integers are determined by their prime-factor sets; and Σ 1/(p-1) ≤ 2Σ 1/p, followed by Mertens.

theorem AnalyticNumberTheory.Sieve.panMainTotientWeight_term_squarefree (q : ℕ) (hq : Squarefree q) : ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card / ↑q.totient = ∏ p ∈ q.primeFactors, 3 / (↑p - 1)

Main-term weight for squarefree q: μ²(q)·3^{ω(q)}/φ(q) = ∏_{p|q} 3/(p-1).

theorem AnalyticNumberTheory.Sieve.panMainTotientWeight_term_non_squarefree (q : ℕ) (hq : ¬Squarefree q) : ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card / ↑q.totient = 0

The main-term weight vanishes for nonsquarefree q, since μ(q) = 0.

theorem AnalyticNumberTheory.Sieve.sum_squarefree_prod_primeFactors_le_prod_one_add (Q : ℕ) (c : ℕ → ℝ) (hc : ∀ (p : ℕ), Nat.Prime p → 0 ≤ c p) : ∑ q ∈ Finset.range (Q + 1) with Squarefree q, ∏ p ∈ q.primeFactors, c p ≤ ∏ p ∈ Mertens.primesUpTo Q, (1 + c p)

Subset bound: for nonnegative coefficients, Σ_{q≤Q, squarefree} ∏_{p|q} c p ≤ ∏_{p≤Q} (1+c p). A squarefree integer is determined by its prime-factor set, q = ∏ p ∈ q.primeFactors, p, and the product on the right expands into the sum of ∏_{p∈S} c p over all subsets S ⊆ {p prime : p ≤ Q}.

theorem AnalyticNumberTheory.Sieve.panMainTotientWeightedSum_le_prod_one_add (Q : ℕ) : panMainTotientWeightedSum Q ≤ ∏ p ∈ Mertens.primesUpTo Q, (1 + 3 / (↑p - 1))

The weighted reciprocal-totient sum is bounded by ∏_{p≤Q} (1+3/(p-1)).

theorem AnalyticNumberTheory.Sieve.panMainTotientWeightedSum_mono : Monotone panMainTotientWeightedSum

The weighted reciprocal-totient sum is monotone in Q, since its summands are nonnegative.

theorem AnalyticNumberTheory.Sieve.panMainTotientWeightedSum_le_polylog : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℕ), panMainTotientWeightedSum Q ≤ C * Real.log (↑Q + 2) ^ 6

Polylogarithmic q-factor bound: Σ_{q≤Q} μ²(q)·3^{ω(q)}/φ(q) ≤ C·log⁶(Q+2). Use subset expansion, ∏(1+u) ≤ exp(Σu), Σ_{p≤Q} 3/(p-1) ≤ 6·Σ_{p≤Q} 1/p, and Mertens' second theorem. Absorb the finite initial range Q ≤ 2 into the constant.

5. Combined polylogarithmic main-term bound

Under |f| ≤ 1, the weighted main-term sum is bounded by C·|xX|·(1+log X)·log⁶(Q+2), using the elementary proxy estimate |li(m)| ≤ m/log 2, the harmonic sum, and the q-factor bound. This is the intermediate estimate for PanMainTermSieveBound. Its absorption into C·xX·(log xX)^{A+7} is the content of PanMainSieveAbsorption in §6: a fixed polylogarithmic factor is dominated by a larger logarithmic power.

theorem AnalyticNumberTheory.Sieve.panMainWeightedSum_polylog (x f : ℕ → ℝ) (hfb : ∀ (a : ℕ), |f a| ≤ 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (X Q : ℕ), (∑ q ∈ Finset.range (Q + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * panPieceMaxY X q ⌊x X⌋₊ f fun (y q' x : ℕ) => logarithmicIntegral ↑y / ↑q'.totient) ≤ C * |x X| * (1 + Real.log ↑X) * Real.log (↑Q + 2) ^ 6

6. Polylogarithmic absorption and the main-term sieve bound

def AnalyticNumberTheory.Sieve.PanMainSieveAbsorption (x : ℕ → ℝ) : Prop

Polylogarithmic absorption proposition: assume the sieve scale dominates the summation range, X ≤ x X (as for x X = (X : ℝ)). Then the fixed factor (1+log X)·log⁶(xX+2) is eventually dominated by any larger logarithmic power: ∀ A > 0, ∃ C > 0, x₀, ∀ X ≥ x₀, xX·(1+log X)·log⁶(xX+2) ≤ C·xX·(log xX)^{A+7}.

Replacing the right side by C·xX/log^A(xX) is impossible: for x X ≡ 2, the factor 1+log X is unbounded while the right side is constant; for x X = X, it would require (1+log X)·log⁶(X+2) ≤ C/log^A X, whose left side grows like log⁷X and whose right side tends to zero.

The classical error O(x/log^A x) comes from subtracting the sieve main term x/log x·∏(1-ν(p)) from li (Liu 2022 §III; HR 1974 Ch. 10), requiring signed main-term and sieve-product analysis (see PAN_PROOF_ATLAS.md). A bound on one absolute contribution only gives a larger log power, of total degree 7 here. panMainSieveAbsorption_of_dom in §6.1 proves this proposition.

Equations

• AnalyticNumberTheory.Sieve.PanMainSieveAbsorption x = ((∀ (X : ℕ), ↑X ≤ x X) ∧ ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → x X * (1 + Real.log ↑X) * Real.log (x X + 2) ^ 6 ≤ C * x X * Real.log (x X) ^ (A + 7))

6.1 Proof of polylogarithmic absorption

For (X : ℝ) ≤ x X, the proof has three steps:

1. Eventual log lower bound (panMainSieve_log_ge_one): monotonicity gives log X ≤ log(xX), while Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop gives log X → ∞. Hence eventually 1 ≤ log(xX).
2. Product bound (panMainSieve_polylog_le, natural powers): for X ≥ 2 and 1 ≤ log(xX), log(xX+2) ≤ log(2·xX) = log 2 + log(xX) ≤ 2·log(xX), and 1+log X ≤ 2·log(xX). Thus (1+log X)·log⁶(xX+2) ≤ (2L)·(2L)^6 = 128·log⁷(xX).
3. Larger exponent (panMainSieveAbsorption_of_dom): for base log(xX) ≥ 1, use Real.rpow_le_rpow_of_exponent_le and 7 ≤ A+7 from A > 0, then multiply by xX ≥ 0.

The theorem not_panMainSieveAbsorption_old_natCast disproves the corresponding logarithmic-saving absorption for x X = X. Taking A = 1 and cancelling X > 0 would give (1+log X)·log⁶(X+2)·log X ≤ C; its left side is at least log X → ∞, contradicting every fixed C. Even refining the inner-sum upper bound to the classical C·xX·(1+log log xX) shape in suitable ranges does not turn the additional log⁶ upper bound into a logarithmic saving. Such a saving concerns a difference, |li main term − sieve main term| ≪ x/log^A x, with the sieve product written as ∏(1-ν(p)/p) when ν uses the unnormalized density convention. It is not a bound on the separate absolute contributions.

There is also a decomposition issue (see PanVaughanPointwise.lean): this module bounds the coarse pure-|li| inner sum mainTermInnerSumMax·Σ. By contrast, finite Vaughan algebra (panWeightedVonMangoldt_abs_le) produces |Σ f(a)·(apSmall − apMiddle)|. After the analytic ψ-to-π conversion, the classical third piece is the signed difference |Σ f(a)·((apSmall − apMiddle)/log(y/a) − li(y/a)/φ(q))|. The separate signed assembly must control this PNT-level main term; the pure-li polylogarithmic bound cannot replace it. See PAN_PROOF_ATLAS.md for the signed-main-term and Chen-weight requirements. The proof here uses elementary mathlib analysis: limits, real powers, and logarithm monotonicity.

theorem AnalyticNumberTheory.Sieve.panMainSieve_log_ge_one {x : ℕ → ℝ} (hdom : ∀ (X : ℕ), ↑X ≤ x X) : ∀ᶠ (X : ℕ) in Filter.atTop, 1 ≤ Real.log (x X)

Eventual logarithmic lower bound: if (X : ℝ) ≤ x X, then eventually 1 ≤ log(x X), from log X → ∞ and log X ≤ log(xX).

theorem AnalyticNumberTheory.Sieve.panMainSieve_polylog_le {x : ℕ → ℝ} (hdom : ∀ (X : ℕ), ↑X ≤ x X) : ∀ᶠ (X : ℕ) in Filter.atTop, (1 + Real.log ↑X) * Real.log (x X + 2) ^ 6 ≤ 128 * Real.log (x X) ^ 7

Polylogarithmic product bound (natural powers): under (X : ℝ) ≤ x X, eventually (1+log X)·log⁶(xX+2) ≤ 128·log⁷(xX). The first factor is at most 2·log(xX) once 1 ≤ log(xX); the second is at most (2·log(xX))^6, by monotonicity, log(2·xX) = log 2 + log(xX), and log 2 ≤ log(xX).

theorem AnalyticNumberTheory.Sieve.panMainSieveAbsorption_of_dom {x : ℕ → ℝ} (hdom : ∀ (X : ℕ), ↑X ≤ x X) : PanMainSieveAbsorption x

Polylogarithmic absorption under domination: for X ≤ x X, use C = 128 and an eventual threshold covering 1 ≤ log(xX) and X ≥ 1. The fixed factor is dominated by a larger log power; eventually_atTop.mp converts eventuality into an explicit ∃ x₀.

theorem AnalyticNumberTheory.Sieve.panMainSieveAbsorption_natCast : PanMainSieveAbsorption fun (N : ℕ) => ↑N

The scale x X = (X : ℝ) satisfies domination definitionally, so it satisfies PanMainSieveAbsorption.

theorem AnalyticNumberTheory.Sieve.not_panMainSieveAbsorption_old_natCast : ¬∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ↑X * (1 + Real.log ↑X) * Real.log (↑X + 2) ^ 6 ≤ C * ↑X / Real.log ↑X ^ A

Counterexample to logarithmic-saving absorption: for x X = (X : ℝ), the assertion that the polylogarithmic factor is bounded by C·xX/log^A(xX) is false. Take A = 1 and cancel X > 0; the inequality becomes (1+log X)·log⁶(X+2)·log X ≤ C, with left side at least log X → ∞. Thus every C > 0 and threshold x₀ are exceeded. This is the obstruction in §6: the coarse pure-main-term bound under |f| ≤ 1, after discarding coprimality weights, cannot yield x/log^A x. The classical saving is a signed difference estimate involving the sieve main term.

theorem AnalyticNumberTheory.Sieve.PanMainTermSieveBound.of_innerSumBound {x f : ℕ → ℝ} (hfb : ∀ (a : ℕ), |f a| ≤ 1) (hAbs : PanMainSieveAbsorption x) : PanMainTermSieveBound x f

Main-term sieve-bound assembly: PanMainSieveAbsorption implies PanMainTermSieveBound. The proxy bound, harmonic sum, q-factor estimate, floor/square-root reductions, and nonnegative weights are handled here; absorption is the analytic input. The right side is the polylogarithmic C·xX·(log xX)^{A+7}, not a logarithmic saving.