theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedPrefix_mass_fibres {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 = ∑ rs ∈ fouvryG9RelaxedPairs N ρ, ↑(fouvryG9RectanglePrefixThirds N ρ rs.1 rs.2 k).card

Exact pair-fibre decomposition of the actual rectangle mass.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9WeightedPrefix_le_primePi {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : ∀ k ∈ fouvryG9GridUsed N e ρ, 3 ≤ ρ ^ k.1) (W : ℕ × ℕ × ℕ → ℝ) (V : ℕ → ℝ) (hV : ∀ rs ∈ fouvryG9RelaxedPairs N ρ, 0 ≤ V rs.1) (hWV : ∀ k ∈ fouvryG9GridUsed N e ρ, ∀ n ∈ fouvryG9LongShortLabels N ρ k, W k ≤ V n) : ∑ k ∈ fouvryG9GridUsed N e ρ, W k * fouvryG9RectangleMass N ρ k ≤ ∑ rs ∈ fouvryG9RelaxedPairs N ρ, V rs.1 * LiLiuPrereqBuchstab.primePi (ρ ^ 3 * ↑N / (↑rs.1 * ↑rs.2))

Signed cell weights are transported locally to a nonnegative pair weight. The occupied third-label families are paid by one prime prefix per pair.