The prime cutoff 27 d⁴ and the absolute constants of the finite-field point counts.

Every count below holds for primes p > stepanovThreshold d = 27 d⁴ and has the shape main term + C d² √p · (lower-order power of p). The constants are derived from the plane constant planeResidueConstant = 161 by explicit additive corrections, recorded in the docstrings and in the _eq_add lemmas. They are defined as numerals, so statements quoting the numerals are definitionally equal to statements using the names.

def CCDN.stepanovThreshold {R : Type u_1} [Semiring R] (d : R) : R

The prime cutoff 27 d⁴ of the Stepanov method. For p > 27 d⁴ the integer Stepanov parameters A = ⌊√p / d⌋, D = ⌊(p - 1) / d⌋, N = d A - 4 d² exist with N > 0 (exists_stepanov_integer_parameters), the Hilbert-dimension inequality holds (stepanov_numeric_dimension), and √p < 32 N (stepanov_real_bound), since 31² · 27 > 160². Bad primes are only counted above this cutoff; below it the trivial bounds are used. The definition is polymorphic so that it reads the same over ℕ and ℝ.

Equations

• CCDN.stepanovThreshold d = 27 * d ^ 4

@[simp]

theorem CCDN.Nat.cast_stepanovThreshold {R : Type u_1} [Semiring R] (d : ℕ) : ↑(stepanovThreshold d) = stepanovThreshold ↑d

The cast of the natural-number cutoff stepanovThreshold d is the cutoff of the cast of d.

theorem CCDN.stepanovThreshold_le_stepanovThreshold {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : stepanovThreshold a ≤ stepanovThreshold b

The cutoff stepanovThreshold is monotone on nonnegative arguments.

def CCDN.planeResidueConstant : ℝ

The constant 161 of the affine plane-curve count #C(𝔽_p) ≤ p + 161 d² √p (plane_finite_field_card_bound). In stepanov_real_bound the Stepanov count t N ≤ d D + p (N + 4 d²) + d² N is bounded using d D < p, (4 d² + 1) p ≤ 5 d² p, p ≤ 32 N √p and 1 ≤ √p, giving t ≤ p + (5 · 32 + 1) d² √p.

Equations

• CCDN.planeResidueConstant = 161

def CCDN.projectivePlaneResidueConstant : ℝ

The constant 162 = 161 + 1 of the projective plane-curve count (projective_plane_finite_field_card_bound): the affine chart contributes p + 161 d² √p and the line at infinity at most d ≤ d² √p further points (projectivePlaneResidueConstant_eq_add).

Equations

• CCDN.projectivePlaneResidueConstant = 162

def CCDN.projectivePlaneDeterminantConstant : ℝ

The constant C = 164 = 162 + 2 for which the projective plane total multiplicity is at most p + (C + 1) d² √p (projectivePlaneTotalMultiplicity_le). The singular correction 3 d² (d - 1) ≤ 3 d² √p adds 3 to 162; the shift by one matches the affine convention of degreeFourDeterminantError, whose singular correction d² (d - 1) costs 1 (projectivePlaneDeterminantConstant_eq_add).

Equations

• CCDN.projectivePlaneDeterminantConstant = 164

def CCDN.hypersurfaceResidueConstant : ℝ

The constant 164 = 161 + 3 of the affine hypersurface count #X(𝔽_p) ≤ p^(m-1) + 164 d² p^(m-2) √p (affine_hypersurface_finite_field_bound). Averaging the plane count over plane sections gives 161; bad and zero plane sections cost at most 3 d² p √p (hypersurface_bad_section_error, hypersurfaceResidueConstant_eq_add).

Equations

• CCDN.hypersurfaceResidueConstant = 164

def CCDN.projectiveHypersurfaceResidueConstant : ℝ

The constant 330 = 2 (164 + 1) of the projective hypersurface count (projective_hypersurface_finite_field_bound). Applied to the affine cone count with error H = 164 d² √p, homogeneous_projective_count_of_cone_bound gives the projective error 2 (H + 1) p^(m-2), and 1 ≤ d² √p (projectiveHypersurfaceResidueConstant_eq_add).

Equations

• CCDN.projectiveHypersurfaceResidueConstant = 330

theorem CCDN.planeResidueConstant_eq : planeResidueConstant = 161

The value of planeResidueConstant is 161.

theorem CCDN.projectivePlaneResidueConstant_eq : projectivePlaneResidueConstant = 162

The value of projectivePlaneResidueConstant is 162.

theorem CCDN.projectivePlaneDeterminantConstant_eq : projectivePlaneDeterminantConstant = 164

The value of projectivePlaneDeterminantConstant is 164.

theorem CCDN.hypersurfaceResidueConstant_eq : hypersurfaceResidueConstant = 164

The value of hypersurfaceResidueConstant is 164.

theorem CCDN.projectiveHypersurfaceResidueConstant_eq : projectiveHypersurfaceResidueConstant = 330

The value of projectiveHypersurfaceResidueConstant is 330.

theorem CCDN.projectivePlaneResidueConstant_eq_add : projectivePlaneResidueConstant = planeResidueConstant + 1

The projective plane constant exceeds the affine plane constant by 1, accounting for the points on the line at infinity.

theorem CCDN.projectivePlaneDeterminantConstant_eq_add : projectivePlaneDeterminantConstant = projectivePlaneResidueConstant + 2

The projective plane determinant constant exceeds the projective plane residue constant by 2.

theorem CCDN.hypersurfaceResidueConstant_eq_add : hypersurfaceResidueConstant = planeResidueConstant + 3

The affine hypersurface constant exceeds the plane constant by 3, accounting for bad and zero plane sections.

theorem CCDN.projectiveHypersurfaceResidueConstant_eq_add : projectiveHypersurfaceResidueConstant = 2 * (hypersurfaceResidueConstant + 1)

The projective hypersurface constant is twice the affine hypersurface constant plus one.

theorem CCDN.planeResidueConstant_pos : 0 < planeResidueConstant

The plane constant planeResidueConstant is positive.

theorem CCDN.projectivePlaneDeterminantConstant_pos : 0 < projectivePlaneDeterminantConstant

The constant projectivePlaneDeterminantConstant is positive.

theorem CCDN.projectiveHypersurfaceResidueConstant_pos : 0 < projectiveHypersurfaceResidueConstant

The constant projectiveHypersurfaceResidueConstant is positive.