theorem G12FlexibleRectangle.rectangle_C2_input (N : ℕ) (ε : ℝ) (M U T V : ℕ) (hT : 1 ≤ T) (hTV : T ≤ V) (hV : V ≤ 2 * T) (Q : Finset ℕ) (c : ℕ → ℝ) : discrepancy N (rectangle N ε M U T V) Q c = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.signedError (Finset.Ioc M U) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval (shortInterval T V hT hTV hV).lower (shortInterval T V hT hTV hV).upper) Q (alpha N ε T V) (fun (r : ℕ) => if r.Coprime N then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta r else 0) c ↑N

The physical rectangle is the exact C2 input with unchanged source scale T.

theorem G12FlexibleRectangle.rectangle_C2_bound (j A : ℕ) {Cscale ζ : ℝ} (hCscale : 1 ≤ Cscale) (hζ : 0 < ζ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M U T V : ℕ), 1 ≤ M → M ≤ U → U ≤ 2 * M → 1 ≤ T → T ≤ V → V ≤ 2 * 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 U T V) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ζ)⌋₊) c| ≤ x / Real.log x ^ A

Uniform threshold precedes every endpoint, the physical epsilon and c. There is no lower bound on either cell width. The boundary is not estimated.