theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Collar_reciprocal_bound (N : ℕ) {ρ : ℝ} (hρ : 1 ≤ ρ) : ∑ v ∈ goldbachG11CollarBoxes N ρ, 1 / ↑(goldbachG11SwitchedBodyProd v) ≤ (ρ - 1) * (∑ p ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), 1 / ↑p) ^ 3

One integer reciprocal strip and three original prime reciprocal sums. No factorial, distinctness, or unproved short-prime distribution is used.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Collar_rough_paid : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ρ : ℝ), 1 ≤ ρ → ρ ≤ 5 / 4 → Real.log ↑N / ↑N * goldbachG11CollarRoughMass N ρ ≤ C * (ρ - 1)

The complete ordering collar is O(rho-1) in the required N/log N scale. Its constant and threshold are uniform for the entire closed rho range.