the proof notes, §6: Gram change of basis det[U_r(φ_a φ_c R_n)] = det(T)^2 · Q_n for any family of degree < h (adapted from det_basis_change in Arith/Local/Entry.lean and Li₂ Base/Gram.lean).

theorem Zeta32.PrimeEdge.gram_basis_change (r : ℚ) (n : ℕ) (E : Fin (3 * n) → Polynomial ℚ) (hE : ∀ (a : Fin (3 * n)), (E a).natDegree < 3 * n) : (Matrix.of fun (a b : Fin (3 * n)) => Arith.Local.Lfun r n (E a * E b * D n ^ 4)).det = Polynomial.C ((Arith.Local.coeffMat E).det ^ 2) * Q r n

S1-Gram.

noncomputable def Zeta32.PrimeEdge.G (r : ℚ) (p : ℕ) : Matrix (Idx p) (Idx p) (Polynomial ℚ)

The entry matrix G_{ac} = U_r(φ_a φ_c R_n) in the CRT basis, n = p - 1.

Equations

• Zeta32.PrimeEdge.G r p = Matrix.of fun (a c : Zeta32.PrimeEdge.Idx p) => Zeta32.Arith.Local.Lfun r (p - 1) (Zeta32.PrimeEdge.Aent p a c)

theorem Zeta32.PrimeEdge.G_apply {p : ℕ} (r : ℚ) (a c : Idx p) : G r p a c = Arith.Local.Lfun r (p - 1) (Aent p a c)

theorem Zeta32.PrimeEdge.G_det {p : ℕ} (r : ℚ) (hp : 5 ≤ p) : (G r p).det = Polynomial.C (basisDet p hp ^ 2) * Q r (p - 1)

S1. det G = det(T)^2 · Q_{p-1}.