Consuming the secondary r-mean on the original occupied carrier

Only nonnegative costs are enlarged to the actual dyadic r interval. The signed coefficient weight remains an exact, r-independent factor. The mean keeps the existing losses: the span is bounded by GridUpper+1, and the gcd average extends to (0,hi], rather than paying just the width.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramFouvryCost_nonneg {C : ℝ} (hC : 0 ≤ C) (ε : ℝ) (a : ℤ) (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (L : WGramLabel) : 0 ≤ wGramFouvryCost ε C a R S M Z K j cap L

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryDyadicMean (ε C : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (v : WGramSecondaryBase) : ℝ

Explicit dyadic mean for a fixed seven-coordinate base. The lower modulus uses 2^(j 3) and the averaging cost uses 2^(j 3+1)-1.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryDyadicMean ε C a R S K j cap v = C * ↑a.natAbs.divisors.card * (↑K.D' + ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper R S K j cap + 1) / ↑(v.1 * 2 ^ j 3 * v.2.1.2.1 * v.2.2.2.1)) * ↑(v.1 * (2 ^ (j 3 + 1) - 1) * v.2.1.2.1 * v.2.2.2.1) ^ (1 / 2 + ε) * (↑(2 ^ (j 3 + 1) - 1) * √↑(v.1 * v.2.2.2.1 * v.2.1.2.1 * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3SecondaryNumerator K.1.2.1 v.2.1.1 v.2.2.1 a v.2.1.2.2).natAbs.divisors.card))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryDyadicMean_nonneg {C : ℝ} (hC : 0 ≤ C) (ε : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (v : WGramSecondaryBase) : 0 ≤ wGramSecondaryDyadicMean ε C a R S K j cap v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryFiber_cost_le_mean {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {v : WGramSecondaryBase} (hv : v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))) : ∑ r ∈ wGramSecondaryFiber (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) v, wGramFouvryCost ε C a R S M Z K j cap (wGramSecondaryJoin v r) ≤ wGramSecondaryDyadicMean ε C a R S K j cap v

Eligibility comes from an occupied label. No positivity or nonzero coefficient is imposed on unoccupied bases, and no mean in n is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryLabels_weighted_cost_le {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) : ∑ L ∈ wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c), |wGramWeight K β ζ L| * wGramFouvryCost ε C a R S M Z K j cap L ≤ ∑ v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)), |wGramWeight K β ζ (wGramSecondaryJoin v 0)| * wGramSecondaryDyadicMean ε C a R S K j cap v

The original secondary aggregate is replaced by a proved mean. Every remaining fixed-data multiplicity and the exact absolute signed weight remain visible in the outer sum; this is not a globally normalized C.2 estimate.