theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedPairPrefix_PNT {ζ : ℝ} (hζ : 0 < ζ) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ρ δ : ℝ), 1 < ρ → δ < 1 / 4 → ∑ rs ∈ fouvryG9RelaxedPairs N ρ, fouvryG9FirstWeight N δ rs.1 * LiLiuPrereqBuchstab.primePi (ρ ^ 3 * ↑N / (↑rs.1 * ↑rs.2)) ≤ (1 + ζ) * ρ ^ 3 * ↑N / Real.log ↑N ^ 2 * fouvryG9RelaxedPairKernel N ρ δ

Uniform prefix PNT and the exact logarithmic algebra assemble the genuine relaxed kernel. No estimate is imposed on each individual third-prime box.