theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5_squareMass_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (A : Finset ℕ), (∀ n ∈ A, 1 ≤ n ∧ n < N) → 400 * ↑(goldbachQA A N (↑N ^ (4 / 53))) ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Pay the actual square mass uniformly over finite carriers below N. No primality or squarefreeness of the carrier is assumed.