Sharp finite-field counting and the complete rational-plane integral-point bound. The finite-field proof uses the constructed Stepanov auxiliary and retains an explicit absolute error constant.

The complete rational plane reduction to sharp finite-field counting. The non-absolutely-irreducible case is bounded by d².

The explicit real-valued error term for the integer Stepanov parameters.

The affine residue points of an integer plane equation are the zeros of its reduction.

theorem CCDN.stepanov_real_bound (d p A D N t : ℕ) (hd : 0 < d) (hp : stepanovThreshold d < p) (hD : d * D < p) (hN : N + 4 * d ^ 2 = d * A) (hNpos : 0 < N) (hpx : p < (d * A + d) ^ 2) (hcount : t * N ≤ d * (D + p * A) + d * (d - 1) * N) : ↑t ≤ ↑p + planeResidueConstant * ↑d ^ 2 * √↑p

The Stepanov count t N ≤ d (D + p A) + d (d - 1) N gives the plane-curve bound t ≤ p + 161 d² √p; see planeResidueConstant for the derivation of 161.

theorem CCDN.plane_finite_field_card_bound {ι : Type u_1} [Fintype ι] (p : ℕ) [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 2) (ZMod p)) (hf : Irreducible f) (hsize : stepanovThreshold ↑f.totalDegree < ↑p) (z : ι → Fin 2 → ZMod p) (hz : Function.Injective z) (hzero : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0) : ↑(Fintype.card ι) ≤ ↑p + planeResidueConstant * ↑f.totalDegree ^ 2 * √↑p

An irreducible plane equation over the prime field has at most p + planeResidueConstant * d² * √p rational points when p > stepanovThreshold d.

theorem CCDN.planeResidueBound : PlaneResidueBound planeResidueConstant

The sharp finite-field hypothesis used by the affine determinant argument holds with the absolute constant planeResidueConstant = 161.

theorem CCDN.planeCurveBound : PlaneCurveBound

The full coefficient-uniform rational-plane integral-point bound.