theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_exceptions_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ∀ (b c : ℝ), ↑(∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) b c, goldbachG11RSquareCount (goldbachDifferenceCarrier N ε) v + ∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) b c, goldbachG11NCount (goldbachDifferenceCarrier N ε) N v) ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Both exceptional counts on the original cross carrier are paid uniformly in both upper endpoints. Only the fixed lower prime exponent is used.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG12_le_roughSum_add_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ∀ (b c : ℝ), ↑(goldbachWeightG12 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) b c) ≤ ↑(∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) b c, goldbachG11RoughCount N ε v) + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Original G12 is bounded by its own rough-quotient sum and an arbitrarily small normalized error. No rough-count or distribution bound is assumed.