@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableB10PanDistribution (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableB10PanDistribution P = Classical.propDecidable P

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10PanPrefixRemainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε γ : ℝ), 0 < ε → ε < 1 → γ < 1 / 3 → ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (β : ℝ), 1 / 18 < β → ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N (B + 1)) with d.Coprime N, |goldbachB10PanPrefixRemainder N d (LiuWeight.liuPanSourceIntervalLower N B) (B10PanGeometryUpperWindow N γ) ε (↑N ^ β) (↑N ^ γ)| ≤ C * ↑N / Real.log ↑N ^ U

Actual B10 divisor remainder at half level with a logarithmic loss. All analytic and geometric inputs are supplied. The threshold is uniform in beta, while epsilon and gamma are fixed before the threshold. The main term retains its coprimality gate and the literal floor endpoint.