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

Dimension depends on the inherited prime product and nu, not on the mother weights.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Linked_upperRosserCertificate {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.goldbachG11LinkedSiftedMass_le_rosserFactor (ρ : ℝ) (hρ : 0 < ρ) : ∃ (z₀ : ℝ), ∀ (N : ℕ) (hEven : Even N) (ε Z Δ s X : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → 0 ≤ X → have S := goldbachG11LinkedBoundingSieve N hEven ε Z X; have P := goldbachB10ProdPrimes N Z; goldbachG11LinkedSiftedMass N ε Z ≤ X * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight P (⌊Δ⌋₊ + 1))

Actual weighted G11 sieve, consuming the already constructed all-depth source. The precise finite remainder is retained for the common-distribution consumer.