noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPhysicalScale (ρ : ℝ) (k : ℕ × ℕ) : ℝ

The physical rectangle scale includes the existing two-thirds endpoint buffer.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPhysicalScale ρ k = 4 * ρ ^ k.2 * (2 / 3 * ρ ^ k.1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridLong_rectangle {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ) {m : ℕ} (hm : m ∈ goldbachG11GridLong N ε ρ k) : ρ ^ k.2 ≤ ↑m ∧ ↑m ≤ 2 * ρ ^ k.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPhysicalScale_window {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) : ε * ↑N < goldbachG11GridPhysicalScale ρ k ∧ goldbachG11GridPhysicalScale ρ k ≤ 4 * ↑N

The strict prefix and an occupied atom give the real physical x-window. It is not legal to replace x by N inside the distribution theorem.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridPhysicalScale_shift {N : ℕ} {ε ρ : ℝ} (hε : 0 < ε) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) : ↑N ≤ 1 / ε * goldbachG11GridPhysicalScale ρ k

Fixed positive epsilon supplies the fixed shift multiplier for the physical scale.

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

Before any later cell, the short distribution scale stays above a fixed power of N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridUsed_card {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) : (goldbachG11GridUsed N ε ρ).card ≤ (fouvryG9GridIndex ρ ↑N + 1) ^ 2

The actual occupied two-dimensional grid has quadratic logarithmic cost.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_pair_product_bound {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) {m p : ℕ} (hm : m ∈ goldbachG11GridLong N ε ρ k) (hp : p ∈ goldbachG11GridShort N ρ k) : m * p ≤ 4 * N

Any overhanging pair in an occupied rectangle remains below 4N.