Documentation

LeanPool.CCDN.AuxiliaryPolynomial.HypersurfacePositionHeight

The bounded shear has a dimension-uniform logarithmic positioning cost.

Bounded integer shears placing a large coefficient first, in all dimensions.

theorem CCDN.log_nat_add_one_le_root {r d : ℕ} (hr : 0 < r) (hd : 0 < d) :
Real.log (↑d + 1) ≤ (↑r + 1) * ↑d ^ (1 / ↑r)

For positive integers r and d, log (d + 1) ≤ (r + 1) * d ^ (1/r).

theorem CCDN.exists_hypersurface_coefficient_position {n r d : ℕ} (hr : 0 < r) (hd : 0 < d) (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) :
∃ (a : Fin n → ℤ) (H : ℝ), (∀ (j : Fin n), 0 ≤ a j ∧ a j ≤ ↑d) ∧ 1 ≤ H ∧ CoefficientHeightLE f H ∧ CoefficientHeightLE ((homogeneousTranslation ℤ a) f) H ∧ Real.log H ≤ Real.log |↑(MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) f))| + (5 * ↑n + 5) * (↑r + 1) * ↑d * ↑d ^ (1 / ↑r)

Integer coordinates supply the logarithmic positioning condition, and the chosen height bounds both the original and translated coefficients.