A polynomial box cutoff from the homogeneous coefficient-height bound. The constants are explicit; only their dependence on dimension is needed in the affine auxiliary-polynomial theorem.

theorem CCDN.affine_coefficient_height_cutoff (n d : ℕ) {A B : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hheight : B / A ≤ ↑((n + d).choose d) * Real.log ↑((n + d).choose d) + ↑((n + d).choose d) * ↑d * Real.log B) : B ≤ 4 * A ^ 2 * (↑d + 1) ^ (4 * n + 2)

If the constant-coefficient prime choice fails while the coefficient height obeys the determinant bound, the box is polynomially bounded in d.

theorem CCDN.polynomial_box_projective_power_bound {r d k : ℕ} (hr : 0 < r) (hd : 0 < d) {S B : ℝ} (hS : 1 ≤ S) (hB : 1 ≤ B) (hbound : B ≤ S * (↑d + 1) ^ k) : B ^ ((↑r + 1) / (↑r * ↑d ^ (1 / ↑r))) ≤ Real.exp (Real.log S + ↑k * (↑r + 1)) * B ^ (1 / ↑d ^ (1 / ↑r))

On a polynomial box range, the projective main term has the affine box exponent up to a constant independent of the degree and the box.