The grid function stays below \(2\) on \((10, 657)\) to Quotients of Q₉ by its divisors are positive

TheoremThe grid function stays below \(2\) on \((10, 657)\)#✓fully proved

For every natural number \(j\) with \(10 \le j < 657\), the Breusch grid function \(G_9\) for \(k = 9\) satisfies \(G_9(j) < 2\).

theorem jmin2_core : ∀ j < 657, 10 ≤ j → G9 j < 2

Uses 1 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Used byFirst index from \(10\) where the grid function reaches \(2\)

TheoremFirst index from \(10\) where the grid function reaches \(2\)#✓fully proved

The Breusch grid function \(G_9\) for \(k = 9\) satisfies \(G_9(657) \ge 2\), and \(G_9(j) < 2\) for every natural number \(j\) with \(10 \le j < 657\). So \(657\) is the least \(j \ge 10\) with \(G_9(j) \ge 2\).

theorem jmin2 : G9 657 ≥ 2 ∧ ∀ j, 10 ≤ j → j < 657 → G9 j < 2

Uses 3 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Proof usesThe grid function reaches \(2\) at \(657\) · The grid function stays below \(2\) on \((10, 657)\)

Used byLevel-\(2\) threshold for the continuous Breusch function

TheoremThe grid function reaches \(3\) at \(963\)#✓fully proved

The Breusch grid function \(G_9\) for \(k = 9\) satisfies \(G_9(963) \ge 3\).

theorem jmin3_attained : G9 963 ≥ 3

Uses 1 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Used byFirst index from 10 on with grid value at least 3

TheoremThe grid function stays below \(3\) on \((10, 963)\)#✓fully proved

For every natural number \(j\) with \(10 \le j < 963\), the Breusch grid function \(G_9\) for \(k = 9\) satisfies \(G_9(j) < 3\).

theorem jmin3_core : ∀ j < 963, 10 ≤ j → G9 j < 3

Uses 1 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Used byFirst index from 10 on with grid value at least 3

TheoremFirst index from 10 on with grid value at least 3#✓fully proved

The grid function \(G_9\) satisfies \(G_9(963) \ge 3\), and \(G_9(j) < 3\) for every natural number \(j\) with \(10 \le j < 963\).

theorem jmin3 : G9 963 ≥ 3 ∧ ∀ j, 10 ≤ j → j < 963 → G9 j < 3

Uses 3 · Used by 1

Statement usesBreusch grid function for \(k = 9\)

Proof usesThe grid function reaches \(3\) at \(963\) · The grid function stays below \(3\) on \((10, 963)\)

Used byLevel-\(3\) threshold for the continuous Breusch function

LemmaSigns in the divisor table for \(210\)#✓fully proved

For every pair \((d, \varepsilon)\) in the Möbius divisor table \(W_9\) for \(210\), \(\varepsilon = 1\) or \(\varepsilon = -1\).

lemma w9_mu_sign : ∀ q ∈ w9, q.2 = 1 ∨ q.2 = -1

Uses 1 · Used by 1

Statement usesThe Möbius divisor table for \(210\)

Used byTermwise Stirling lower bound in Breusch's argument

LemmaThe divisor table for \(210\) has no repeated entries#✓fully proved

No pair \((d, \varepsilon)\) occurs more than once in the list \(W_9\), the Möbius divisor table for \(210\).

lemma w9_nodup : w9.Nodup

Uses 1 · Used by 4

Statement usesThe Möbius divisor table for \(210\)

Used byMöbius reciprocal sum over the divisors of 210, in the rationals · Lower bound for \(\log F_9(n)\) · One-period shift of \(G_9\) · The continuous Breusch function agrees with the grid function

LemmaSum over a duplicate-free list#✓fully proved

Let \(M\) be an additive commutative monoid, let \(l\) be a list of elements of \(\mathbb{N} \times \mathbb{Z}\) with no repeated entries, and let \(f : \mathbb{N} \times \mathbb{Z} \to M\). Then the sum of the values of \(f\) along \(l\) equals the sum of \(f\) over the finite set of entries of \(l\).

lemma map_sum_toFinset {M : Type*} [AddCommMonoid M] (l : List (ℕ × ℤ)) (hl : l.Nodup)
    (f : (ℕ × ℤ) → M) : (l.map f).sum = l.toFinset.sum f

Used by 3

Used byMöbius reciprocal sum over the divisors of 210, in the rationals · One-period shift of \(G_9\) · The continuous Breusch function agrees with the grid function

LemmaExponential bound by the geometric series#✓fully proved

For every real number \(u\) with \(0 \le u < 1\), \(e^u \le \frac{1}{1 - u}\).

lemma exp_le_inv_one_sub {u : ℝ} (h0 : 0 ≤ u) (h1 : u < 1) :
    Real.exp u ≤ 1 / (1 - u)

