theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachB8PlusBoundingSieve_dimensionOneLocalProductBound : ∃ (K : ℝ), 1 < K ∧ ∀ (N : ℕ) (hEven : Even N) (Z : ℝ), SwitchingPrinciple.HasDimensionOneLocalProductBound (goldbachB8PlusBoundingSieve N hEven Z) K

The local product uses only prime values of the reciprocal-totient density.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_upperRosserWeight_certificate {N : ℕ} {Z Δ s : ℝ} (hZ : 2 ≤ Z) (hΔ : 0 < Δ) (hs : s = Real.log Δ / Real.log Z) (hslo : 3 / 2 ≤ s) : LinearSieve.IsUpperRosserCertificate (goldbachB10ProdPrimes N Z) (⌊Δ⌋₊ + 1)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSiftedCount_le_rosserFactor_add_upperErrSum (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), ∀ (N : ℕ) (hEven : Even N) (Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → have S := goldbachB8PlusBoundingSieve N hEven Z; ↑(goldbachB8PlusSiftedAtoms N Z).card ≤ goldbachB8PlusMainMass N * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1))

The genuine upper factor for the full labelled B8plus count and its fixed mass.