theorem G12FlexibleWF.residue_linked (N : ℕ) (A : Finset (ℕ × ℕ)) (d : ℕ) : G12OutsideBudget.residue N (Finset.image G12RectangleWF.linkedEmbed A) d = residue N A d

Literal transport of the physical residual, without a new coefficient.

theorem G12FlexibleWF.outside_linked (N : ℕ) (A : Finset (ℕ × ℕ)) (Z Q : ℝ) (c : ℕ → ℝ) : G12OutsideBudget.outside N (Finset.image G12RectangleWF.linkedEmbed A) Z Q c = outsidePrimorial N A Z Q c

noncomputable def G12FlexibleWF.correctionBudget (N : ℕ) (Q η : ℝ) : ℝ

Equations

• G12FlexibleWF.correctionBudget N Q η = 800 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 2 + 20 * ↑N * (4 / MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η ^ η ^ 2) * (1 + Real.log ↑⌊Q⌋₊) ^ 2

theorem G12FlexibleWF.signed_corrections_paid {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (A : Finset (ℕ × ℕ)) (hA : Finset.image G12RectangleWF.linkedEmbed A ⊆ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedAtoms N ε) (Z Q η : ℝ) (hQ : Q ≤ ↑N) (hD : 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) (hη : 0 < η) (hηu : η < 1 / 8) (hf : ∀ t ∈ MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z, MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t) Q) : have S := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z; have c := fun (t : List ℕ) => MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm true (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z) (MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) η Z t; ∑ t ∈ S, (G12FlexibleRectangle.discrepancy N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑(c t) - G12RectangleWF.gate N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑(c t) - outsidePrimorial N A Z Q ⇑(c t)) ≤ ∑ t ∈ S, |G12FlexibleRectangle.discrepancy N A (Finset.Ioc 0 ⌊Q⌋₊) ⇑(c t)| + ↑S.card * correctionBudget N Q η

Both actual corrections are paid on the very same full external family.