noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridKey (ρ : ℝ) (v : ℕ × ℕ) : ℕ × ℕ

The first coordinate is the short-prime cell, the second the long-product cell.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridKey ρ v = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridIndex ρ ↑v.2, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridIndex ρ ↑v.1)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed (N : ℕ) (ε ρ : ℝ) : Finset (ℕ × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed N ε ρ = Finset.image (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridKey ρ) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeProductAtoms N ε)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong (N : ℕ) (ε ρ : ℝ) (k : ℕ × ℕ) : Finset ℕ

Long coefficient support uses only geometry and roughness, never output primality.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong N ε ρ k = {m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε | ρ ^ k.2 ≤ ↑m ∧ ↑m < ρ ^ (k.2 + 1) ∧ ρ ^ k.1 ≤ ↑m.minFac}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ) : Finset ℕ

Exact integer encoding of the short half-open cell, clipped at the original lower cutoff.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort N ρ k = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (↑⌈max (ρ ^ k.1) (↑N ^ (4 / 53))⌉ - 1) (↑⌈ρ ^ (k.1 + 1)⌉ - 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed_witness {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) : ∃ (m : ℕ) (p : ℕ), m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ p ∈ goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m ∧ ρ ^ k.1 ≤ ↑p ∧ ↑p < ρ ^ (k.1 + 1) ∧ ρ ^ k.2 ≤ ↑m ∧ ↑m < ρ ^ (k.2 + 1)

Actual occupied atoms supply both logarithmic cells and their original strict window.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed_short_gates {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) : 3 ≤ ρ ^ k.1 ∧ max (ρ ^ k.1) (↑N ^ (4 / 53)) ≤ ρ ^ (k.1 + 1) ∧ ρ ^ (k.1 + 1) ≤ 4 / 3 * ρ ^ k.1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPrimeInterval {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) (k : ℕ × ℕ) (hk : k ∈ goldbachG11GridUsed N ε ρ) : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPrimeInterval hρ hρu hbig k hk = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.g9PrimeHalfOpenInterval (ρ ^ k.1) (max (ρ ^ k.1) (↑N ^ (4 / 53))) (ρ ^ (k.1 + 1)) ⋯ ⋯ ⋯ ⋯

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridShort_mem_iff {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) (p : ℕ) : p ∈ goldbachG11GridShort N ρ k ↔ max (ρ ^ k.1) (↑N ^ (4 / 53)) ≤ ↑p ∧ ↑p < ρ ^ (k.1 + 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_actual_grid_cover {N : ℕ} {ε ρ : ℝ} (hN : 2 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {m p : ℕ} (hm : m ∈ goldbachG11ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hpF : p ∈ goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m) : ∃ k ∈ goldbachG11GridUsed N ε ρ, m ∈ goldbachG11GridLong N ε ρ k ∧ p ∈ goldbachG11GridShort N ρ k

Every actual prime/product atom, including closed arithmetic boundaries, is covered.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal_le_actual_grid {N : ℕ} {ε ρ : ℝ} (hN : 2 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) : ↑(goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ ∑ k ∈ goldbachG11GridUsed N ε ρ, goldbachG11RectanglePrimeMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k)

The coverage premise is now supplied for the original good G11 count.