Auxiliary nonmultiples and explicit degree choices for polynomial images of the original integer plane curve. Sharp finite-field counts remain explicit.

Explicit integer degree choices for both coefficient-height ranges.

theorem CCDN.auxiliary_integer_degree_selection (d : ℕ) {l R : ℝ} (hl : 0 ≤ l) (hR : 0 ≤ R) : ∃ (M : ℕ), d ≤ M ∧ l ≤ ↑M ∧ R < ↑M ∧ ↑M ≤ ↑d + l + R + 2

For nonnegative reals l and R, there is an integer M with d ≤ M, l ≤ M, R < M and M ≤ d + l + R + 2.

theorem CCDN.polynomial_map_auxiliary_small_height_degree {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {d t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 0 < d) {q : MvPolynomial (Fin 2) ℤ} {H : ℝ} (hq : IsBoundedPlaneCurve F q d H) (τ : Fin 3 → MvPolynomial (Fin 2) ℤ) (z : Fin t → Fin 2 → ℤ) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) q = 0) {B C : ℝ} (himage : IsBoxZeroFamily f B fun (i : Fin t) (j : Fin 3) => (MvPolynomial.eval (z i)) (τ j)) (hC : 0 ≤ C) (hheight : Real.log |↑(order.leadingCoeff f)| ≤ 4 * ↑d * Real.log B) (hcount : PlaneResidueCountBound C d q) : ∃ (M : ℕ), ↑M ≤ ↑d + Real.log B + 2 * Real.exp (heightDeterminantError C + 23) * ↑d ^ 3 * (1 + Real.log H / ↑d ^ 2) * B ^ (2 / ↑d) / |↑(order.leadingCoeff f)| ^ (1 / ↑d ^ 2) + 2 ∧ ∃ (g : MvPolynomial (Fin 3) ℤ), IsPointAuxiliary f g M fun (i : Fin t) (j : Fin 3) => (MvPolynomial.eval (z i)) (τ j)

Small-height auxiliary form for polynomial images of a plane curve: if the points τ (z i) are images of integral points z i on a bounded plane curve q of degree d and are integral zeros of the degree-d form f in a box of radius B, the leading coefficient of f has logarithm at most 4 d log B, and q satisfies the residue count bound with constant C, then there is an auxiliary form of explicitly bounded degree M through all of them.

theorem CCDN.polynomial_map_auxiliary_large_height_degree {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {d t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 0 < d) {q : MvPolynomial (Fin 2) ℤ} {H : ℝ} (hq : IsBoundedPlaneCurve F q d H) (τ : Fin 3 → MvPolynomial (Fin 2) ℤ) (z : Fin t → Fin 2 → ℤ) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) q = 0) {B C : ℝ} (himage : IsBoxZeroFamily f B fun (i : Fin t) (j : Fin 3) => (MvPolynomial.eval (z i)) (τ j)) (hC : 0 ≤ C) (T : ℝ) (hT : 0 ≤ T) (hheight : 4 * ↑d * Real.log B ≤ Real.log H) (hposition : Real.log H ≤ Real.log |↑(order.leadingCoeff f)| + T * ↑d ^ 2) (hcount : PlaneResidueCountBound C d q) : ∃ (M : ℕ), ↑M ≤ (34 + 8 * Real.exp (heightDeterminantError C + 6 + T)) * ↑d ^ 3 ∧ ∃ (g : MvPolynomial (Fin 3) ℤ), IsPointAuxiliary f g M fun (i : Fin t) (j : Fin 3) => (MvPolynomial.eval (z i)) (τ j)

Large-height auxiliary form for polynomial images of a plane curve: if the points τ (z i) are images of integral points z i on a bounded plane curve q of degree d and height H and are integral zeros of the degree-d form f in a box of radius B, with 4 d log B ≤ log H, H at most the leading coefficient of f times exp (T d²), and q satisfying the residue count bound with constant C, then there is an auxiliary form through all of them of degree at most (34 + 8 exp (heightDeterminantError C + 6 + T)) d³.