theorem G12RectangleGate.numerical_log_saving (U : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, 800 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 2 ≤ ↑N / Real.log ↑N ^ U

The cutoff depends only on the requested logarithmic saving.

theorem G12RectangleGate.gate_log_saving (U : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (A : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ), linkEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε → Q ⊆ Finset.Icc 1 N → (∀ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, |c d| ≤ 1) → |G12RectangleWF.gate N A Q c| ≤ ↑N / Real.log ↑N ^ U

Uniform in the atom subset, window, modulus carrier and full signed coefficient.

theorem G12RectangleGate.gate_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (A : Finset (ℕ × ℕ)) (Q : Finset ℕ) (c : ℕ → ℝ), linkEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε → Q ⊆ Finset.Icc 1 N → (∀ d ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q ↑N, |c d| ≤ 1) → 400 * |G12RectangleWF.gate N A Q c| ≤ δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Original body multiplicity 400 is included in the actual singular-series scale.

theorem G12RectangleGate.real_interval_subset {N : ℕ} {Q : ℝ} (hQ : Q ≤ ↑N) : Finset.Ioc 0 ⌊Q⌋₊ ⊆ Finset.Icc 1 N

Full real-level interval: no primorial or squarefree mask is introduced.

theorem G12RectangleGate.gate_wellFactorable {N : ℕ} {ε Q : ℝ} {A : Finset (ℕ × ℕ)} {f : ArithmeticFunction ℝ} (hN : 2 ≤ N) (hQ : Q ≤ ↑N) (hA : linkEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (hf : MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q) : |G12RectangleWF.gate N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑f| ≤ 800 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 2

WF1 is used only for its coefficient bound, at the absolute-gate payment step.

theorem G12RectangleGate.rectangle_gate_le {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (M T : ℕ) (hlow : ↑N ^ (4 / 53) ≤ ↑T) (hhigh : ↑(2 * T) < ↑N ^ (1 / 10)) {Q : ℝ} (hQ : Q ≤ ↑N) {f : ArithmeticFunction ℝ} (hf : MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q) : |G12RectangleWF.gate N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑f| ≤ 800 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 2

Literal original rectangle, under its already-proved inclusion geometry.

theorem G12RectangleGate.rectangle_gate_log_saving (U : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (M T : ℕ), ↑N ^ (4 / 53) ≤ ↑T → ↑(2 * T) < ↑N ^ (1 / 10) → ∀ (Q : ℝ) (f : ArithmeticFunction ℝ), Q ≤ ↑N → MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q → |G12RectangleWF.gate N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑f| ≤ ↑N / Real.log ↑N ^ U

Fixed logarithmic saving for the actual full real-level rectangle gate.

theorem G12RectangleGate.rectangle_gate_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ε : ℝ) (M T : ℕ), ↑N ^ (4 / 53) ≤ ↑T → ↑(2 * T) < ↑N ^ (1 / 10) → ∀ (Q : ℝ) (f : ArithmeticFunction ℝ), Q ≤ ↑N → MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q → 400 * |G12RectangleWF.gate N (G12LowRectangle.rectangle N ε M T) (Finset.Ioc 0 ⌊Q⌋₊) ⇑f| ≤ δ * (MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The normalization cutoff is selected before every changing rectangle and WF member.