noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum (N : ℕ) (l₁ l₂ : GoldbachG11Label → ℝ) : ℝ

Real differences retain the two original integer rough counts. The endpoints may vary with each original label; no uniformity in e0 at zero.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum N l₁ l₂ = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), (↑(LiLiuPrereqBuchstab.roughCount (l₂ v * (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v))) ↑v.snd.snd.snd) - ↑(LiLiuPrereqBuchstab.roughCount (l₁ v * (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v))) ↑v.snd.snd.snd))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum_le_kernel (e₀ : ℝ) (he₀ : 0 < e₀) (he₁ : e₀ ≤ 1) (w η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (l₁ l₂ : GoldbachG11Label → ℝ), (∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), e₀ ≤ l₁ v ∧ l₁ v ≤ l₂ v ∧ l₂ v ≤ 1 ∧ l₂ v - l₁ v ≤ w) → Real.log ↑N / ↑N * goldbachG12ThinSum N l₁ l₂ ≤ (564383 / 1000000 * w + η) * goldbachG12PrimeKernel (fun (x : ℝ) => 1) N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ThinSum_integral_budget (e₀ : ℝ) (he₀ : 0 < e₀) (he₁ : e₀ ≤ 1) (w : ℝ) (hw : 0 ≤ w) (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (l₁ l₂ : GoldbachG11Label → ℝ), (∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), e₀ ≤ l₁ v ∧ l₁ v ≤ l₂ v ∧ l₂ v ≤ 1 ∧ l₂ v - l₁ v ≤ w) → Real.log ↑N / ↑N * goldbachG12ThinSum N l₁ l₂ ≤ (564383 / 1000000 * w * goldbachG12PrimeIntegral fun (x : ℝ) => 1) + δ

Aggregate thin-window budget at the raw-mother normalization log(N)/N. This consumes both actual Buchstab counts and original cross quadrature. It deliberately asserts neither a second logarithm nor an output-prime bound.