theorem G12LowRectangle.rectangle_C2_bound (j A : ℕ) {Cscale ζ : ℝ} (hCscale : 1 ≤ Cscale) (hζ : 0 < ζ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T : ℕ), 1 ≤ M → 1 ≤ T → ∀ (ν : ℝ), 4 * ↑M * ↑T = x → ζ ≤ ν → ν ≤ 1 / 10 + ζ / 10 → ↑T = x ^ ν → ∀ (N : ℕ), 0 < N → ↑N ≤ Cscale * x → ∀ (ε : ℝ) (c : ℕ → ℝ), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ζ)) c → |discrepancy N (rectangle N ε M T) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ζ)⌋₊) c| ≤ x / Real.log x ^ A

The actual finite rectangle consumes the proved prime-C2 source. Its unpaid boundary and the later common-family density remain separate obligations.