Minimal-polynomial linkage in Harcos's Theorem 6

Harcos, §3, pages 7–8 (pages/harcos-lpolynomial-07.png and pages/harcos-stepanov-08.png), identifies the character on each orbit with a power of the polynomial character. The extension multiplicity is a natural-number quotient, not division in the base field.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpoly_inv_natDegree (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (t : L) : (minpoly K t⁻¹).natDegree = (minpoly K t).natDegree

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpoly_inv (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (t : L) (ht : t ≠ 0) : minpoly K t⁻¹ = (minpoly K t).reverse * Polynomial.C ((minpoly K t).coeff 0)⁻¹

The inverse minimal polynomial is the normalized coefficient reversal.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpoly_inv_nextCoeff (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (t : L) (ht : t ≠ 0) : (minpoly K t⁻¹).nextCoeff = (minpoly K t).coeff 1 / (minpoly K t).coeff 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpoly_extension_index (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (t : L) : Module.finrank (↥K⟮t⟯) L = Module.finrank K L / (minpoly K t).natDegree

The tower index is an integer quotient before casting to the base field.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_inv_minpoly (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (t : L) (ht : t ≠ 0) : (Algebra.trace K L) t⁻¹ = ↑(Module.finrank K L / (minpoly K t).natDegree) * (-(minpoly K t).coeff 1 / (minpoly K t).coeff 0)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_minpoly_phase (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (a b : K) (t : L) (ht : t ≠ 0) : (Algebra.trace K L) ((algebraMap K L) a * t + (algebraMap K L) b / t) = ↑(Module.finrank K L / (minpoly K t).natDegree) * (-a * (minpoly K t).nextCoeff - b * (minpoly K t).coeff 1 / (minpoly K t).coeff 0)

The actual trace of the Kloosterman phase, including inseparable tower indices and indices divisible by the characteristic.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpoly_eta_power (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (a b : ZMod p) (m : ℕ) (t : F) (ht : t ≠ 0) : ZMod.stdAddChar (↑m * (Algebra.trace (ZMod p) F) ((algebraMap (ZMod p) F) a * t + (algebraMap (ZMod p) F) b / t)) = harcosEta a b (minpoly (ZMod p) t) ^ (m * (Module.finrank (ZMod p) F / (minpoly (ZMod p) t).natDegree))

The character value is constant on the minimal-polynomial fiber. The exponent is a natural number even when the characteristic divides the index.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMinpolyOrbits (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] : Finset (Polynomial (ZMod p))

The finite set of minimal polynomials of nonzero elements of the extension.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMinpolyOrbits p F = Finset.image (fun (t : Fˣ) => minpoly (ZMod p) ↑t) Finset.univ

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMinpolyFiber (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (k : Polynomial (ZMod p)) : Finset Fˣ

Each orbit is represented by its actual nonzero roots in the given field.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMinpolyFiber p F k = {t : Fˣ | minpoly (ZMod p) ↑t = k}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_mem_minpolyOrbits (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (k : Polynomial (ZMod p)) : k ∈ harcosMinpolyOrbits p F ↔ ∃ (t : Fˣ), minpoly (ZMod p) ↑t = k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_mem_minpolyFiber (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (k : Polynomial (ZMod p)) (t : Fˣ) : t ∈ harcosMinpolyFiber p F k ↔ minpoly (ZMod p) ↑t = k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_mem_minpolyOrbits_iff (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (k : Polynomial (ZMod p)) : k ∈ harcosMinpolyOrbits p F ↔ k.Monic ∧ Irreducible k ∧ k.coeff 0 ≠ 0 ∧ k.natDegree ∣ Module.finrank (ZMod p) F

Harcos's orbit index set is exactly all monic irreducibles of degree dividing the extension degree, except X, excluded by the nonzero constant coefficient.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpolyFiber_card (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (k : Polynomial (ZMod p)) (hk : k ∈ harcosMinpolyOrbits p F) : (harcosMinpolyFiber p F k).card = k.natDegree

Each minimal-polynomial fiber has cardinality exactly its degree, with no chosen algebraic closure and no assumption about orbit cardinalities.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_minpolyFiber_character_sum (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] (a b : ZMod p) (m : ℕ) (k : Polynomial (ZMod p)) (hk : k ∈ harcosMinpolyOrbits p F) : ∑ t ∈ harcosMinpolyFiber p F k, ZMod.stdAddChar (↑m * (Algebra.trace (ZMod p) F) ((algebraMap (ZMod p) F) a * ↑t + (algebraMap (ZMod p) F) b / ↑t)) = ↑k.natDegree * harcosEta a b k ^ (m * (Module.finrank (ZMod p) F / k.natDegree))

The contribution of a single orbit is its degree times its eta power.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_character_minpoly_sum (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] [DecidableEq F] (a b : ZMod p) (m : ℕ) : ∑ t : Fˣ, ZMod.stdAddChar (↑m * (Algebra.trace (ZMod p) F) ((algebraMap (ZMod p) F) a * ↑t + (algebraMap (ZMod p) F) b / ↑t)) = ∑ k ∈ harcosMinpolyOrbits p F, ↑k.natDegree * harcosEta a b k ^ (m * (Module.finrank (ZMod p) F / k.natDegree))

The finite orbit-sum identity in the last step of Harcos's Theorem 6. Together with harcos_mem_minpolyOrbits_iff, this is precisely the sum over monic irreducibles of degrees dividing the extension degree, excluding X.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosTraceKloosterman_minpoly_sum (p : ℕ) [Fact (Nat.Prime p)] (F : Type u_1) [Field F] [Fintype F] [Algebra (ZMod p) F] [DecidableEq F] (a b m : ZMod p) : harcosTraceKloosterman p F a b m = ∑ k ∈ harcosMinpolyOrbits p F, ↑k.natDegree * harcosEta a b k ^ (m.val * (Module.finrank (ZMod p) F / k.natDegree))

The orbit identity consumes the actual trace-character sum used in the Artin–Schreier point-count bridge, for every prime-field frequency.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosEta_frequency_of_coeff_zero_ne (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) (k : Polynomial (ZMod p)) (hk : k.coeff 0 ≠ 0) : harcosEta (m * a) (m * b) k = harcosEta a b k ^ m.val

Frequency scaling agrees with an eta power on polynomials not divisible by X. The nonzero-constant condition matters at frequency zero.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionMinpolyOrbits (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Finset (Polynomial (ZMod p))

Orbit indices for the same fixed extension used by harcosExtensionKloosterman.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionMinpolyOrbits p n = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosMinpolyOrbits p (GaloisField p n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_mem_extensionMinpolyOrbits_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (k : Polynomial (ZMod p)) : k ∈ harcosExtensionMinpolyOrbits p n ↔ k.Monic ∧ Irreducible k ∧ k.coeff 0 ≠ 0 ∧ k.natDegree ∣ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_minpoly_sum (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) (n : ℕ) (hn : 0 < n) : harcosExtensionKloosterman p a b m n = ∑ k ∈ harcosExtensionMinpolyOrbits p n, ↑k.natDegree * harcosEta a b k ^ (m.val * (n / k.natDegree))

The orbit identity for the actual extension sequence, only at positive degrees: GaloisField p 0 is not a field with one element.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_minpoly_sum_scaled (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) (n : ℕ) (hn : 0 < n) : harcosExtensionKloosterman p a b m n = ∑ k ∈ harcosExtensionMinpolyOrbits p n, ↑k.natDegree * harcosEta (m * a) (m * b) k ^ (n / k.natDegree)

Frequency-scaled form of the orbit identity, matching the finite Euler coefficient for the actual polynomial character harcosEta (m*a) (m*b).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionMinpolyOrbits_eq_euler (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : harcosExtensionMinpolyOrbits p n = harcosEulerNonzeroPrimes p n

The independently constructed Euler index and actual field-orbit index agree.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_eq_eulerLogCoefficient (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) (n : ℕ) (hn : 0 < n) : harcosExtensionKloosterman p a b m n = harcosEulerLogCoefficient (↑(harcosEtaHom (m * a) (m * b))) n

Actual extension-field character sums are the logarithmic coefficients of the actual polynomial-character Euler series.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosExtensionKloosterman_eq_reciprocalRoots (p : ℕ) [Fact (Nat.Prime p)] (a b m : ZMod p) (ha : a ≠ 0) (hm : m ≠ 0) (n : ℕ) (hn : 0 < n) : harcosExtensionKloosterman p a b m n = -(harcosReciprocalRootPlus (m * a) (m * b) ^ n + harcosReciprocalRootMinus (m * a) (m * b) ^ n)

Harcos's Theorem 6 with explicitly constructed reciprocal roots, not an assumed power-sum or Euler identity.