the proof notes, §6 "Basis": the CRT product basis for n = p - 1, φ_{b,i} = (t + b)^i ∏_{b' ≠ b} (t + b')^{m_{b'}} (0 ≤ b < p, i < m_b), h = 3(p-1) vectors, each of degree < h. On the disc t = -b + p u it is (p u)^i · (p-unit), and on every other disc b' it carries the factor (t + b')^{m_{b'}}.

noncomputable def Zeta32.PrimeEdge.crtBasis (p : ℕ) (a : Idx p) : Polynomial ℚ

The CRT product basis vector φ_a.

Equations

• Zeta32.PrimeEdge.crtBasis p a = (Polynomial.X + Polynomial.C ↑↑a.fst) ^ ↑a.snd * ∏ b ∈ (Finset.range p).erase ↑a.fst, (Polynomial.X + Polynomial.C ↑b) ^ Zeta32.PrimeEdge.mult p b

noncomputable def Zeta32.PrimeEdge.Aent (p : ℕ) (a c : Idx p) : Polynomial ℚ

The entry numerator φ_a φ_c D_n^4, n = p - 1.

Equations

• Zeta32.PrimeEdge.Aent p a c = Zeta32.PrimeEdge.crtBasis p a * Zeta32.PrimeEdge.crtBasis p c * Zeta32.D (p - 1) ^ 4

noncomputable def Zeta32.PrimeEdge.idxEquiv {p : ℕ} (hp : 5 ≤ p) : Fin (3 * (p - 1)) ≃ Idx p

An enumeration of the basis indices by Fin h.

Equations

• Zeta32.PrimeEdge.idxEquiv hp = (Fintype.equivFinOfCardEq ⋯).symm

noncomputable def Zeta32.PrimeEdge.basisDet (p : ℕ) (hp : 5 ≤ p) : ℚ

Determinant of the change of basis from monomials to the CRT basis.

Equations

• Zeta32.PrimeEdge.basisDet p hp = (Zeta32.Arith.Local.coeffMat fun (i : Fin (3 * (p - 1))) => Zeta32.PrimeEdge.crtBasis p ((Zeta32.PrimeEdge.idxEquiv hp) i)).det

theorem Zeta32.PrimeEdge.crtBasis_natDegree_lt {p : ℕ} (hp : 5 ≤ p) (a : Idx p) : (crtBasis p a).natDegree < 3 * (p - 1)

S1-deg. deg φ_a = i + (h - m_b) < h.

theorem Zeta32.PrimeEdge.basisDet_unit {p : ℕ} [Fact (Nat.Prime p)] (hp : 5 ≤ p) : basisDet p hp ≠ 0 ∧ padicValRat p (basisDet p hp) = 0

S1-unit. The change of basis is unimodular over ℤ_(p): the CRT basis is independent modulo p (centres -b distinct mod p), so its coefficient determinant is a p-adic unit.

theorem Zeta32.PrimeEdge.D_natDegree_le (m : ℕ) : (D m).natDegree ≤ m

theorem Zeta32.PrimeEdge.Aent_natDegree {p : ℕ} (hp : 5 ≤ p) (a c : Idx p) : (Aent p a c).natDegree + 2 ≤ 10 * (p - 1)