theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_integer_collar_reciprocal {q : ℕ} {ρ : ℝ} (hq : 0 < q) (hρ : 1 ≤ ρ) : ∑ p ∈ Finset.Ioc q ⌊ρ * ↑q⌋₊, 1 / ↑p ≤ ρ - 1

The strict lower integer endpoint avoids an artificial +1 loss in the ordering collar. Dropping primality here is an upper bound, not an identity.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_prime_reciprocal_bounded : ∃ (B : ℝ), 0 < B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ p ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), 1 / ↑p ≤ B

Reuse Mertens' fixed logarithmic-window limit. The slightly wider lower exponent includes the original closed endpoint without changing the main term.