Documentation

LeanPool.CCDN.Plane.StepanovParameters

Integer parameters for the Stepanov construction above the cutoff stepanovThreshold d = 27 * d ^ 4.

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) :
N * (x + y + d + d ^ 2 * N) < (x - d ^ 2) * (y - d ^ 2)

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) :
∃ (A : ℕ) (D : ℕ) (N : ℕ), d ≤ A ∧ d ≤ D ∧ d * D < p ∧ N ≤ p ∧ N + 4 * d ^ 2 = d * A ∧ 0 < N ∧ (d * A) ^ 2 ≤ p ∧ p ≤ d * D + d ∧ p < (d * A + d) ^ 2

Concrete integer degrees: A=floor(sqrt(p)/d), D=floor((p-1)/d), and N=dA-4d^2. The cutoff ensures a positive multiplicity.