Coefficient height of an integer plane section with bounded parameters, and the resulting bound on the universal bad-prime witness.

theorem CCDN.universalPlaneSection_map {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommRing R] [CommRing S] (φ : R →+* S) (f : MvPolynomial σ R) (v : PlaneParameters σ → R) : universalPlaneSection ((MvPolynomial.map φ) f) (⇑φ ∘ v) = (bivariateMap φ) (universalPlaneSection f v)

Taking plane sections commutes with mapping coefficients along a ring homomorphism φ: the section of map φ f at φ ∘ v is the coefficient-wise image of the section of f at v.

def CCDN.integerPlaneHeight (m d : ℕ) (H A : ℝ) : ℝ

Height supplied by interpolation on the plane grid.

Equations

• CCDN.integerPlaneHeight m d H A = (↑d + 1) ^ (2 * (d + 1)) * ((↑d + 1) ^ m * H * (A * (1 + 2 * ↑d)) ^ d)

theorem CCDN.integer_plane_section_coefficient_bound {σ : Type u_1} [Fintype σ] (f : MvPolynomial σ ℤ) (H A : ℝ) (hH : 0 ≤ H) (hA : 1 ≤ A) (hf : CoefficientHeightLE f H) (v : PlaneParameters σ → ℤ) (hv : InBox v A) : BivariateCoefficientBound (universalPlaneSection f v) (integerPlaneHeight (Fintype.card σ) f.totalDegree H A)

Each coefficient of a bounded integer plane section is bounded explicitly in terms of the original coefficient height, degree and ambient dimension.