theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12CommonMass_buchstab_and_distribution (A η : ℝ) (hA : 0 < A) (hη : 0 < η) : ∃ (B : ℝ) (C : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ) (Q : ℕ), ↑Q ≤ √↑N / Real.log ↑N ^ B → 400 * goldbachG12PrimeWindowMainMass N ε ≤ goldbachG12BuchstabUpperMass N η + 8400 * ↑N / ↑N ^ (4 / 53) ∧ ∑ d ∈ goldbachG11LinkedModuli N Q, |goldbachG12CommonDivisorResidual N ε d| ≤ C * ↑N / Real.log ↑N ^ A

The same modulus-independent mass controls the original cross mother and the actual divisor residual.