Li--Liu's literal 1 + 1.9 count and actual finite Goldbachbasic bridge

This module freezes the objects at labels p+rq/r<, D1a, and Goldbachbasic of Li--Liu (2026). The exponent condition for a = 19/10 is kept entirely in natural-number arithmetic:

r ≤ q^(9/10) is represented by r^10 ≤ q^9.

In particular, this is not an encoding by an unrestricted almost-prime predicate. The witnesses r and q, their primality conditions, and the size relation all remain literal.

@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.instDecidable_mathlibNt (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.instDecidable_mathlibNt P = Classical.propDecidable P

The literal representation predicate and D_{1,19/10}(N)

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.IsOnePlusOneNineRepresentation (N p : ℕ) : Prop

A literal Li--Liu 1 + 1.9 representation of N, with p retained as the counted variable. This is label p+rq/r< specialized to a = 19/10. The rational-power inequality is cleared to r^10 ≤ q^9.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.IsOnePlusOneNineRepresentation N p = (Nat.Prime p ∧ ∃ (r : ℕ) (q : ℕ), (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.onePlusOneNineRepresentedPrimes (N : ℕ) : Finset ℕ

The finite set of primes p counted by Li--Liu's D_{1,19/10}(N). The range cutoff is inclusive because range (N + 1) represents p ≤ N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.onePlusOneNineRepresentedPrimes N = Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.IsOnePlusOneNineRepresentation N) (Finset.range (N + 1))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19 (N : ℕ) : ℕ

Literal finite representation count D_{1,19/10}(N) from label D1a. It counts admissible values of p, exactly as the displayed set in the source, rather than counting witness triples (p,r,q).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19 N = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.onePlusOneNineRepresentedPrimes N).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.mem_onePlusOneNineRepresentedPrimes_iff {N p : ℕ} : p ∈ onePlusOneNineRepresentedPrimes N ↔ p ≤ N ∧ IsOnePlusOneNineRepresentation N p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19_pos_iff (N : ℕ) : 0 < D19 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

Positive literal count is equivalent to existence of a literal p + r*q representation satisfying the cleared 1.9 constraint.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19_ne_zero_iff (N : ℕ) : D19 N ≠ 0 ↔ ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9

A literal finite form of the first Goldbachbasic weight

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast (z n : ℕ) : Prop

P⁻(n) ≥ z, written without choosing a real-power cutoff: every prime divisor of n is at least the natural cutoff z.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast z n = ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ∣ n → z ≤ ℓ

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast (k n : ℕ) : Prop

The source's multiplicity-counting condition Ω(n) ≥ k.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast k n = (k ≤ n.primeFactorsList.length)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasicWeight (zAlpha zTau n : ℕ) : ℤ

The four-term pointwise weight in Goldbachbasic, valued in ℤ so that the displayed subtractions are literal.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasicWeight zAlpha zTau n = (((if MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zAlpha n then 1 else 0) - if MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zTau n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast 2 n then 1 else 0) + if MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zTau n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast 3 n then 1 else 0) - if MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zAlpha n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast 3 n then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasicFiniteRHS (A : Finset ℕ) (zAlpha zTau : ℕ) : ℤ

The four finite cardinalities on the right side of Goldbachbasic. A is the finite Goldbach difference carrier; zAlpha,zTau are exact natural cutoffs standing for the source's N^α,N^τ.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasicFiniteRHS A zAlpha zTau = ↑(Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zAlpha) A).card - ↑{n ∈ A | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zTau n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast 2 n}.card + ↑{n ∈ A | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zTau n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast 3 n}.card - ↑{n ∈ A | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.LeastPrimeFactorAtLeast zAlpha n ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.OmegaAtLeast 3 n}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.sum_goldbachBasicWeight_eq_finiteRHS (A : Finset ℕ) (zAlpha zTau : ℕ) : ∑ n ∈ A, goldbachBasicWeight zAlpha zTau n = goldbachBasicFiniteRHS A zAlpha zTau

Complete finite combinatorial identity behind the displayed four sums in Goldbachbasic. No asymptotic or analytic premise enters this theorem.

Actual pointwise producer

Source: 1+1.9v2.tex, lines 845--900; PDF pp. 12--13. The proposition's second indicator is Ω ≥ 2. The proof's opening display locally prints Ω = 2, contrary to the proposition and its own Case 3. We retain the proposition's four terms without changing the existing weight. The final result is an eventual specialization, not the printed effective cutoff.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachPrimeCarrier (N : ℕ) (ε : ℝ) : Finset ℕ

The source's prime carrier uses the linear cutoff (1-ε)N.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachPrimeCarrier N ε = {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ ↑p < (1 - ε) * ↑N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachPowerCutoff (N : ℕ) (β : ℝ) : ℕ

Exact natural cutoff, preserving the real weak inequality at integer primes.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachPowerCutoff N β = ⌈↑N ^ β⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.leastPrimeFactorAtLeast_powerCutoff_iff (N n : ℕ) (β : ℝ) : LeastPrimeFactorAtLeast (goldbachPowerCutoff N β) n ↔ ∀ (r : ℕ), Nat.Prime r → r ∣ n → ↑N ^ β ≤ ↑r

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.leastPrimeFactorAtLeast_powerCutoff_iff_minFac (N n : ℕ) (β : ℝ) (hn : 2 ≤ n) : LeastPrimeFactorAtLeast (goldbachPowerCutoff N β) n ↔ ↑N ^ β ≤ ↑n.minFac

For actual differences n ≥ 2, the encoded cutoff is exactly the paper's real inequality for the least prime factor P⁻(n).

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.positive_goldbachBasicWeight_structure {zAlpha zTau n : ℕ} (hn : 2 ≤ n) (hw : 0 < goldbachBasicWeight zAlpha zTau n) : Nat.Prime n ∨ ∃ (r : ℕ) (q : ℕ), Nat.Prime r ∧ Nat.Prime q ∧ n = r * q ∧ r < zTau

Every positive weight comes from a prime or a two-prime product with a prime factor strictly below the upper cutoff. Multiplicity is retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasicWeight_le_one (zAlpha zTau n : ℕ) : goldbachBasicWeight zAlpha zTau n ≤ 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.exists_goldbachBasic_growth_cutoff (ε : ℝ) (hε : 0 < ε) : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → 1 < ε * ↑N ∧ (↑N ^ (9 / 19 - ε)) ^ 19 ≤ (ε * ↑N) ^ 9

Uniform scalar absorption. The cutoff depends only on ε, and is chosen before N and the prime variable p. No explicit bound is claimed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.oneNine_power_bound {N n r q : ℕ} {ε : ℝ} (hε : 0 < ε) (hn : ε * ↑N < ↑n) (hscale : (↑N ^ (9 / 19 - ε)) ^ 19 ≤ (ε * ↑N) ^ 9) (hr : 0 < r) (hnprod : n = r * q) (hrcut : r < goldbachPowerCutoff N (9 / 19 - ε)) : r ^ 10 ≤ q ^ 9

The essential 1.9 inequality: the upper-cutoff prime obeys the literal power imbalance after cancellation. Works also when r = q.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasic_pointwise_of_growth {N p : ℕ} {ε α : ℝ} (hε : 0 < ε) (hlarge : 1 < ε * ↑N) (hscale : (↑N ^ (9 / 19 - ε)) ^ 19 ≤ (ε * ↑N) ^ 9) (hp : p ∈ goldbachPrimeCarrier N ε) : goldbachBasicWeight (goldbachPowerCutoff N α) (goldbachPowerCutoff N (9 / 19 - ε)) (N - p) ≤ if IsOnePlusOneNineRepresentation N p then 1 else 0

Pointwise arithmetic producer under explicit scalar bounds. These scalar bounds are discharged uniformly in the eventual theorem below.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasic_eventual_pointwise (ε : ℝ) (hε : 0 < ε) : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (α : ℝ), ∀ p ∈ goldbachPrimeCarrier N ε, goldbachBasicWeight (goldbachPowerCutoff N α) (goldbachPowerCutoff N (9 / 19 - ε)) (N - p) ≤ if IsOnePlusOneNineRepresentation N p then 1 else 0

Genuine pointwise domination, with one cutoff chosen before N, α and p. In fact the first inequality needs no restriction on α: the paper's 0 < α < τ < 1/2 is an immediate specialization.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier (N : ℕ) (ε : ℝ) : Finset ℕ

The literal difference carrier A from equation (4.5).

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N ε = Finset.image (fun (p : ℕ) => N - p) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachPrimeCarrier N ε)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.mem_goldbachPrimeCarrier_iff {N p : ℕ} {ε : ℝ} (hε : 0 ≤ ε) : p ∈ goldbachPrimeCarrier N ε ↔ Nat.Prime p ∧ ↑p < (1 - ε) * ↑N

The redundant finite range does not change the paper's prime cutoff.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachBasic_finite_le_D19 (ε : ℝ) (hε : 0 < ε) : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (α : ℝ), goldbachBasicFiniteRHS (goldbachDifferenceCarrier N ε) (goldbachPowerCutoff N α) (goldbachPowerCutoff N (9 / 19 - ε)) ≤ ↑(D19 N)

The actual finite Goldbachbasic inequality. No pointwise-domination assumption remains: the preceding producer supplies it. The threshold is uniform in α and is an eventual specialization, not the source's effective bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.exists_representation_of_goldbachBasicFiniteRHS_pos (ε : ℝ) (hε : 0 < ε) : ∃ (N0 : ℕ), ∀ (N : ℕ), N0 ≤ N → ∀ (α : ℝ), 0 < goldbachBasicFiniteRHS (goldbachDifferenceCarrier N ε) (goldbachPowerCutoff N α) (goldbachPowerCutoff N (9 / 19 - ε)) → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9

A positive actual Goldbachbasic RHS yields a literal 1+1.9 representation. Only positivity of the four finite counts remains, not a pointwise input.