Li–Liu's one-plus-one-point-nine theorem

This entry point exposes the unconditional existence theorem and the quantitative bound for distinct primes. Goldbach.Theorem remains the independent Chen 1+2 entry point. Import Goldbach.All to use both public interfaces together.

theorem Goldbach.one_plus_one_nine : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9

Every sufficiently large even integer has the Li–Liu representation, with its exponent restriction written using exact natural powers.

theorem Goldbach.one_plus_one_nine_real : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ ↑r ≤ ↑q ^ (19 / 10 - 1)

The same existence theorem in the paper's real-exponent notation.

theorem Goldbach.one_plus_one_nine_count : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → 1 / 2500 * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) < ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19 N)

The strict paper bound counts distinct primes p, using the Liu singular series.

theorem Goldbach.one_plus_one_nine_lower_bound (κ : ℝ) (hκ : κ < 515093 / 800000000) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → κ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19 N)

Fix the coefficient before choosing the common eventual threshold.