theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_three_triples_le_s6_add_b6 (A : Finset ℕ) (N : ℕ) {α β γ : ℝ} (hN : 2 ≤ N) (hz : 2 ≤ ↑N ^ α) (hαβ : α ≤ β) (hβ : 1 / 18 < β) (hβγ : β < (1 - 3 * β) / 3) (hγ : (1 - 3 * β) / 3 < γ) (hγu : γ < 1 / 3) : goldbachWeightT14 A N (↑N ^ α) (↑N ^ β) + goldbachWeightT15 A N (↑N ^ α) (↑N ^ β) (↑N ^ γ) + goldbachWeightT16 A N (↑N ^ β) (↑N ^ γ) ≤ goldbachS6Closed A N (↑N ^ α) (↑N ^ (1 / 3)) + goldbachB6 A N (↑N ^ α) (↑N ^ β)

The literal three-resource coverage, with the actual shared endpoint.

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

The common eleven terms, with their literal finite carriers. The omitted negative term is separately either corrected G10 or the labelled prime source.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveBase A N z b c T = 3 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1 A N z + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1 A N b - 4 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2 A N T - 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

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

The corrected twelve-term expression; this is not the printed G10 expression.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveCorrectedRHS A N z b c T = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveBase A N z b c T - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG10Corrected A N b c

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

The twelve-term expression with the genuine labelled prime source in place of corrected G10. No analytic estimate of that source is built into this definition.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveSwitchedRHS A N ε z b c T = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightTwelveBase A N z b c T - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPi10 N ε b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_twelve_corrected_lower_bound_eventually (ε : ℝ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (α β γ : ℝ), 1 / 18 < α → α < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → ↑(goldbachWeightTwelveCorrectedRHS (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β) (↑N ^ γ) (↑N ^ (9 / 19 - ε))) - 1334 * ↑N ^ (1 - α) ≤ 4 * ↑(D19 N)

The actual D19 lower bound for the corrected twelve-term formula, with all finite losses paid. This is a signed lower bound, not a positivity theorem.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_twelve_switched_lower_bound_eventually (ε : ℝ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (α β γ : ℝ), 1 / 18 < α → α < β → β < (1 - 3 * β) / 3 → (1 - 3 * β) / 3 < γ → γ < 1 / 3 → ↑(goldbachWeightTwelveSwitchedRHS (goldbachDifferenceCarrier N ε) N ε (↑N ^ α) (↑N ^ β) (↑N ^ γ) (↑N ^ (9 / 19 - ε))) - 2214 * ↑N ^ (1 - α) ≤ 4 * ↑(D19 N)

The same actual lower bound with labelled Pi10 and its additional finite payment. This still does not assert an analytic bound or positive main term.