theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedBoundingSieve_rem_eq_common (N : ℕ) (hEven : Even N) (ε Z : ℝ) {d : ℕ} (hd : d ∣ goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = goldbachG12CommonDivisorResidual N ε d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Linked_upperErrSum_le (N : ℕ) (hEven : Even N) (ε Z : ℝ) (D Q : ℕ) (hDQ : D ≤ Q + 1) : have S := goldbachG12LinkedBoundingSieve N hEven ε Z (goldbachG12PrimeWindowMainMass N ε); have P := goldbachB10ProdPrimes N Z; LinearSieve.upperErrSum S D (LinearSieve.upperRosserWeight P D) ≤ ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG12CommonDivisorResidual N ε d|

True Rosser divisors embed into the proved squarefree coprime carrier, including d=1. No full-modulus removal of the squarefree condition is used.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12OutputTotal_le_paidRosser (A ρ : ℝ) (hA : 0 < A) (hρ : 0 < ρ) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (hEven : Even N) (ε Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → Δ ≤ √↑N / Real.log ↑N ^ B → have X := goldbachG12PrimeWindowMainMass N ε; have S := goldbachG12LinkedBoundingSieve N hEven ε Z X; 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ 400 * X * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + 400 * C * ↑N / Real.log ↑N ^ A + 8000 * ↑⌈Z⌉₊

The original G12 physical output fibres with their genuine common prime-window mass, proved Rosser factor and paid distribution error. Main-mass normalization and small-output asymptotic absorption are deliberately not claimed here.