theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Collar_cofactor_geometry {N : ℕ} (hN : 4 ≤ N) {ρ : ℝ} (hρ : 1 ≤ ρ) (hρu : ρ ≤ 5 / 4) {v : GoldbachG11SwitchedBody} (hv : v ∈ goldbachG11CollarBoxes N ρ) : have y := ρ ^ 2 * ↑N / ↑(goldbachG11SwitchedBodyProd v); ↑N ^ (1 / 2) ≤ y ∧ y ≤ ↑N ^ 2 ∧ ↑N ^ (4 / 53) ≤ ↑v.snd.snd.fst ∧ ↑v.snd.snd.fst ≤ ↑N ^ (4 / 33) ∧ 0 < goldbachG11SwitchedBodyProd v ∧ Nat.Prime v.snd.snd.fst

The same rho that enlarges the short-prime endpoint also enlarges the product endpoint by rho^2. Hence no extra loss is needed for the lower cofactor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Collar_rough_point_bound : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ρ : ℝ), 1 ≤ ρ → ρ ≤ 5 / 4 → ∀ v ∈ goldbachG11CollarBoxes N ρ, Real.log ↑N / ↑N * ↑(LiLiuPrereqBuchstab.roughCount (ρ ^ 2 * ↑N / ↑(goldbachG11SwitchedBodyProd v)) ↑v.snd.snd.fst) ≤ 53 * (1 / ↑(goldbachG11SwitchedBodyProd v))

A fixed coarse rough-count budget for the ordering collar, uniform in rho.