Uniform scalar budgets for the unbounded dimension constant

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.EdgeDensity.dimension_quotient_le_target {ε x K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hx : 1 ≤ x) (hK : 0 ≤ K) : K / x ≤ (ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * x ^ (-(1 / 3))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.EdgeDensity.large_dimension_square_le_target {a ε x y K : ℝ} (ha : 0 < a) (hε : 0 < ε) (hε1 : ε ≤ 1) (hx : 1 ≤ x) (hy : 0 ≤ y) (hyx : y ≤ x) (hxK : x ≤ K) : (y / a * (1 + K / a)) ^ 2 ≤ (1 / a * (1 + 1 / a)) ^ 2 * ((ε ^ 8)⁻¹ * Real.exp (6 * K + 2) * x ^ (-(1 / 3)))

Large K is paid directly from the bounded aggregate, without multiplying the internal analytic error by an unbounded Euler ratio.