Integer parameters for the Stepanov construction

Harcos, Weil's bound for Kloosterman sums, printed page 12 (pages/harcos-weil-12.png). The coefficient spaces have integer dimension 2 * J * B; the equation space has the actual dimension ∑ k : Fin ell, (B + k.val * (m - 1) + (J - 1)). The ceiling choices below prove the strict inequality between these dimensions.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovEll (q : ℕ) : ℕ

The multiplicity parameter on Harcos's printed page 12.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovEll q = ⌈√↑q⌉₊

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovB (q m : ℕ) : ℕ

The integer number of coefficients in each polynomial block.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovB q m = ⌈(↑q - ↑m) / 2⌉₊

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovJ (q m ell : ℕ) : ℕ

The integer number of blocks in each of the two polynomial families.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovJ q m ell = ⌈↑ell / 2 + ↑ell ^ 2 * ↑m / ↑q⌉₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_equation_count (ell B J m : ℕ) : ∑ k : Fin ell, (B + ↑k * (m - 1) + (J - 1)) = ell * (B + (J - 1)) + ell * (ell - 1) / 2 * (m - 1)

Exact equation count, not an estimate for a hypothetical system.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_equation_count_real (ell B J m : ℕ) (hell : 0 < ell) (hJ : 0 < J) (hm : 1 ≤ m) : ↑(∑ k : Fin ell, (B + ↑k * (m - 1) + (J - 1))) = ↑ell * (↑B + ↑J - 1) + ↑ell * (↑ell - 1) / 2 * (↑m - 1)

The real form of the exact count, with no rounding of dimensions.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovEll_bounds {q : ℕ} (hq : 18 < q) : 0 < stepanovEll q ∧ 3 * stepanovEll q ≤ q ∧ q ≤ stepanovEll q ^ 2

For q > 18, the source's ceiling of the square root satisfies both the construction's range restriction and the final square-root bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanovB_bounds {q m : ℕ} (hmq : m < q) : 0 < stepanovB q m ∧ (↑q - ↑m) / 2 ≤ ↑(stepanovB q m) ∧ ↑(stepanovB q m) < (↑q - ↑m) / 2 + 1 ∧ 2 * (stepanovB q m - 1) + m < q

The ceiling defining the coefficient-block size respects the strict nonvanishing restriction 2(B-1)+m < q.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_parameters_count {q m ell : ℕ} (hm : 3 ≤ m) (hmq : 6 * m < q) (hell : 0 < ell) (hellq : 3 * ell ≤ q) : 0 < stepanovJ q m ell ∧ ∑ k : Fin ell, (stepanovB q m + ↑k * (m - 1) + (stepanovJ q m ell - 1)) < 2 * stepanovJ q m ell * stepanovB q m

Integer rounding of the two block parameters gives strictly more unknown coefficients than actual coefficient equations.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_parameters_degree {q m ell : ℕ} (hm : 3 ≤ m) (hmq : 6 * m < q) (hell : 0 < ell) (hellq : 3 * ell ≤ q) (hqsq : q ≤ ell ^ 2) : ↑(stepanovB q m + (q - 1) / 2 * m + (stepanovJ q m ell - 1) * q + ell * m) < ↑ell * (↑q / 2 + 2 * ↑m * ↑ell)

The same rounded parameters meet the source's degree budget. Only the final step uses q ≤ ell²; no parity assumption is needed here.

structure MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.StepanovParameterBounds (q m ell B J : ℕ) : Prop

All numerical requirements for the genuine finite-dimensional construction, including its exact equation count and a strict real degree budget.

• ell_pos : 0 < ell
• ell_le_card : ell ≤ q
• three_mul_ell_le : 3 * ell ≤ q
• card_le_ell_sq : q ≤ ell ^ 2
• B_pos : 0 < B
• J_pos : 0 < J
• coefficient_bound : 2 * (B - 1) + m < q
• equation_count_lt : ∑ k : Fin ell, (B + ↑k * (m - 1) + (J - 1)) < 2 * J * B
• degree_budget : ↑(B + (q - 1) / 2 * m + (J - 1) * q + ell * m) < ↑ell * (↑q / 2 + 2 * ↑m * ↑ell)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_integer_parameters (q m : ℕ) (hm : 3 ≤ m) (hmq : 6 * m < q) : StepanovParameterBounds q m (stepanovEll q) (stepanovB q m) (stepanovJ q m (stepanovEll q))

Harcos's three ceiling choices satisfy every integer constraint. This numerical theorem is valid even without assuming q odd.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_integer_parameters_exists (q m : ℕ) (hm : 3 ≤ m) (hmq : 6 * m < q) : ∃ (ell : ℕ) (B : ℕ) (J : ℕ), ell = ⌈√↑q⌉₊ ∧ B = ⌈(↑q - ↑m) / 2⌉₊ ∧ J = ⌈↑ell / 2 + ↑ell ^ 2 * ↑m / ↑q⌉₊ ∧ StepanovParameterBounds q m ell B J

An existential interface spelling out the source-matching choices.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stepanov_exists_auxiliary_polynomial_of_large_card {F : Type u_1} [Field F] [Fintype F] (f : Polynomial F) (a : F) (hq : Odd (Fintype.card F)) (hf0 : Polynomial.eval 0 f ≠ 0) (hf : ¬IsSquare (Polynomial.map (algebraMap F (AlgebraicClosure F)) f)) (hm : 3 ≤ f.natDegree) (hmq : 6 * f.natDegree < Fintype.card F) : have q := Fintype.card F; have ell := stepanovEll q; have B := stepanovB q f.natDegree; have J := stepanovJ q f.natDegree ell; ∃ (h : Polynomial F), h ≠ 0 ∧ h.degree < ↑(B + (q - 1) / 2 * f.natDegree + (J - 1) * q + ell * f.natDegree) ∧ ↑h.natDegree < ↑ell * (↑q / 2 + 2 * ↑f.natDegree * ↑ell) ∧ ∀ (x : F), Polynomial.eval x f = 0 ∨ Polynomial.eval x f ^ ((q - 1) / 2) = a → ∀ k < ell, Polynomial.eval x ((Polynomial.hasseDeriv k) h) = 0

The actual auxiliary polynomial with no assumed dimension inequality: the integer choices above discharge all numerical construction hypotheses. Both the strict integer degree bound and its real budget are retained.