theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_positivePair_normalized_lower (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ((1 - ε) * Real.exp (-Real.eulerMascheroniConstant) * (159 / 2 * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor 6 + 33 / 2 * SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (33 / 8)) - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(3 * goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) + goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 33)))

The two actual S1 positive terms in the signed weight, with their genuine multiplicities and a single arbitrary error budget. This is not a Base bound.