the proof notes, §6 Proposition 6. exceptional is defined in Zeta32.PrimeEdge.Reference (same name, same value). the proof is the S5 assembly (primitive reduction).

theorem Zeta32.PrimeEdge.isPrimitive_neg {f : Polynomial ℤ} (hf : f.IsPrimitive) : (-f).IsPrimitive

theorem Zeta32.PrimeEdge.P_isPrimitive (r : ℚ) (n : ℕ) (hQ : Q r n ≠ 0) : (P r n).IsPrimitive

theorem Zeta32.PrimeEdge.P_map_eq (r : ℚ) (n : ℕ) : Polynomial.map (Int.castRingHom ℚ) (P r n) = Polynomial.C (dtilde r n * scale n) * Q r n

theorem Zeta32.PrimeEdge.prime_edge (r : ℚ) (p : ℕ) [Fact (Nat.Prime p)] (hp : 7 ≤ p) (hE : p ∉ exceptional) (hden : ¬p ∣ r.den) : ∃ (c : ZMod p), c ≠ 0 ∧ Polynomial.map (Int.castRingHom (ZMod p)) (P r (p - 1)) = Polynomial.C c