theorem G12FlexibleWF.corrections_log_saving (B : ℕ) {η σ : ℝ} (hη : 0 < η) (hηu : η < 1 / 8) (hσ : 0 < σ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (ε : ℝ) (A : Finset (ℕ × ℕ)), Finset.image G12RectangleWF.linkedEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε → ∀ (Z Q : ℝ), ↑N ^ σ ≤ Q → Q ≤ ↑N → 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η → (400 * ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z, have c := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t; |G12RectangleWF.gate N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑c| + |outsidePrimorial N A Z Q ⇑c|) ≤ ↑N / Real.log ↑N ^ B

The complete actual family, including the original factor 400, has arbitrary logarithmic saving. The cutoff precedes all submothers and all level/cutoff choices.