theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSmallMass_subpower : ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 1 ≤ ↑N → ∀ (U V : Finset ℕ) (z : ℝ), 0 ≤ z → z ≤ √↑N → goldbachG11RectangleSmallMass N U V z ≤ C * ↑N ^ (1 - 1 / 4)

Original G11 weighted small outputs, including zero, have a fixed subpower bound on every finite rectangle. No label-injectivity or rectangle-volume premise.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_small_outputs_paid (A : ℕ) {ρ : ℝ} (hρ : 1 < ρ) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ε : ℝ) (z : ℕ × ℕ → ℝ), (∀ k ∈ goldbachG11GridUsed N ε ρ, 0 ≤ z k ∧ z k ≤ √↑N) → ∑ k ∈ goldbachG11GridUsed N ε ρ, goldbachG11RectangleSmallMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) (z k) ≤ ↑N / Real.log ↑N ^ A

The entire actual G11 grid pays small outputs. The threshold precedes all epsilon values and all changing per-cell square-root-window cutoffs.