noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PaidRosserEnvelope (N : ℕ) (hEven : Even N) (ε Z s A C ρ : ℝ) : ℝ

Explicit proved Rosser envelope; its common mass is still unnormalized.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PaidRosserEnvelope N hEven ε Z s A C ρ = 400 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass N ε * (MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedBoundingSieve N hEven ε Z (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass N ε)) + 400 * C * ↑N / Real.log ↑N ^ A + 8000 * ↑⌈Z⌉₊

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11PaidBase (N : ℕ) (ε : ℝ) : ℤ

Only the still-unevaluated G11 good count is removed from the previous base.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11PaidBase N ε = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11GoodRemainder N ε + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GoodSwitchedTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_paidRosser (A ρ δ : ℝ) (hA : 0 < A) (hρ : 0 < ρ) (hδ : 0 < δ) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (hEven : Even N) (ε : ℝ), 0 ≤ ε → ∀ (Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → Δ ≤ √↑N / Real.log ↑N ^ B → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ goldbachG11PaidRosserEnvelope N hEven ε Z s A C ρ + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_g11PaidRosser_consumed (A ρ δ : ℝ) (hA : 0 < A) (hρ : 0 < ρ) (hδ : 0 < δ) : ∃ (B : ℝ) (C : ℝ) (z₀ : ℝ), 0 < B ∧ 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (hEven : Even N) (Zlow : ℝ), 1 ≤ Zlow → Zlow ≤ √↑N → ∀ (Z Δ s : ℝ), z₀ ≤ Z → 2 ≤ Z → 0 < Δ → s = Real.log Δ / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → Δ ≤ √↑N / Real.log ↑N ^ B → ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Zlow) + (goldbachWeightHighFirstCoefficient ε - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) - goldbachG11PaidRosserEnvelope N hEven ε Z s A C ρ ≤ 4 * ↑(D19 N)

Actual D19 lower bound with the good G11 count replaced by its paid Rosser expression. The remaining signed base, low term and common-mass normalization remain explicit; no final positivity is asserted.