Used by 1

Used byLogarithm is at least 1 − 1/t

LemmaLogarithm is at least 1 − 1/t#✓fully proved

For every real number \(t \ge 1\), \(1 - 1/t \le \log t\).

lemma one_sub_inv_le_log {t : ℝ} (ht : 1 ≤ t) : 1 - 1 / t ≤ Real.log t

Uses 1 · Used by 1

Proof usesExponential bound by the geometric series

Used byWeak Stirling upper bound for factorials

LemmaWeak Stirling lower bound for factorials#✓fully proved

For every natural number \(n \ge 1\), \(n^n e^{1-n} \le n!\).

lemma stirling_lower {n : ℕ} (hn : 1 ≤ n) :
    (n : ℝ) ^ n * Real.exp (-(n : ℝ) + 1) ≤ (Nat.factorial n : ℝ)

Used by 1

Used byLower bound for \(\log N!\)

LemmaWeak Stirling upper bound for factorials#✓fully proved

For every natural number \(n \ge 1\), \(n! \le n^{n+1} e^{1-n}\).

lemma stirling_upper {n : ℕ} (hn : 1 ≤ n) :
    (Nat.factorial n : ℝ) ≤ (n : ℝ) ^ (n + 1) * Real.exp (-(n : ℝ) + 1)

Uses 1 · Used by 1

Proof usesLogarithm is at least 1 − 1/t

Used byUpper bound for \(\log N!\)

DefinitionScaled factorial argument \(N_{10}\)#✓fully proved

Let \(Q_9 = 2 \cdot 3 \cdot 5 \cdot 7 = 210\). For natural numbers \(m\) and \(n\), \(N_{10}(m, n)\) is the natural number \(10 n \lfloor Q_9 / m \rfloor\), where \(\lfloor Q_9 / 0 \rfloor\) is taken to be \(0\).

def N10m (m n : ℕ) : ℕ := 10 * n * (Q9 / m)

Uses 1 · Used by 17

Statement usesThe modulus \(Q_9 = 210\)

Used byBinomial factor ratio₉ · Termwise Stirling lower bound in Breusch's argument · Logarithm of the binomial factor · Exact formula for the scaled factorial argument \(N_{10}\) · Upper bound for the scaled factorial argument \(N_{10}\) · Positivity of the scaled factorial argument \(N_{10}\) · N₁₀ splits as N₉ + N₁ · Factorial divisibility behind ratio₉ · Positivity of ratio₉ · Lower bound for \(\log F_9(n)\) · Legendre terms of \(N_{10}\) as real floors · One divisor's contribution to the valuation · Valuation of a factorial ratio as a difference of valuations · Valuation identity for the weighted product · Valuation term of one binomial factor · Valuation terms vanish off the prime support · Bound on the prime factors of the ratio factors

DefinitionScaled factorial argument N₉#✓fully proved

For natural numbers \(m\) and \(n\), \(N_9(m, n) = 9n \lfloor Q_9 / m \rfloor\), where \(Q_9 = 210\) and \(\lfloor Q_9 / m \rfloor\) is the quotient of natural-number division, taken to be \(0\) when \(m = 0\).

def N9m (m n : ℕ) : ℕ := 9 * n * (Q9 / m)

Uses 1 · Used by 17

Statement usesThe modulus \(Q_9 = 210\)

Used byBinomial factor ratio₉ · Termwise Stirling lower bound in Breusch's argument · Logarithm of the binomial factor · Upper bound for the scaled factorial argument \(N_9\) · Positivity of the scaled argument N₉ · N₁₀ splits as N₉ + N₁ · Factorial divisibility behind ratio₉ · Positivity of ratio₉ · Lower bound for \(\log F_9(n)\) · Exact formula for the scaled factorial argument \(N_9\) · Legendre terms of \(N_9\) as real floors · One divisor's contribution to the valuation · Valuation of a factorial ratio as a difference of valuations · Valuation identity for the weighted product · Valuation term of one binomial factor · Valuation terms vanish off the prime support · Bound on the prime factors of the ratio factors

DefinitionScaled factorial argument \(N_1\)#✓fully proved

Let \(Q_9 = 2 \cdot 3 \cdot 5 \cdot 7 = 210\). For natural numbers \(m\) and \(n\), \(N_1(m, n)\) is the natural number \(n \lfloor Q_9 / m \rfloor\), where \(\lfloor Q_9 / 0 \rfloor\) is taken to be \(0\).

def N1m (m n : ℕ) : ℕ := n * (Q9 / m)

Uses 1 · Used by 17

Statement usesThe modulus \(Q_9 = 210\)

