theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12OutputTotal_le_paidRosser_actualEuler (A ρ : ℝ) (hA : 0 < A) (hρ : 0 < ρ) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, 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 → 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ 400 * goldbachG12PrimeWindowMainMass N ε * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * goldbachB10PrimeProduct N Z + 400 * C * ↑N / Real.log ↑N ^ A + 8000 * ↑⌈Z⌉₊

Paid upper sieve for the literal original G12 output-prime fibres. All constants and thresholds precede epsilon, the sieve cutoff and its level. The Euler product is the actual inherited Goldbach product, not an asymptotic surrogate.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal_le_paidRosser_actualEuler (A ρ : ℝ) (hA : 0 < A) (hρ : 0 < ρ) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, 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 → ↑(goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) ≤ 400 * goldbachG12PrimeWindowMainMass N ε * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * goldbachB10PrimeProduct N Z + 400 * C * ↑N / Real.log ↑N ^ A + 8000 * ↑⌈Z⌉₊

Equivalent endpoint in the original integer product count; no G11 large-domain count is substituted for the G12 mother.