Exact Goldbach product bridge in Liu's normalization

The finite identity in MertensTheorem.sieveProduct_identity keeps the strict prime cutoff and cancels precisely the factors at primes dividing N. For even N, removing the local factor at 2 gives twice Liu's odd-prime truncation (Liu, main.tex, lines 98--102; see LiuSingularSeries).

We use this identity before estimating the prime product. Multiplication by the positive logarithm pays one denominator once, and the resulting two-sided bound is shared by the S1 lower and B10 upper estimates. No infinite-series approximation is made here: each consumer separately controls the difference between the actual finite truncation and the full Liu singular series.

theorem MathlibNt.SieveTheory.GoldbachLiuProductBridge.product_eq_two_mul_liuTruncated (N Z : ℕ) (hZ : 3 ≤ Z) (hEven : Even N) : MertensTheorem.goldbachSieveProduct N Z = 2 * SingularSeries.liuSingularSeriesTruncated N (Z - 1) * MertensTheorem.primeProduct (Z - 1)

Exact finite product, including the factor at 2 and the strict cutoff.

theorem MathlibNt.SieveTheory.GoldbachLiuProductBridge.product_nonneg {N Z : ℕ} (hEven : Even N) : 0 ≤ MertensTheorem.goldbachSieveProduct N Z

Nonnegativity also holds below the analytic cutoff; evenness excludes 2 from the nondivisor product.

theorem MathlibNt.SieveTheory.GoldbachLiuProductBridge.exists_log_bounds : ∃ (C : ℝ), ∀ (N Z : ℕ), 3 ≤ Z → Even N → 4 ≤ N → 2 * SingularSeries.liuSingularSeriesTruncated N (Z - 1) * (Real.exp (-Real.eulerMascheroniConstant) - |C| / Real.log ↑(Z - 1)) ≤ MertensTheorem.goldbachSieveProduct N Z * Real.log ↑(Z - 1) ∧ MertensTheorem.goldbachSieveProduct N Z * Real.log ↑(Z - 1) ≤ 2 * SingularSeries.liuSingularSeriesTruncated N (Z - 1) * (Real.exp (-Real.eulerMascheroniConstant) + |C| / Real.log ↑(Z - 1))

Mertens' frozen prime-product estimate, transferred through the exact finite identity. The same constant and both signs serve the two consumers; the old quantitative domain N ≥ 4, even N, Z ≥ 3 is retained.