Used byBinomial factor ratio₉ · Termwise Stirling lower bound in Breusch's argument · Logarithm of the binomial factor · Upper bound for the scaled factorial argument \(N_1\) · Positivity of the scaled factorial argument \(N_1\) · N₁₀ splits as N₉ + N₁ · Factorial divisibility behind ratio₉ · Positivity of ratio₉ · Lower bound for \(\log F_9(n)\) · Exact formula for the scaled factorial argument \(N_1\) · Legendre terms of \(N_1\) as real floors · One divisor's contribution to the valuation · Valuation of a factorial ratio as a difference of valuations · Valuation identity for the weighted product · Valuation term of one binomial factor · Valuation terms vanish off the prime support · Bound on the prime factors of the ratio factors

DefinitionBinomial factor ratio₉#✓fully proved

For natural numbers \(m\) and \(n\), \(\mathrm{ratio}_9(m, n) = N_{10}(m, n)! / (N_9(m, n)! \cdot N_1(m, n)!)\), with natural-number division, where \(N_k(m, n) = kn \lfloor Q_9 / m \rfloor\) for \(k = 1, 9, 10\) and \(Q_9 = 210\) (the quotient \(\lfloor Q_9 / m \rfloor\) is taken to be \(0\) when \(m = 0\)).

def ratio9 (m n : ℕ) : ℕ := (N10m m n)! / ((N9m m n)! * (N1m m n)!)

Uses 3 · Used by 10

Statement usesScaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉

Used byLogarithm of Breusch's product \(F_9(n)\) · Logarithm of the binomial factor · Positivity of ratio₉ · Lower bound for \(\log F_9(n)\) · Valuation of a factorial ratio as a difference of valuations · Prime factorization of \(\log F_9(n)\) · Valuation term of one binomial factor · Valuation terms vanish off the prime support · A weighted log-factor as a sum over primes · Bound on the prime factors of the ratio factors

DefinitionLogarithm of Breusch's product \(F_9(n)\)#✓fully proved

Let \(w_9\) be the table of divisors \(d\) of \(Q_9 = 210\) paired with their Möbius values \(\varepsilon\). For a natural number \(n\), writing \(k_d = 210/d\),

\[\log F_9(n) = \sum_{(d, \varepsilon) \in w_9} \varepsilon \log \frac{(10 n k_d)!}{(9 n k_d)!\,(n k_d)!}.\]

This is the logarithm of the Möbius-weighted product \(F_9(n)\) in Breusch's argument.

noncomputable def logF9 (n : ℕ) : ℝ :=
  w9.toFinset.sum (fun q : ℕ × ℤ => (q.2 : ℝ) * Real.log ((ratio9 q.1 n : ℕ) : ℝ))

Uses 2 · Used by 5

Statement usesBinomial factor ratio₉ · The Möbius divisor table for \(210\)

Used byLower bound for \(\log F_9(n)\) · Prime factorization of \(\log F_9(n)\) · Upper bound for \(\log F_9(n)\) when \((1890n, 2100n)\) has no prime · Endgame contradiction in Breusch's theorem · Breusch's endgame upper-bound inequality

LemmaQ₉ is positive#✓fully proved

The truncation modulus \(Q_9\) of the \(k = 9\) case satisfies \(0 < Q_9\).

lemma Q9_pos : 0 < Q9

Uses 1 · Used by 3

Statement usesThe modulus \(Q_9 = 210\)

Used byQuotients of Q₉ by its divisors are positive · Combined main term of the Möbius-weighted Stirling sums · The continuous Breusch function vanishes at small ratios

LemmaValue of Q₉#✓fully proved

The truncation modulus \(Q_9 = 2 \cdot 3 \cdot 5 \cdot 7\) of the \(k = 9\) case equals \(210\).

lemma Q9_eq : Q9 = 210

Uses 1 · Used by 10

Statement usesThe modulus \(Q_9 = 210\)

Used byLower bound for \(\log F_9(n)\) · Combined main term of the Möbius-weighted Stirling sums · One-period shift of \(G_9\) · The continuous Breusch function agrees with the grid function · Level-\(1\) threshold for the continuous Breusch function · Level-\(2\) threshold for the continuous Breusch function · Level-\(3\) threshold for the continuous Breusch function · The continuous Breusch function vanishes near zero · Value of \(10Qn\) · Bound on the prime factors of the ratio factors

LemmaQuotients of Q₉ by its divisors are positive#✓fully proved

For every natural number \(m \ge 1\) dividing \(Q_9 = 210\), the quotient \(Q_9 / m\) is at least \(1\).

lemma Q9div_pos {m : ℕ} (hm1 : 1 ≤ m) (hd : m ∣ Q9) : 1 ≤ Q9 / m

Uses 2 · Used by 3

Statement usesThe modulus \(Q_9 = 210\)

Proof usesQ₉ is positive

Used byPositivity of the scaled factorial argument \(N_1\) · Positivity of the scaled factorial argument \(N_{10}\) · Positivity of the scaled argument N₉

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.