theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_outputDivisors_empty {N m d : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport N) (hNd : N.Coprime d) (hmd : ¬m.Coprime d) : {r ∈ goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m} = ∅

An inadmissible cofactor contributes no actual output divisible by d.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedDivisorResidual (N : ℕ) (ε : ℝ) (d : ℕ) : ℝ

Literal weighted divisor count of the geometric output mother, minus its coprime-gated prime-window main term. The counting sum runs over the whole E.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedDivisorResidual N ε d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | d ∣ N - r * m}.card - (∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N with m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * (AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiHi N m⌋₊ - AnalyticNumberTheory.LargeSieve.PanPrincipal.primeCount ⌊MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PiLiLo N ε m⌋₊)) / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedDivisorResidual_eq {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (d : ℕ) (hNd : N.Coprime d) : goldbachG12LinkedDivisorResidual N ε d = goldbachG12LinkedWindowResidual N ε d N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedDivisorResidual_log_saving (A : ℝ) (hA : 0 < A) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG12LinkedDivisorResidual N ε d| ≤ C * ↑N / Real.log ↑N ^ A

An unconditional distribution estimate for the actual output-divisor count. The sole remaining level restriction is the proved source's sqrt(N)/log(N)^B.