theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachComposite_moving_lowerDensity (B ρ : ℝ) (hB : 0 ≤ B) (hρ : 0 < ρ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (ε : ℝ) (m : ℕ), 0 < m → ↑N ^ (8 / 53) ≤ ↑m → ↑m ≤ ↑N ^ (13 / 33) → have S := goldbachS3BoundingSieve N hEven ε (↑N ^ (4 / 53)) m; have D := LiuWeight.panModulusCutoff N B / m + 1; have t := Real.log ↑D / Real.log (↑N ^ (4 / 53)); 2 ≤ t → AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S * (JurkatRichert1965ChenGammaOneQOne.jr1965f t - ρ) ≤ BoundingSieve.mainSum (LinearSieve.lowerRosserWeight S.prodPrimes D)

The genuine moving natural layer on every composite modulus in the pair range. The single threshold precedes all N, epsilon and outer moduli. Only the active coordinate branch t >= 2 is asserted for the signed Rosser density.