theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11NormalizedProductCoefficient_le_tau_two (N m : ℕ) : 0 ≤ goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m ∧ goldbachG11NormalizedProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m ≤ ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 2) m)

Reuse the stronger order-one bound; this weaker order-two form fits the already proved arbitrary weighted-fibre interface, including m=0.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Rectangle_natAbs_fibre_le (N r : ℕ) (U V : Finset ℕ) : (∑ v ∈ U ×ˢ V, if (↑N - ↑v.1 * ↑v.2).natAbs = r then goldbachG11RectangleWeight N v else 0) ≤ 400 * (↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 3) (N + r)) + ↑((AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau 3) (N - r)))

Original labelled G11 multiplicities on the absolute-difference fibre. Repeated factors, the zero output, and the overhanging negative side all remain.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Rectangle_fibres_subpower {κ : ℝ} (hκ : 0 < κ) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ (N : ℕ) (U V : Finset ℕ), ∀ r ≤ 4 * N, (∑ v ∈ U ×ˢ V, if (↑N - ↑v.1 * ↑v.2).natAbs = r then goldbachG11RectangleWeight N v else 0) ≤ 800 * C₀ * (5 * ↑N) ^ κ

Fixed subpower fibre bound, uniform over all finite rectangles of original G11 weights.