Coefficient-uniform projective plane counts after a bounded integral coordinate change. The finite-field and positioning inputs are proved.

theorem CCDN.projective_plane_finite_count_positioned {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {d t : ℕ} (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hd : 2 ≤ d) (hprim : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) (z : Fin t → IntPoint 3) (hz0 : ∀ (i : Fin t), z i ≠ 0) (hinj : Function.Injective fun (i : Fin t) => Projectivization.mk ℚ (rationalPoint (z i)) ⋯) {B : ℝ} (hzB : IsPrimitiveBoxZeroFamily f B z) : ↑t ≤ max (↑d * scaledPlaneAuxiliaryDegreeBound d projectivePlaneDeterminantConstant ((↑d + 1) * B) 1) ((34 + 8 * Real.exp (heightDeterminantError projectivePlaneDeterminantConstant + 20)) * ↑d ^ 4)

Coefficient-uniform projective plane count: for a primitive ternary integer form f of degree d ≥ 2, absolutely irreducible over an algebraically closed field of characteristic zero, the number of distinct projective points with primitive integer coordinates in the box of size B on f = 0 is at most the maximum of the two degree bounds of the scaled plane count with residue constant projectivePlaneDeterminantConstant. The proof first moves f by a bounded integral coordinate change.