theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_prodPrimes_eq (N : ℕ) (hEven : Even N) (ε Z X : ℝ) : (goldbachG12LinkedBoundingSieve N hEven ε Z X).prodPrimes = (goldbachG11LinkedBoundingSieve N hEven ε Z X).prodPrimes

The original Goldbach sieve prime product is unchanged.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_nu_eq (N : ℕ) (hEven : Even N) (ε Z X : ℝ) : (goldbachG12LinkedBoundingSieve N hEven ε Z X).nu = (goldbachG11LinkedBoundingSieve N hEven ε Z X).nu

The entire multiplicative density is unchanged, not just its prime values.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_sieveProduct_eq (N : ℕ) (hEven : Even N) (ε Z X : ℝ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachG12LinkedBoundingSieve N hEven ε Z X) = goldbachB10PrimeProduct N Z

The actual Euler product, with the inherited local factors.

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

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_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.goldbachG12LinkedSiftedMass_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 := goldbachG12LinkedBoundingSieve N hEven ε Z X; have P := goldbachB10ProdPrimes N Z; goldbachG12LinkedSiftedMass N ε Z ≤ X * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight P (⌊Δ⌋₊ + 1))

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