The arithmetic node (the proof notes, §8 opening and §9): from the per-prime bounds (taken as hypotheses) and ArithSum.arith_sum, ∀ ε > 0, ∀ᶠ n, Q r n ≠ 0 → log d_n ≤ (283/50 + ε) n².

Bridge: for Q r n ≠ 0, P = d Q is primitive, so v_p(d) = −min_k v_p(Q_k) = cost r n p for every prime p, and log d = Σ_p v_p(d) log p over any finite set of primes containing the support. Primes p > 5n have cost ≤ 0 (large-prime integrality; for n ≥ den r no such prime divides den r). For Q r n = 0 the definition of cost is irrelevant (the conclusion is vacuous); arith_sum is applied to costQ, which equals cost when Q r n ≠ 0 and is below every hypothesis bound when Q r n = 0.

Logarithm of a positive rational as a finite prime sum

def Zeta32.Arith.ratPrimeSupport (s : ℚ) : Finset ℕ

Prime divisors of the numerator or denominator of a rational number.

Equations

• Zeta32.Arith.ratPrimeSupport s = s.num.natAbs.factorization.support ∪ s.den.factorization.support

theorem Zeta32.Arith.ratPrimeSupport_prime {s : ℚ} {p : ℕ} (hp : p ∈ ratPrimeSupport s) : Nat.Prime p

theorem Zeta32.Arith.padicValRat_eq_factorizations (p : ℕ) (hp : Nat.Prime p) (s : ℚ) : padicValRat p s = ↑(s.num.natAbs.factorization p) - ↑(s.den.factorization p)

theorem Zeta32.Arith.padicValRat_eq_zero_of_not_mem_ratPrimeSupport {s : ℚ} {p : ℕ} (hp : Nat.Prime p) (hnot : p ∉ ratPrimeSupport s) : padicValRat p s = 0

theorem Zeta32.Arith.log_nat_eq_sum_of_support_subset (n : ℕ) (S : Finset ℕ) (hS : n.factorization.support ⊆ S) : Real.log ↑n = ∑ p ∈ S, ↑(n.factorization p) * Real.log ↑p

theorem Zeta32.Arith.log_rat_eq_sum_padicValRat {s : ℚ} (hs : 0 < s) : Real.log ↑s = ∑ p ∈ ratPrimeSupport s, ↑(padicValRat p s) * Real.log ↑p

theorem Zeta32.Arith.log_rat_eq_sum_padicValRat_of_support_subset {s : ℚ} (hs : 0 < s) (S : Finset ℕ) (hS : ratPrimeSupport s ⊆ S) (hprime : ∀ p ∈ S, Nat.Prime p) : Real.log ↑s = ∑ p ∈ S, ↑(padicValRat p s) * Real.log ↑p

Primitive content: v_p(d) = −min_k v_p(Q_k)

theorem Zeta32.Arith.primitive_exists_coeff_not_dvd (p : ℕ) [hp : Fact (Nat.Prime p)] (T : Polynomial ℤ) (hT : T.IsPrimitive) : ∃ (k : ℕ), ¬↑p ∣ T.coeff k

theorem Zeta32.Arith.primitive_scale_coeff_valuation_minimum (p : ℕ) [Fact (Nat.Prime p)] (T : Polynomial ℤ) (hT : T.IsPrimitive) (F : Polynomial ℚ) (s : ℚ) (hs : s ≠ 0) (hprop : Polynomial.map (algebraMap ℤ ℚ) T = Polynomial.C s * F) : ∃ (k : ℕ), F.coeff k ≠ 0 ∧ padicValRat p (F.coeff k) = -padicValRat p s ∧ ∀ (j : ℕ), F.coeff j ≠ 0 → padicValRat p (F.coeff k) ≤ padicValRat p (F.coeff j)

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

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

theorem Zeta32.Arith.cost_eq_padicValRat_dtilde (r : ℚ) (n p : ℕ) (hp : Nat.Prime p) (hQ : Q r n ≠ 0) : cost r n p = ↑(padicValRat p (dtilde r n))

For Q r n ≠ 0, cost r n p = v_p(d).

theorem Zeta32.Arith.cost_le_of_forall (r : ℚ) (n p : ℕ) (hQ : Q r n ≠ 0) (b : ℝ) (h : ∀ (k : ℕ), (Qtilde r n).coeff k ≠ 0 → b ≤ ↑(padicValRat p ((Qtilde r n).coeff k))) : cost r n p ≤ -b

A uniform lower bound on the coefficient valuations bounds cost from above.

theorem Zeta32.Arith.log_dtilde_le_sum (r : ℚ) (n : ℕ) (hQ : Q r n ≠ 0) (hlarge : ∀ (p : ℕ), Nat.Prime p → 5 * n < p → cost r n p ≤ 0) : Real.log ↑(dtilde r n) ≤ ∑ p ∈ Finset.range (5 * n + 1) with Nat.Prime p, cost r n p * Real.log ↑p

For Q r n ≠ 0 and cost ≤ 0 beyond 5n: log d ≤ Σ_{p ≤ 5n} cost_p log p.

The node

noncomputable def Zeta32.Arith.costQ (r : ℚ) (n p : ℕ) : ℝ

cost, patched on Q r n = 0 (where the conclusion of the node is vacuous) to lie below every per-prime bound.

Equations

• Zeta32.Arith.costQ r n p = if Zeta32.Q r n = 0 then min (↑n * Zeta32.ArithSum.psiL (↑p / ↑n) + 3 / 4) (min (↑n * Zeta32.ArithSum.phiL (↑p / ↑n) + 5) 0) else Zeta32.cost r n p

theorem Zeta32.Arith.rpow_third {x : ℝ} (hx : 0 < x) : x ^ (2 / 3) = (x ^ (1 / 3)) ^ 2 ∧ x = (x ^ (1 / 3)) ^ 3

theorem Zeta32.Arith.arith_of_parts (r : ℚ) : (∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ), Nat.Prime p → ↑n ^ (2 / 3) < ↑p → p ≤ 5 * n → ¬p ∣ r.den → GreedyBound r n p) → (∀ (n p : ℕ), Nat.Prime p → 7 ≤ p → 5 * n < p ^ 2 → Q r n ≠ 0 → 3 * p ≤ 7 * n → GreedyBound r n p → cost r n p ≤ ↑n * ArithSum.psiL (↑p / ↑n) + 3 / 4) → (∀ᶠ (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) → (∀ (n p : ℕ), Nat.Prime p → 5 * n < p → ¬p ∣ r.den → ∀ (k : ℕ), (Qtilde r n).coeff k ≠ 0 → 0 ≤ padicValRat p ((Qtilde r n).coeff k)) → (∀ (n p : ℕ), Nat.Prime p → ∀ (k : ℕ), (Qtilde r n).coeff k ≠ 0 → padicValRat p ((Qtilde r n).coeff k) ≥ -3 * (3 * ↑n) * ↑(Nat.log p (10 * n + 2)) - 3 * ↑n * ↑(padicValNat p r.den)) → ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, Q r n ≠ 0 → Real.log ↑(dtilde r n) ≤ (283 / 50 + ε) * ↑n ^ 2