theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9PrimeOutput_mass_upper : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 1 < K ∧ ∀ (A : ℕ) (e ε δ η ρ : ℝ), 0 < e → e ≤ 1 → 0 < ε → ε < 4 / 53 → ε < δ → δ < 1 / 4 → 0 < η → η < 1 / 8 → 1 < ρ → ρ ≤ 5 / 4 → ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → fouvryG9MotherPrimeOutput N e ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9UpperFactor N (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) C K η * (fouvryG9BaseEuler N √↑N * (1 + 1 / (↑N ^ (4 / 53) / 2 - 2)) ^ 3 * fouvryG9RectangleMass N ρ k) + ↑N / Real.log ↑N ^ A

Original prime-output mother bounded by actual labelled rectangle mass. The small-output correction, actual Euler correction and distribution remainder are proved, rather than supplied as target-shaped hypotheses.