theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Grid_short_endpoints {N : ℕ} {e ρ : ℝ} (hρ : 1 < ρ) {k : ℕ × ℕ × ℕ} (hne : (fouvryG9GridCell N e ρ k).Nonempty) : max (ρ ^ k.1) (↑N ^ (4 / 53)) ≤ min (ρ ^ (k.1 + 1)) (↑N ^ (1 / 10))

The endpoints of an occupied cell have a genuine interval between them.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridPrimeInterval {N : ℕ} {e ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) : AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval

The actual short-coordinate geometry, with exact integer endpoint encoding.

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongShortLabels_eq_interval {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) : have z := fouvryG9GridPrimeInterval hρ hρu k hbig hne; fouvryG9LongShortLabels N ρ k = {n ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval z.lower z.upper | Nat.Prime n ∧ n.Coprime N}

The finite short-label set equals the interval filtered by the two literal arithmetic conditions. There is no condition on the third prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongShortLabels_sum_interval {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) (F : ℕ → ℝ) : have z := fouvryG9GridPrimeInterval hρ hρu k hbig hne; ∑ n ∈ fouvryG9LongShortLabels N ρ k, F n = ∑ n ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval z.lower z.upper, (if n.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0) * F n

An arbitrary signed finite kernel is transferred exactly to the existing prime/copN coefficient, not merely bounded by it.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Long_cell_le_prime_rectangle {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) (F : ℕ → ℕ → ℝ) (hF : ∀ (n m : ℕ), 0 ≤ F n m) : have z := fouvryG9GridPrimeInterval hρ hρu k hbig hne; ∑ y ∈ fouvryG9GridCell N e ρ k, F y.2.2 y.1 ≤ ∑ m ∈ fouvryG9LongProducts N ρ k, ∑ n ∈ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval z.lower z.upper, (fouvryG9LongAlpha N ρ k m * if n.Coprime N then AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta n else 0) * F n m

Positive enlargement now lands in the literal prime interval coefficient accepted by expanded C2, with the actual long multiplicity unchanged.