theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_thirds_le_primePi {N : ℕ} {e ρ : ℝ} (hρ : 1 < ρ) (n s : ℕ) : ↑(∑ k ∈ fouvryG9GridUsed N e ρ, (fouvryG9RectanglePrefixThirds N ρ n s k).card) ≤ LiLiuPrereqBuchstab.primePi (ρ ^ 3 * ↑N / (↑n * ↑s))

Identification with the genuine prime-counting function, including the right endpoint of the prefix.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_uniform_PNT {ζ : ℝ} (hζ : 0 < ζ) : ∃ (Y : ℝ), 3 ≤ Y ∧ ∀ y ≥ Y, ∀ x ≥ y, LiLiuPrereqBuchstab.primePi x ≤ (1 + ζ) * (x / Real.log x)

One PNT threshold works for every later prefix endpoint. This directly consumes the proved error envelope, not a PNT hypothesis.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectanglePrefix_thirds_PNT {ζ : ℝ} (hζ : 0 < ζ) : ∃ (Y : ℝ), 3 ≤ Y ∧ ∀ (N : ℕ) (e ρ : ℝ), 1 < ρ → ∀ (n s : ℕ), Y ≤ ρ ^ 3 * ↑N / (↑n * ↑s) → ↑(∑ k ∈ fouvryG9GridUsed N e ρ, (fouvryG9RectanglePrefixThirds N ρ n s k).card) ≤ (1 + ζ) * (ρ ^ 3 * ↑N / (↑n * ↑s) / Real.log (ρ ^ 3 * ↑N / (↑n * ↑s)))

Genuine finite prefix merging followed by the existing uniform PNT. The sole size condition is on the prefix endpoint, not on each third box.