The factorization on a disc (n = p - 1): for d < p, dissectNum p d (Aent a c) = p^E u^E R(u) with R scaled and R(0) a unit, where

• on another disc d ≠ b (a, c of class b): E = 2 m_d + (1 if d = 0 else 4);
• on the own disc b: E = E_b + i + k, E_b = 1 for b = 0 and 4 otherwise, with R depending only on b. Also: farProd is scaled with unit constant term, and the near sets for n = p - 1.

noncomputable def Zeta32.PrimeEdge.crt0 (p b : ℕ) : Polynomial ℚ

The CRT basis vector without its own-class factor.

Equations

• Zeta32.PrimeEdge.crt0 p b = ∏ b' ∈ (Finset.range p).erase b, (Polynomial.X + Polynomial.C ↑b') ^ Zeta32.PrimeEdge.mult p b'

theorem Zeta32.PrimeEdge.crtBasis_eq {p : ℕ} (a : Idx p) : crtBasis p a = (Polynomial.X + Polynomial.C ↑↑a.fst) ^ ↑a.snd * crt0 p ↑a.fst

noncomputable def Zeta32.PrimeEdge.B0 (p b : ℕ) : Polynomial ℚ

φ_{b,0} φ_{b,0} D_{p-1}^4.

Equations

• Zeta32.PrimeEdge.B0 p b = Zeta32.PrimeEdge.crt0 p b * Zeta32.PrimeEdge.crt0 p b * Zeta32.D (p - 1) ^ 4

def Zeta32.PrimeEdge.ownExp (b : ℕ) : ℕ

Exponent of the own disc.

Equations

• Zeta32.PrimeEdge.ownExp b = if b = 0 then 1 else 4

theorem Zeta32.PrimeEdge.good_crt0 {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (hd : d < p) (b : ℕ) : Good p d (crt0 p b) (if d ∈ (Finset.range p).erase b then mult p d else 0)

theorem Zeta32.PrimeEdge.good_D {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (hd : d < p) : Good p d (D (p - 1)) (if d ∈ Finset.Icc 1 (p - 1) then 1 else 0)

theorem Zeta32.PrimeEdge.good_pow_own {p : ℕ} [Fact (Nat.Prime p)] {d b : ℕ} (hd : d < p) (hb : b < p) (i : ℕ) : Good p d ((Polynomial.X + Polynomial.C ↑b) ^ i) (i * if b = d then 1 else 0)

theorem Zeta32.PrimeEdge.good_other {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (hd : d < p) (a c : Idx p) (hac : a.fst = c.fst) (hdb : d ≠ ↑a.fst) : Good p d (Polynomial.X * Aent p a c) (2 * mult p d + if d = 0 then 1 else 4)

Other disc.

theorem Zeta32.PrimeEdge.good_B0 {p : ℕ} [Fact (Nat.Prime p)] {b : ℕ} (hb : b < p) : Good p b (Polynomial.X * B0 p b) (ownExp b)

theorem Zeta32.PrimeEdge.dissect_same {p : ℕ} [Fact (Nat.Prime p)] {b : ℕ} (hb : b < p) : ∃ (R : Polynomial ℚ), Scaled p R ∧ IsUnitV p (R.coeff 0) ∧ ∀ (a c : Idx p), ↑a.fst = b → ↑c.fst = b → dissectNum p b (Aent p a c) = Polynomial.C (↑p ^ (ownExp b + ↑a.snd + ↑c.snd)) * Polynomial.X ^ (ownExp b + ↑a.snd + ↑c.snd) * R

Own disc. The factor R depends only on the class b.

Far poles

theorem Zeta32.PrimeEdge.farProd_scaled {p : ℕ} [Fact (Nat.Prime p)] {n b : ℕ} (hb : b < p) : Scaled p (farProd n p b) ∧ IsUnitV p ((farProd n p b).coeff 0)

theorem Zeta32.PrimeEdge.scaledPS_div {p : ℕ} [Fact (Nat.Prime p)] {R F : Polynomial ℚ} (hR : Scaled p R) (hF : Scaled p F) (hF0 : IsUnitV p (F.coeff 0)) : ScaledPS p (↑R * (↑F)⁻¹)

The regular factor R / farProd as a power series.

theorem Zeta32.PrimeEdge.coeff_zero_div (R F : Polynomial ℚ) : (PowerSeries.coeff 0) (↑R * (↑F)⁻¹) = R.coeff 0 * (F.coeff 0)⁻¹

theorem Zeta32.PrimeEdge.series_eq {p : ℕ} (R F : Polynomial ℚ) (E : ℕ) : ↑(Polynomial.C (↑p ^ E) * Polynomial.X ^ E * R) * (↑F)⁻¹ = PowerSeries.C (↑p ^ E) * PowerSeries.X ^ E * (↑R * (↑F)⁻¹)

The dissected series: dissectNum / farProd = p^E u^E K(u).

Near sets for n = p - 1

theorem Zeta32.PrimeEdge.mem_nearSet_iff {p n b : ℕ} (hb : b < p) (m : ℕ) : m ∈ nearSet n p b ↔ 1 ≤ b + p * m ∧ b + p * m ≤ 5 * n

theorem Zeta32.PrimeEdge.lt_five_of_mem_nearSet {p b : ℕ} (hb : b < p) {m : ℕ} (hm : m ∈ nearSet (p - 1) p b) : m < 5

theorem Zeta32.PrimeEdge.nearSet_subset {p b : ℕ} (hb : b < p) : nearSet (p - 1) p b ⊆ Finset.range 5

theorem Zeta32.PrimeEdge.nearSet_zero {p : ℕ} (hp : 5 ≤ p) : nearSet (p - 1) p 0 = {1, 2, 3, 4}

theorem Zeta32.PrimeEdge.nearSet_low {p b : ℕ} (hb1 : 1 ≤ b) (hb : b + 5 ≤ p) : nearSet (p - 1) p b = {0, 1, 2, 3, 4}

theorem Zeta32.PrimeEdge.nearSet_high {p : ℕ} (hp : 5 ≤ p) {b : ℕ} (hb1 : 1 ≤ b) (hbp : b < p) (hb : p < b + 5) : nearSet (p - 1) p b = {0, 1, 2, 3}