Independent literal and axiom checks for the Li–Liu public interface

theorem Goldbach.OnePlusOneNineChecks.oneNine : ∃ (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

Independent literal Li–Liu specification with exact natural powers.

theorem Goldbach.OnePlusOneNineChecks.count_is_literal (N : ℕ) : ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19 N) = ↑{p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ∃ (r : ℕ) (q : ℕ), (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9}.card

Extensional equality avoids relying on definitional equality of filter deciders.

theorem Goldbach.OnePlusOneNineChecks.paperCount : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → 4e-4 * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) < ↑{p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ∃ (r : ℕ) (q : ℕ), (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9}.card

Literal count of distinct primes p, rather than of representation witnesses.