theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_mass_labels (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) : fouvryG9RectangleMass N ρ k = ∑ n ∈ fouvryG9RectanglePrimeSupport N ρ k, ∑ _z ∈ fouvryG9LongLabels N ρ k, fouvryG9RectangleBeta N n

Expanding the actual mass retains every ordered long label, including multiplicities of equal products. No coprimality is imposed on the third prime.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_index_unique {ρ x : ℝ} (hρ : 1 < ρ) {i j : ℕ} (hi : ρ ^ i ≤ x ∧ x < ρ ^ (i + 1)) (hj : ρ ^ j ≤ x ∧ x < ρ ^ (j + 1)) : i = j

Half-open geometric intervals have unique natural indices.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_mass_eq_card {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (k : ℕ × ℕ × ℕ) (hbig : 3 ≤ ρ ^ k.1) (hne : (fouvryG9GridCell N e ρ k).Nonempty) : fouvryG9RectangleMass N ρ k = ↑(fouvryG9LongShortLabels N ρ k ×ˢ fouvryG9LongLabels N ρ k).card

The actual weighted mass is exactly the number of ordered rectangle labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_label_unique {N : ℕ} {ρ : ℝ} (hρ : 1 < ρ) {k k' : ℕ × ℕ × ℕ} {n : ℕ} {z : ℕ × ℕ} (hn : n ∈ fouvryG9LongShortLabels N ρ k) (hz : z ∈ fouvryG9LongLabels N ρ k) (hn' : n ∈ fouvryG9LongShortLabels N ρ k') (hz' : z ∈ fouvryG9LongLabels N ρ k') : k = k'

A labelled triple can occur in at most one rectangle. This prevents counting the same third-prime prefix once per occupied cell.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_enlarged_geometry {N : ℕ} {e ρ : ℝ} (hρ : 1 < ρ) {k : ℕ × ℕ × ℕ} (hne : (fouvryG9GridCell N e ρ k).Nonempty) {n : ℕ} {z : ℕ × ℕ} (hn : n ∈ fouvryG9LongShortLabels N ρ k) (hz : z ∈ fouvryG9LongLabels N ρ k) : ↑n * ↑z.1 * ↑z.2 < ρ ^ 3 * ↑N ∧ ↑n * ↑z.1 ^ 2 ≤ ρ ^ 3 * ↑N

Occupancy enlarges both curved bounds by rho cubed. In particular the original pair curve is NOT imposed on the enlarged rectangle.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_pair_and_prefix {N : ℕ} {e ρ : ℝ} (hρ : 1 < ρ) {k : ℕ × ℕ × ℕ} (hne : (fouvryG9GridCell N e ρ k).Nonempty) {n : ℕ} {z : ℕ × ℕ} (hn : n ∈ fouvryG9LongShortLabels N ρ k) (hz : z ∈ fouvryG9LongLabels N ρ k) : (n, z.1) ∈ fouvryG9RelaxedPairs N ρ ∧ Nat.Prime z.2 ∧ ↑z.2 ≤ ρ ^ 3 * ↑N / (↑n * ↑z.1) ∧ ↑z.1 ≤ ρ ^ 3 * ↑N / (↑n * ↑z.1)

Every occupied rectangular label lands in the parent's exact relaxed pair carrier and in one true prime prefix.

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

The third-prime labels in an occupied rectangle, with the first two labels fixed. Keeping the cell index until the injection proves no duplication.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefixThirds N ρ n s k = {t ∈ Finset.range (N + 1) | n ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongShortLabels N ρ k ∧ (s, t) ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9LongLabels N ρ k}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_thirds_sum_le {N : ℕ} {e ρ : ℝ} (hρ : 1 < ρ) (n s : ℕ) : ∑ k ∈ fouvryG9GridUsed N e ρ, (fouvryG9RectanglePrefixThirds N ρ n s k).card ≤ (Finset.filter Nat.Prime (Finset.range (⌊ρ ^ 3 * ↑N / (↑n * ↑s)⌋₊ + 1))).card

All occupied third boxes merge into ONE prime prefix, not one prefix per cell. This is a finite injection and uses no prime-number theorem.