Quantitative large-box and small-box reductions for affine scaling.

theorem CCDN.large_box_height_threshold {d : ℕ} (hd : 0 < d) {A B : ℝ} (hA : 1 ≤ A) (hB : (12 * A) ^ 2 * ↑d ^ 2 ≤ B) : 4 * ↑d * Real.log ((↑d + 1) * B) ≤ B / A

Above a fixed multiple of d², a logarithmic height of B/A is large enough for the unscaled auxiliary-polynomial branch.

theorem CCDN.small_box_unscaled_degree_bound {d : ℕ} (hd : 0 < d) {S B C : ℝ} (hS : 1 ≤ S) (hB : 1 ≤ B) (hBS : B ≤ S * ↑d ^ 2) : ↑d * scaledPlaneAuxiliaryDegreeBound d C ((↑d + 1) * B) 1 ≤ (Real.log S + 6 + 2 * Real.exp (heightDeterminantError C + 23) * Real.exp 14 * Real.exp (2 * Real.log S + 6)) * ↑d ^ 4

In the small-box range 1 ≤ B ≤ S * d ^ 2 (with 1 ≤ S), the unscaled auxiliary degree bound d * scaledPlaneAuxiliaryDegreeBound d C ((d + 1) * B) 1 is at most a constant depending only on S and C, times d ^ 4.