theorem G12OutsideBudget.scalar_log_saving (B : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℝ) in Filter.atTop, 2 ≤ n ∧ 80 * (1 + Real.log n) ^ 2 / n ^ δ ≤ 1 / Real.log n ^ B

A fixed positive power absorbs the entire numerical transport constant.

theorem G12OutsideBudget.denominator_lower {n Q η σ : ℝ} (hn : 0 ≤ n) (hη : 0 < η) (hηsmall : η < 1 / 8) (hQ : n ^ σ ≤ Q) : n ^ (σ * ((1 + η + η ^ 9)⁻¹ * η ^ 2)) ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η ^ η ^ 2

The external denominator has a fixed positive power at every Q >= N^sigma.

theorem G12OutsideBudget.family_log_saving (B : ℕ) {η σ : ℝ} (hη : 0 < η) (hηsmall : η < 1 / 8) (hσ : 0 < σ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (ε : ℝ), ∀ A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε, ∀ (Z Q : ℝ), ↑N ^ σ ≤ Q → Q ≤ ↑N → 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η → ∑ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z, |outside N A Z Q ⇑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t)| ≤ ↑(MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z).card * ↑N / Real.log ↑N ^ B

The threshold precedes every submother, epsilon, cutoff and actual family. The tag cardinality is retained rather than assumed bounded.