S3: the X-free block-diagonal reference matrix of the proof notes, §6 and its determinant p^{Σπ} · (unit). Blocks: Ref_{⟨b,i⟩,⟨b,k⟩} = p^{c_b+i+k} w_b V⁰(u^{i+k} r_type).

def Zeta32.PrimeEdge.exceptional : Finset ℕ

The exceptional primes of Proposition 6.

Equations

• Zeta32.PrimeEdge.exceptional = {11, 67, 193, 283, 367, 110731}

noncomputable def Zeta32.PrimeEdge.Ref (p : ℕ) (w : ℕ → ℚ) : Matrix (Idx p) (Idx p) (Polynomial ℚ)

The reference matrix for unit weights w.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Zeta32.PrimeEdge.hankelDet (p : ℕ) (b : Fin p) : ℚ

The Hankel determinant of the fixed block of class b.

Equations

• Zeta32.PrimeEdge.hankelDet p b = (Matrix.of fun (i k : Fin (Zeta32.PrimeEdge.mult p ↑b)) => Zeta32.PrimeEdge.blockMoment p (↑b) (↑i + ↑k)).det

noncomputable def Zeta32.PrimeEdge.refUnit (p : ℕ) (w : ℕ → ℚ) : ℚ

The unit of the reference determinant.

Equations

• Zeta32.PrimeEdge.refUnit p w = ∏ b : Fin p, w ↑b ^ Zeta32.PrimeEdge.mult p ↑b * Zeta32.PrimeEdge.hankelDet p b

def Zeta32.PrimeEdge.levelSum (p : ℕ) : ℤ

Σ π as an integer.

Equations

• Zeta32.PrimeEdge.levelSum p = ∑ a : Zeta32.PrimeEdge.Idx p, Zeta32.PrimeEdge.level p a

theorem Zeta32.PrimeEdge.Ref_det {p : ℕ} [Fact (Nat.Prime p)] (w : ℕ → ℚ) : (Ref p w).det = Polynomial.C (↑p ^ levelSum p * refUnit p w)

S3a (block diagonal determinant). Scaling rows by p^{c_b+i} and columns by p^k inside each class block (det_mul_row, det_mul_column, BlockTriangular.det or det_blockDiagonal'-type reindexing).

theorem Zeta32.PrimeEdge.hankelDet_eq {p : ℕ} (b : Fin p) : hankelDet p b = if ↑b = 0 then M₀.det else if ↑b + 5 ≤ p then lowBlockMatrix.det else highBlockMatrix.det

S3b (the three fixed determinants). hankelDet is det M₀, det lowBlockMatrix or det highBlockMatrix.

theorem Zeta32.PrimeEdge.padicValRat_eq_zero_of_not_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] {z d : ℕ} (hz : z ≠ 0) (hd : d ≠ 0) (hpz : ¬p ∣ z) (hpd : ¬p ∣ d) : padicValRat p (↑z / ↑d) = 0

theorem Zeta32.PrimeEdge.not_dvd_of_prime_factor {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℕ} (hq : Nat.Prime q) (hpq : p ≠ q) : ¬p ∣ q

theorem Zeta32.PrimeEdge.not_dvd_two_three_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (hp7 : 7 ≤ p) (a b : ℕ) : ¬p ∣ 2 ^ a * 3 ^ b

theorem Zeta32.PrimeEdge.VG_of_mul_int {p : ℕ} [hp : Fact (Nat.Prime p)] (hp7 : 7 ≤ p) {q : ℚ} (z : ℤ) (hq : q * 1296 = ↑z) : Zeta5Irrational.VG p q 0

theorem Zeta32.PrimeEdge.zeroMoment_int (i : Fin 7) : ∃ (z : ℤ), zeroMoment i * 1296 = ↑z

theorem Zeta32.PrimeEdge.lowMoment_int (i : Fin 5) : ∃ (z : ℤ), lowMoment i * 1296 = ↑z

theorem Zeta32.PrimeEdge.highMoment_int (i : Fin 3) : ∃ (z : ℤ), highMoment i * 1296 = ↑z

theorem Zeta32.PrimeEdge.blockMoment_VG {p : ℕ} [Fact (Nat.Prime p)] (hp7 : 7 ≤ p) (b e : ℕ) (he : e + 1 < 2 * mult p b) : Zeta5Irrational.VG p (blockMoment p b e) 0

S2b-4'. The fixed moments in the range used by one class block are p-integral for p ≥ 7 (denominators divide 2⁴3⁴).

theorem Zeta32.PrimeEdge.unit_of_ratio {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {z1 z2 d : ℕ} (hq : q = -↑(z1 * z2) / ↑d) (h1 : Nat.Prime z1) (h2 : Nat.Prime z2) (hp1 : p ≠ z1) (hp2 : p ≠ z2) (hd : d ≠ 0) (hpd : ¬p ∣ d) : q ≠ 0 ∧ padicValRat p q = 0

theorem Zeta32.PrimeEdge.hankelDet_unit {p : ℕ} [Fact (Nat.Prime p)] (hp7 : 7 ≤ p) (hE : p ∉ exceptional) (b : Fin p) : hankelDet p b ≠ 0 ∧ padicValRat p (hankelDet p b) = 0

S3c. The three fixed determinants are p-adic units for p ≥ 7, p ∉ exceptional.

theorem Zeta32.PrimeEdge.refUnit_unit {p : ℕ} [hp : Fact (Nat.Prime p)] (hp7 : 7 ≤ p) (hE : p ∉ exceptional) (w : ℕ → ℚ) (hw : ∀ b < p, w b ≠ 0 ∧ padicValRat p (w b) = 0) : refUnit p w ≠ 0 ∧ padicValRat p (refUnit p w) = 0

S3. The reference unit is a p-adic unit when all w_b are.