Positioning a scaled homogeneous model while retaining a coefficient bound for the original affine equation and the full scaling gain in its height.

A monotone scaled logarithmic-height ratio. A lower bound for the scaled model height yields the saving needed to change the box exponent 2/d to 1/d.

theorem CCDN.exists_scaled_model_position (f : MvPolynomial (Fin 2) ℤ) (hf0 : f ≠ 0) (hd : 0 < f.totalDegree) {h : ℤ} (hh : 1 ≤ h) : ∃ (a : Fin 2 → ℤ) (H : ℝ), (∀ (j : Fin 2), 0 ≤ a j ∧ a j ≤ ↑f.totalDegree) ∧ 1 ≤ H ∧ ↑h ^ f.totalDegree ≤ H ∧ CoefficientHeightLE f H ∧ Real.log |↑(MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) (scaledHomogenize f.totalDegree h f)))| ≤ Real.log H ∧ Real.log H ≤ Real.log |↑(MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) (scaledHomogenize f.totalDegree h f)))| + 14 * ↑f.totalDegree ^ 2

The model height is at least h^d and also bounds every original affine coefficient, even after leading-coefficient positioning of the scaled model.

theorem CCDN.scaled_positioned_height_ratio_le {d : ℕ} (hd : 0 < d) {h H L : ℝ} (hh : 1 ≤ h) (hH : h ^ d ≤ H) (hL : 0 < L) (hposition : Real.log H ≤ Real.log L + 14 * ↑d ^ 2) : (1 + Real.log H / ↑d ^ 2) / L ^ (1 / ↑d ^ 2) ≤ Real.exp 14 * ((1 + Real.log h / ↑d) / h ^ (1 / ↑d))

The exact height saving obtained from a scaling factor h.