theorem G12MovingEuler.error_eventually (K C t : ℝ) (hC : 0 < C) (ht : 0 < t) : ∃ (η : ℝ), 0 < η ∧ η < 1 / 8 ∧ ∀ᶠ (Q : ℝ) in Filter.atTop, C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))) ≤ t * Real.exp Real.eulerMascheroniConstant

The genuine fixed-parameter JR error can be made small, before Q varies.

theorem G12MovingEuler.geometry (L : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (Q : ℝ), ↑N ^ (1 / 3) ≤ Q → Q ≤ ↑N → L ≤ Q ∧ 4 ≤ Q ∧ 0 < Real.log ↑N ∧ 0 < Real.log Q ∧ Real.log ↑N / 3 ≤ Real.log Q ∧ 4 * Real.log ↑N / Real.log Q ≤ 12

A single ambient threshold admits every moving Q in the stated range.

theorem G12MovingEuler.euler_eq (N : ℕ) (Z : ℝ) : ∏ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z, (1 - AnalyticNumberTheory.Sieve.goldbachNu p) = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct N Z

Identify exactly the strict prime product used by the physical sieve.

theorem G12MovingEuler.euler_nonneg (N : ℕ) (Z : ℝ) : 0 ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PrimeProduct N Z

Nonnegativity is proved on the actual prime carrier, including p=2.

theorem G12MovingEuler.normalized (K C τ : ℝ) (_hK : 1 < K) (hC : 0 < C) (hτ : 0 < τ) : ∃ (η : ℝ), 0 < η ∧ η < 1 / 8 ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (Q : ℝ), ↑N ^ (1 / 3) ≤ Q → Q ≤ ↑N → have Z := √Q; have Euler := ∏ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z, (1 - AnalyticNumberTheory.Sieve.goldbachNu p); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); 2 ≤ Z ∧ Euler * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) ≤ (4 * Real.log ↑N / Real.log Q + τ) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N / Real.log ↑N

Genuine moving-Q Euler/JR normalization. No error-smallness premise and no geometric-scale choice is hidden in the interface. The cutoff precedes N and Q.