Positioning a coefficient-height witness as the lexicographic leading coefficient by a bounded integral translation of the affine chart.

theorem CCDN.exponent_le_pure_first {n d : ℕ} (m : Fin (n + 1) →₀ ℕ) (hm : (m.sum fun (x : Fin (n + 1)) (e : ℕ) => e) ≤ d) : MonomialOrder.lex.toSyn m ≤ MonomialOrder.lex.toSyn (Finsupp.single 0 d)

Every exponent of total degree at most d is lexicographically at most the pure power x₀ ^ d of the first variable.

theorem CCDN.lex_leadingCoeff_eq_pure_first {R : Type u_1} [CommRing R] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (hd : f.totalDegree ≤ d) (hc : f.coeff (Finsupp.single 0 d) ≠ 0) : MonomialOrder.lex.leadingCoeff f = f.coeff (Finsupp.single 0 d)

If f has total degree at most d and a nonzero coefficient at x₀ ^ d, then its lexicographic leading coefficient is that coefficient.

theorem CCDN.homogeneousTranslation_pure_first {R : Type u_1} [CommRing R] {n d : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin (n + 1)) R) (hf : f.IsHomogeneous d) : ((homogeneousTranslation R a) f).coeff (Finsupp.single 0 d) = (MvPolynomial.eval (Fin.cons 1 a)) f

For f homogeneous of degree d, the coefficient of x₀ ^ d in the translate homogeneousTranslation R a f is the value f (1, a).

theorem CCDN.exists_bounded_leading_coefficient_translation {d : ℕ} (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) : ∃ (a : Fin 2 → ℤ), (∀ (j : Fin 2), 0 ≤ a j ∧ a j ≤ ↑d) ∧ MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) f) ≠ 0 ∧ CoefficientHeightLE f ((↑d + 1) ^ (2 * (d + 1)) * |↑(MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) f))|)

Every original coefficient is controlled by the leading coefficient obtained by a translation with parameters in 0,...,d.