Paying the actual occupied zero fibers by their divisor encoding

The divisor variables are (n₂,s); cancellation determines the signed h'. The coefficient-dependent majorant preserves both original beta/zeta factors. The k payment is only 2^(j 1), obtained from the actual interval.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceProduct (v : WGramResonanceBase) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceProduct v = v.2.1 * ↑v.2.2.1 * ↑v.2.2.2

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceDivisorMass (K : WExtractedKey) (β ζ : ℕ → ℝ) (v : WGramResonanceBase) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceDivisorMass K β ζ v = ∑ m ∈ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceProduct v).natAbs.divisors, ∑ s ∈ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceProduct v * (↑K.1.2.1 * ↑v.1.2 - ↑m)).natAbs.divisors, |MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramWeight K β ζ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceJoin v (m, s, 0))|

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceFiber_card_le_divisor_sum {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} (ha : a ≠ 0) {x η R S M Z T : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (hNT : ∀ n ∈ N, T ≤ ↑n) (hT : x ^ η < T) {K : WExtractedKey} {b : ℕ} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {v : WGramResonanceBase} (hv : v ∈ wGramResonanceBases (wGramZeroLabels K a V)) : (wGramResonanceFiber (wGramZeroLabels K a V) v).card ≤ ∑ m ∈ (wGramResonanceProduct v).natAbs.divisors, (fouvryTau 2) (wGramResonanceProduct v * (↑K.1.2.1 * ↑v.1.2 - ↑m)).natAbs

The genuine aggregate divisor count is instantiated on each occupied resonance base, not on a new caller-supplied canonical carrier.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceFiber_weighted_le_divisor_mass {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} (ha : a ≠ 0) {x η R S M Z T : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (hNT : ∀ n ∈ N, T ≤ ↑n) (hT : x ^ η < T) {K : WExtractedKey} {b : ℕ} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) {v : WGramResonanceBase} (hv : v ∈ wGramResonanceBases (wGramZeroLabels K a V)) : ∑ t ∈ wGramResonanceFiber (wGramZeroLabels K a V) v, |wGramWeight K β ζ (wGramResonanceJoin v t)| * ↑(wGramPairCount N a x η R S M Z K b j cap positive c (wGramResonanceJoin v t)) ≤ ↑(2 ^ j 1) * wGramResonanceDivisorMass K β ζ v

The weighted count retains the coordinate dependence of the coefficients; it does not require any coefficient envelope.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramZeroLabels_sum_le_divisor_mass {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} (ha : a ≠ 0) {x η R S M Z T : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (hNT : ∀ n ∈ N, T ≤ ↑n) (hT : x ^ η < T) {K : WExtractedKey} {b : ℕ} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) : ∑ L ∈ wGramZeroLabels K a V, |wGramWeight K β ζ L| * ↑(wGramPairCount N a x η R S M Z K b j cap positive c L) ≤ ↑(2 ^ j 1) * ∑ v ∈ wGramResonanceBases (wGramZeroLabels K a V), wGramResonanceDivisorMass K β ζ v

All actual zero labels are regrouped and paid by the proved weighted divisor encoding. Every common-k multiplicity has already been counted.