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

A finite short-coordinate cover with literal real endpoints. No rounding or analytic interval adapter is built into this definition.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongShortLabels N ρ k = {n ∈ Finset.range (N + 1) | Nat.Prime n ∧ n.Coprime N ∧ ↑N ^ (4 / 53) ≤ ↑n ∧ ↑n < ↑N ^ (1 / 10) ∧ ρ ^ k.1 ≤ ↑n ∧ ↑n < ρ ^ (k.1 + 1)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongShortLabels_of_cell {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) {k y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9GridCell N eps ρ k) : y.2.2 ∈ fouvryG9LongShortLabels N ρ k

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongRectCoordinates (y : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ

The actual cell embeds into the rectangular label product without merging ordered prime labels. This map is used only for positive enlargement.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongRectCoordinates y = (y.2.2, y.2.1, y.1 / y.2.1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongRectCoordinates_injOn (N : ℕ) (eps ρ : ℝ) (k : ℕ × ℕ × ℕ) : Set.InjOn fouvryG9LongRectCoordinates ↑(fouvryG9GridCell N eps ρ k)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongRectCoordinates_subset {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) (k : ℕ × ℕ × ℕ) : Finset.image fouvryG9LongRectCoordinates (fouvryG9GridCell N eps ρ k) ⊆ fouvryG9LongShortLabels N ρ k ×ˢ fouvryG9LongLabels N ρ k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Long_cell_le_label_rectangle {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) (k : ℕ × ℕ × ℕ) (F : ℕ → ℕ → ℝ) (hF : ∀ (n m : ℕ), 0 ≤ F n m) : ∑ y ∈ fouvryG9GridCell N eps ρ k, F y.2.2 y.1 ≤ ∑ n ∈ fouvryG9LongShortLabels N ρ k, ∑ z ∈ fouvryG9LongLabels N ρ k, F n (z.1 * z.2)

Positive cell enlargement, not a bound for a signed curved-cell error.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Long_cell_le_weighted_rectangle {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) (k : ℕ × ℕ × ℕ) (F : ℕ → ℕ → ℝ) (hF : ∀ (n m : ℕ), 0 ≤ F n m) : ∑ y ∈ fouvryG9GridCell N eps ρ k, F y.2.2 y.1 ≤ ∑ n ∈ fouvryG9LongShortLabels N ρ k, ∑ m ∈ fouvryG9LongProducts N ρ k, fouvryG9LongAlpha N ρ k m * F n m

Positive rectangular domination with a genuinely short-independent long coefficient. The exact regrouping retains the original s multiplicity.