noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveSiftedRHS (A : Finset ℕ) (N : ℕ) (ε z b c T Z : ℝ) : ℤ

The actual twelve-term expression with a labelled sifted B10 source. Only the tenth source changes; no output or factor labels are deduplicated.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveSiftedRHS A N ε z b c T Z = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveBase A N z b c T - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount N ε b c Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_twelve_sifted_log_scale_eventually (ε δ θ : ℝ) (hε : 0 < ε) (hεu : ε < 2 / 15) (hδ : 0 < δ) (_hθ0 : 0 ≤ θ) (hθ1 : θ < 1) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (α β γ Z : ℝ), 1 / 18 < α → α < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → 1 ≤ Z → Z ≤ ↑N ^ θ → ↑(goldbachWeightTwelveSiftedRHS (goldbachDifferenceCarrier N ε) N ε (↑N ^ α) (↑N ^ β) (↑N ^ γ) (↑N ^ (9 / 19 - ε)) Z) - δ * ↑N / Real.log ↑N ^ 2 ≤ 4 * ↑(D19 N)

A uniform analytic-scale lower bound from the actual sifted labelled source. The fixed theta is strictly below one; the threshold precedes every Z and all sieve exponents. This supplies no analytic bound on the sifted main term.