Divisor-free explicit main contribution

In addition to the joint gcd mean, the remaining single completion factor tau(|a|) is paid by its proved uniform subpower bound. The already paid zero and secondary contributions are kept literally unchanged.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainSubpowerFactor (κ δ C Ca : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainSubpowerFactor κ δ C Ca a R S K j cap = C * (Ca * ↑a.natAbs ^ δ) * (↑K.D' + ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper R S K j cap + 1) / ↑(2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4)) * ↑(2 ^ (j 2 + 1) * (2 ^ (j 3 + 1) - 1) * 2 ^ (j 4 + 1) * 2 ^ (j 4 + 1)) ^ (1 / 2 + κ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramDirectMainCostFactor_le_subpower {δ : ℝ} (hδ : 0 < δ) : ∃ (Ca : ℝ), 0 < Ca ∧ ∀ (κ C : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ), 0 ≤ C → a ≠ 0 → wGramDirectMainCostFactor κ C a R S K j cap ≤ wGramDirectMainSubpowerFactor κ δ C Ca a R S K j cap

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_direct_main_subpower {ε κ δ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hδ : 0 < δ) : ∃ (Czero : ℝ) (Cnonzero : ℝ) (Csecondary : ℝ) (Cτ : ℝ) (Cjoint : ℝ) (Ca : ℝ), 0 < Czero ∧ 0 < Cnonzero ∧ 0 < Csecondary ∧ 0 < Cτ ∧ 0 < Cjoint ∧ 0 < Ca ∧ ∀ (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z T εSupport : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) (Bβ Bζ : ℝ), a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → (∀ n ∈ N, n ≤ F) → 1 < x → η < εSupport → x ^ εSupport ≤ T → 0 ≤ Bβ → 0 ≤ Bζ → (∀ n ∈ N, |β n| ≤ Bβ) → (∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) → wSeparatedCorrelationEnergy x N S (wGramPrefix N a x η R S M Z K b j cap positive) c K β ζ a ≤ (Bβ * Bζ) ^ 2 * ↑(2 ^ j 1) * Czero * ↑(wGramResonanceScaleBoxCard K F j) * wGramResonanceScaleEnvelope K F j ε + (wGramSecondaryBaseCountBound K F j * ((Bβ * Bζ) ^ 2 * wGramSecondaryScaleEnvelope κ δ Cnonzero Csecondary a R S K F j cap) + (Bβ * Bζ) ^ 2 * wGramDirectMainSubpowerFactor κ δ Cnonzero Ca a R S K j cap * wGramMainJointMean δ Cτ Cjoint a K F j)

No main gcd, divisor, or label sum remains. All constants are selected before every family, signed shift, key, prefix and scale.