The determinant comparison for polynomial homogeneous-coordinate maps of integer plane-curve points. The residue geometry comes from the plane equation, so coordinates such as (H,x,y) need no rational rows.

theorem CCDN.eval_polynomial_coordinate_map {R : Type u_1} [CommRing R] {n m : ℕ} (τ : Fin m → MvPolynomial (Fin n) R) (g : MvPolynomial (Fin m) R) (z : Fin n → R) : (MvPolynomial.eval z) ((MvPolynomial.aeval τ) g) = (MvPolynomial.eval fun (j : Fin m) => (MvPolynomial.eval z) (τ j)) g

Evaluating the composite g ∘ τ of a polynomial map τ and a polynomial g at z is evaluating g at τ(z).

theorem CCDN.polynomial_map_no_auxiliary_height_comparison {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] {d M t : ℕ} (order : MonomialOrder (Fin 3)) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 0 < d) (hdM : d ≤ M) {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) (hrel : ∀ (g : MvPolynomial (Fin 3) ℤ), g.IsHomogeneous M → (∀ (i : Fin t), (MvPolynomial.eval fun (j : Fin 3) => (MvPolynomial.eval (z i)) (τ j)) g = 0) → f ∣ g) (hcount : PlaneResidueCountBound C d q) : ∃ (s : ℕ), 0 < s ∧ s + (2 + (M - d)).choose (M - d) = (2 + M).choose M ∧ 2 * s + d ^ 2 = d * (2 * M + 3) ∧ ↑s ^ 2 / 2 * (Real.log ↑s - 4 * Real.log ↑d - Real.log (1 + Real.log H / ↑d ^ 2) - heightDeterminantError C) ≤ Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((2 + M).choose M) + ↑s * ↑M * Real.log B - (↑((2 + M).choose M) - ↑s) * Real.log |↑(order.leadingCoeff f)|

The complete comparison on the image of any polynomial coordinate map. The sharp finite-field count is an explicit hypothesis.