noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingEight (A : Finset ℕ) (N : ℕ) (z b c : ℝ) : ℤ

The eight literal signed terms left after consuming both S1 terms and S2. No analytic estimate or positivity is built into this finite expression.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightRemainingEight A N z b c = -MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3Closed A N z (↑N ^ (1 / 3)) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3Closed A N z c + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG6 A N z b + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG7 A N z b c - 2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4 A N c - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed A N z (↑N ^ (1 / 3)) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11 A N z b - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12 A N z b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveBase_eq_positivePair_sub_s2_add_remainingEight (A : Finset ℕ) (N : ℕ) (z b c T : ℝ) : goldbachWeightTwelveBase A N z b c T = 3 * goldbachS1 A N z + goldbachS1 A N b - 4 * goldbachS2 A N T + goldbachWeightRemainingEight A N z b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_remainingEight_S1_S2_I10_consumed_eventually (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightRemainingEight (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) + ((1 - ε) * Real.exp (-Real.eulerMascheroniConstant) * (159 / 2 * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 6 + 33 / 2 * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (33 / 8)) - 32 * Real.log ((1 - (9 / 19 - ε)) / (9 / 19 - ε)) - 8 * (1 - ε) * goldbachB10I10 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Actual D19 consumer: both S1 lower bounds, the S2 upper bound (with its external multiplicity four), and I10 are consumed. Eight signed terms remain.