theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPair_ideal_term_normalized (B ρ : ℝ) (hB : 0 ≤ B) (hρ : 0 < ρ) (hρK : ρ < 53 / (2 * Real.exp Real.eulerMascheroniConstant)) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (m : ℕ), 0 < m → ↑m ≤ ↑N ^ (13 / 33) → have S := goldbachS3BoundingSieve N hEven ε (↑N ^ (4 / 53)) m; have D := LiuWeight.panModulusCutoff N B / m + 1; (53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) * goldbachPairIdealWeight N (2 * ρ) m ≤ S.totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S * max 0 (JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log ↑D / Real.log (↑N ^ (4 / 53))) - ρ)

Scalar normalization and coordinate transport on the same composite atom.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPair_ideal_sum_normalized (B ρ : ℝ) (hB : 0 ≤ B) (hρ : 0 < ρ) (hρK : ρ < 53 / (2 * Real.exp Real.eulerMascheroniConstant)) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (T : Finset (ℕ × ℕ)), (∀ a ∈ T, 0 < a.1 * a.2 ∧ ↑(a.1 * a.2) ≤ ↑N ^ (13 / 33)) → (53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) * goldbachPairIdealSum N (2 * ρ) T ≤ goldbachPairMovingMain N hEven ε B ρ T

The threshold is shared by every finite family of admissible products.