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

A cell is the exact fibre inside the actual carrier, not an enlarged prefix.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell N eps ρ k = {y ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Carrier N eps | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridKey ρ y = k}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_mem_iff {N : ℕ} {eps ρ : ℝ} {k y : ℕ × ℕ × ℕ} : y ∈ fouvryG9GridCell N eps ρ k ↔ y ∈ fouvryG9Carrier N eps ∧ fouvryG9GridKey ρ y = k

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_nonempty_iff {N : ℕ} {eps ρ : ℝ} {k : ℕ × ℕ × ℕ} : (fouvryG9GridCell N eps ρ k).Nonempty ↔ k ∈ fouvryG9GridUsed N eps ρ

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_rectangle {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) {k y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9GridCell N eps ρ k) : ρ ^ k.1 ≤ ↑y.2.2 ∧ ↑y.2.2 < ρ * ρ ^ k.1 ∧ ρ ^ (k.2.1 + k.2.2) ≤ ↑y.1 ∧ ↑y.1 < ρ ^ 2 * ρ ^ (k.2.1 + k.2.2)

Rectangular geometry uses both separate long-coordinate prime labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_long_le_two {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k y : ℕ × ℕ × ℕ} (hy : y ∈ fouvryG9GridCell N eps ρ k) : ↑y.1 ≤ 2 * ρ ^ (k.2.1 + k.2.2)

With the small mesh, the long-coordinate interval lies in [M,2M].

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_scale_window {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ × ℕ} (hne : (fouvryG9GridCell N eps ρ k).Nonempty) : eps * ↑N < 4 * ρ ^ (k.2.1 + k.2.2) * ρ ^ k.1 ∧ 4 * ρ ^ (k.2.1 + k.2.2) * ρ ^ k.1 ≤ 4 * ↑N

A genuine occupied-cell witness supplies the scale window; no error estimate is claimed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_sum (N : ℕ) (eps ρ : ℝ) (F : ℕ × ℕ × ℕ → ℝ) : ∑ k ∈ fouvryG9GridUsed N eps ρ, ∑ y ∈ fouvryG9GridCell N eps ρ k, F y = ∑ y ∈ fouvryG9Carrier N eps, F y

Exact partition of the carrier sum into its occupied grid cells.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCell_card_sum (N : ℕ) (eps ρ : ℝ) : ∑ k ∈ fouvryG9GridUsed N eps ρ, (fouvryG9GridCell N eps ρ k).card = (fouvryG9Carrier N eps).card

Exact positive counting partition; no carrier point is lost or merged.