theorem
CCDN.stepanov_numeric_dimension
(d p x y N : ℕ)
(hd : 0 < d)
(hp : stepanovThreshold d < p)
(hx : x ^ 2 ≤ p)
(hy : p ≤ y + d)
(hN : N + 4 * d ^ 2 = x)
(hNpos : 0 < N)
:
The numerical dimension inequality of the Stepanov method: for p > 27 d⁴, x ^ 2 ≤ p,
p ≤ y + d and N = x - 4 d² > 0, one has N (x + y + d + d² N) < (x - d²) (y - d²).
theorem
CCDN.exists_stepanov_integer_parameters
(d p : ℕ)
(hd : 0 < d)
(hp : stepanovThreshold d < p)
:
Concrete integer degrees: A=floor(sqrt(p)/d), D=floor((p-1)/d), and N=dA-4d^2. The cutoff ensures a positive multiplicity.