the proof notes, §4 Lemma 5 and §8.2 Lemma 9: for every prime p with 7n < 3p ≤ 15n, p ∤ den r, cost r n p ≤ n φ(p/n) + 5. The Gauss bound outer_valuation_bound is Lemma 5 with the class costs of Lemma 9 inserted; the arithmetic comparison with n φ(p/n) is outer_arith. Both hold for every n (the hypotheses force n ≥ 1, p ≥ 3, p > 2n, p² > 5n); outer_per_prime_bound is the eventual form used by Arith.arith_of_parts.

theorem Zeta32.Outer.cost_le_of_GV {r : ℚ} {n p : ℕ} {B : ℚ} (hQ : Qtilde r n ≠ 0) (h : Zeta5Irrational.GV p (Qtilde r n) B) : cost r n p ≤ -↑B

cost is bounded by minus any Gauss lower bound of the nonzero Qtilde.

theorem Zeta32.Outer.Qtilde_ne_zero {r : ℚ} {n : ℕ} (hQ : Q r n ≠ 0) : Qtilde r n ≠ 0

def Zeta32.Arith.outerClassBound (n p : ℕ) : ℚ

The outer class sum, Σ_c gcl, in closed form.

Equations

• Zeta32.Arith.outerClassBound n p = -4 - ↑(5 * n - 2 * p) - 4 * ↑(min (p - 1 - n) (5 * n - p - n))

theorem Zeta32.Arith.outer_valuation_bound (r : ℚ) (n p : ℕ) (hp : Nat.Prime p) (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) (hden : ¬p ∣ r.den) : Zeta5Irrational.GV p (Qtilde r n) (Outer.normVal p n + outerClassBound n p - ↑(5 * n + 1 - p))

the proof notes, Lemma 5 (with Lemma 9's class costs) in the outer range: every coefficient of Qtilde r n has v_p ≥ normVal + Σ_classes - r_p, r_p = 5n + 1 - p.

theorem Zeta32.Arith.outer_arith (n p : ℕ) (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) : -↑(Outer.normVal p n + outerClassBound n p - ↑(5 * n + 1 - p)) ≤ ↑n * ArithSum.phiL (↑p / ↑n) + 5

The comparison of Lemma 9 with n φ(p/n) + 5, term by term on the four pieces of φ.

theorem Zeta32.Arith.outer_cost_bound (r : ℚ) (n p : ℕ) (hp : Nat.Prime p) (h73 : 7 * n < 3 * p) (hp5 : p ≤ 5 * n) (hden : ¬p ∣ r.den) (hQ : Q r n ≠ 0) : cost r n p ≤ ↑n * ArithSum.phiL (↑p / ↑n) + 5

Lemma 9 for one prime: cost r n p ≤ n φ(p/n) + 5 for every n.

theorem Zeta32.Arith.outer_per_prime_bound (r : ℚ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ), Nat.Prime p → 7 * n < 3 * p → p ≤ 5 * n → ¬p ∣ r.den → Q r n ≠ 0 → cost r n p ≤ ↑n * ArithSum.phiL (↑p / ↑n) + 5

the proof notes, §8.2, Lemma 9, in the form used by ArithSum.arith_sum (hypothesis h2).