theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_authorIntegral_direct (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (561522 / 1000000 * goldbachG11PrimeIntegral goldbachG11AuthorWeight + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual author-weight producer. Both distribution branches, sieve families, Euler factors, original labels, expanded endpoints and all exceptional pieces are discharged; only the fixed original parameters remain.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_le_authorScalar_direct (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (10191 / 100000 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The existing certified author integral is consumed, not recomputed.