theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachD19_author_actual_lower_of_remaining (r : ℝ) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (r - 10191 / 100000 - 661251229 / 200000000 - δ) / 4 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(D19 N)

Consume the new actual G11 producer in the existing signed ledger. Only the independently owned literal remaining-count estimate is still a premise.