The modulus \(Q_9 = 210\) to The grid function reaches \(2\) at \(657\)

DefinitionThe modulus \(Q_9 = 210\)#✓fully proved

For the \(k = 9\) case of Breusch's argument, the truncation modulus is the natural number \(Q_9 = 2 \cdot 3 \cdot 5 \cdot 7 = 210\).

def Q9 : ℕ := 210

Used by 48

Used byThe divisor table for \(210\) lists every divisor · Entries of the divisor table for \(210\) divide \(210\) · Scaled factorial argument \(N_{10}\) · Scaled factorial argument \(N_1\) · Scaled factorial argument N₉ · Value of Q₉ · Q₉ is positive · Quotients of Q₉ by its divisors are positive · Divisors of 210 divide multiples of 210 · 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\) · 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}\) · 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₉ · Closed form of the Möbius-weighted main-term sum · Lower bound for \(\log F_9(n)\) · Exact formula for the scaled factorial argument \(N_1\) · Exact formula for the scaled factorial argument \(N_9\) · Combined main term of the Möbius-weighted Stirling sums · One-period shift of \(G_9\) · Continuous Breusch function · Legendre terms of \(N_1\) as real floors · Legendre terms of \(N_{10}\) as real floors · Legendre terms of \(N_9\) as real floors · 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 · The continuous Breusch function vanishes at small ratios · Valuation of a factorial ratio as a difference of valuations · Single-term valuation identity for large primes · Valuation identity for the weighted product · Value of \(10Qn\) · 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 · Primes up to \(1890n\) have \(n/p \ge 1/1890\) · Contribution of primes with \(p^2 > 2100n\) · Bound for one small-square prime term

DefinitionThe Möbius divisor table for \(210\)#✓fully proved

\(W_9\) is the list of pairs of a natural number and an integer \((1, 1), (2, -1), (3, -1), (5, -1), (6, 1), (7, -1), (10, 1), (14, 1), (15, 1), (21, 1),\) \((30, -1), (35, 1), (42, -1), (70, -1), (105, -1), (210, 1)\), in this order. It pairs each divisor \(d\) of \(210\) with its Möbius value \(\mu(d)\).

def w9 : List (ℕ × ℤ) :=
  [(1, 1), (2, -1), (3, -1), (5, -1), (6, 1), (7, -1), (10, 1), (14, 1),
   (15, 1), (21, 1), (30, -1), (35, 1), (42, -1), (70, -1), (105, -1),
   (210, 1)]

Used by 24

Used byBreusch grid function for \(k = 9\) · The divisor table for \(210\) lists every divisor · Entries of the divisor table for \(210\) divide \(210\) · The divisor table for \(210\) has 16 entries · Divisors in the table for \(210\) are positive · Logarithm of Breusch's product \(F_9(n)\) · Signs in the divisor table for \(210\) · The divisor table for \(210\) has no repeated entries · Divisors of 210 divide multiples of 210 · The constant \(K_9\) · Termwise Stirling lower bound in Breusch's argument · Möbius reciprocal sum over the divisors of 210, in the rationals · Möbius reciprocal sum over the divisors of 210, in the reals · Closed form of the Möbius-weighted main-term sum · Lower bound for \(\log F_9(n)\) · Combined main term of the Möbius-weighted Stirling sums · One-period shift of \(G_9\) · Continuous Breusch function · The continuous Breusch function agrees with the grid function · The \(p\)-adic valuation of the weighted product · Valuation identity for the weighted product · Prime factorization of \(\log F_9(n)\) · A weighted log-factor as a sum over primes · Bound on the prime factors of the ratio factors

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

The Möbius divisor table \(W_9\) for \(210\) is a list of length \(16\).

lemma w9_length : w9.length = 16

Uses 1 · Used by 1

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

Used byLower bound for \(\log F_9(n)\)

LemmaThe divisor table for \(210\) lists every divisor#✓fully proved

The set of first components \(d\) of the pairs \((d, \varepsilon)\) in the Möbius divisor table \(W_9\) is exactly the set of divisors of \(Q_9 = 210\).

lemma w9_complete : (w9.map Prod.fst).toFinset = Nat.divisors Q9

Uses 2

Statement usesThe modulus \(Q_9 = 210\) · The Möbius divisor table for \(210\)

LemmaDivisors in the table for \(210\) are positive#✓fully proved

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

lemma w9_pos : ∀ p ∈ w9, 1 ≤ p.1

Uses 1 · Used by 7

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

Used byTermwise Stirling lower bound in Breusch's argument · Closed form of the Möbius-weighted main-term sum · Lower bound for \(\log F_9(n)\) · One-period shift of \(G_9\) · Valuation identity for the weighted product · A weighted log-factor as a sum over primes · Bound on the prime factors of the ratio factors

LemmaEntries of the divisor table for \(210\) divide \(210\)#✓fully proved

For every pair \((d, \varepsilon)\) in the Möbius divisor table \(W_9\), \(d\) divides \(Q_9 = 210\).

lemma w9_dvd : ∀ p ∈ w9, p.1 ∣ Q9

Uses 2 · Used by 8

Statement usesThe modulus \(Q_9 = 210\) · The Möbius divisor table for \(210\)

Used byDivisors of 210 divide multiples of 210 · Termwise Stirling lower bound in Breusch's argument · Lower bound for \(\log F_9(n)\) · One-period shift of \(G_9\) · The continuous Breusch function agrees with the grid function · Valuation identity for the weighted product · A weighted log-factor as a sum over primes · Bound on the prime factors of the ratio factors

DefinitionSummand of the Breusch grid function#✓fully proved

For a natural number \(d\), an integer \(m\) and a natural number \(j\), the summand of the pair \((d, m)\) at \(j\) is the integer

\[ m \Bigl( \Bigl\lfloor \frac{10 \cdot 210 \cdot j}{18900\, d} \Bigr\rfloor - \Bigl\lfloor \frac{9 \cdot 210 \cdot j}{18900\, d} \Bigr\rfloor - \Bigl\lfloor \frac{210 \cdot j}{18900\, d} \Bigr\rfloor \Bigr), \]

where each floor is a quotient in natural-number division (equal to \(0\) when \(d = 0\)) and the differences are taken in the integers.

def G9term (q : ℕ × ℤ) (j : ℕ) : ℤ :=
  q.2 * (((10 * 210 * j / (q.1 * 18900) : ℕ) : ℤ)
    - ((9 * 210 * j / (q.1 * 18900) : ℕ) : ℤ)
    - ((210 * j / (q.1 * 18900) : ℕ) : ℤ))

Used by 3

Used byBreusch grid function for \(k = 9\) · One-period shift of \(G_9\) · The continuous Breusch function agrees with the grid function

DefinitionBreusch grid function for \(k = 9\)#✓fully proved

For a natural number \(j\), \(G_9(j)\) is the integer

\[ G_9(j) = \sum_{d \mid 210} \mu(d) \Bigl( \Bigl\lfloor \frac{10 \cdot 210 \cdot j}{18900\, d} \Bigr\rfloor - \Bigl\lfloor \frac{9 \cdot 210 \cdot j}{18900\, d} \Bigr\rfloor - \Bigl\lfloor \frac{210 \cdot j}{18900\, d} \Bigr\rfloor \Bigr), \]

where \(\mu\) is the Möbius function, the sum runs over the \(16\) positive divisors \(d\) of \(210 = 2 \cdot 3 \cdot 5 \cdot 7\), each floor is a quotient of natural numbers, and the differences are taken in the integers.

The sum runs over an explicit table of the divisors of \(210\) with their Möbius values.

def G9 (j : ℕ) : ℤ := (w9.map (fun q => G9term q j)).sum

Uses 2 · Used by 29

Statement usesSummand of the Breusch grid function · The Möbius divisor table for \(210\)

Used byFirst index from \(10\) where the grid function reaches \(1\) · The grid function reaches \(1\) at \(279\) · The grid function stays below \(1\) on \((10, 279)\) · The grid function reaches \(2\) at \(657\) · Grid bound \(G_9 \le 3\) for \(0 \le j < 2700\) · Grid bound \(G_9 \le 3\) for \(2700 \le j < 5400\) · Grid bound \(G_9 \le 3\) for \(5400 \le j < 8100\) · Grid bound \(G_9 \le 3\) for \(8100 \le j < 10800\) · Grid bound \(G_9 \le 3\) for \(10800 \le j < 13500\) · Grid bound \(G_9 \le 3\) for \(13500 \le j < 16200\) · Grid bound \(G_9 \le 3\) for \(16200 \le j < 18900\) · Grid bound \(G_9 \le 3\) · First index from \(10\) where the grid function reaches \(2\) · The grid function stays below \(2\) on \((10, 657)\) · First index from 10 on with grid value at least 3 · The grid function reaches \(3\) at \(963\) · The grid function stays below \(3\) on \((10, 963)\) · One-period shift of \(G_9\) · Value of \(G_9\) at \(9\) · \(G_9\) depends only on the residue modulo \(18900\) · Periodicity of \(G_9\) in multiples of \(18900\) · Bound \(G_9 \le 1\) below \(10\) · The Breusch grid function vanishes below 9 · The continuous Breusch function agrees with the grid function · The continuous Breusch function is at most 3 · 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

LemmaGrid bound \(G_9 \le 3\) for \(0 \le j < 2700\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(0 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j < 2700\).

lemma M9_block0 : ∀ k < 2700, G9 (0 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

LemmaGrid bound \(G_9 \le 3\) for \(2700 \le j < 5400\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(2700 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j\) with \(2700 \le j < 5400\).

lemma M9_block1 : ∀ k < 2700, G9 (2700 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

LemmaGrid bound \(G_9 \le 3\) for \(5400 \le j < 8100\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(5400 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j\) with \(5400 \le j < 8100\).

lemma M9_block2 : ∀ k < 2700, G9 (5400 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

LemmaGrid bound \(G_9 \le 3\) for \(8100 \le j < 10800\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(8100 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j\) with \(8100 \le j < 10800\).

lemma M9_block3 : ∀ k < 2700, G9 (8100 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

LemmaGrid bound \(G_9 \le 3\) for \(10800 \le j < 13500\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(10800 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j\) with \(10800 \le j < 13500\).

lemma M9_block4 : ∀ k < 2700, G9 (10800 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

LemmaGrid bound \(G_9 \le 3\) for \(13500 \le j < 16200\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(13500 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j\) with \(13500 \le j < 16200\).

lemma M9_block5 : ∀ k < 2700, G9 (13500 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

LemmaGrid bound \(G_9 \le 3\) for \(16200 \le j < 18900\)#✓fully proved

For every natural number \(k < 2700\), the grid function satisfies \(G_9(16200 + k) \le 3\); that is, \(G_9(j) \le 3\) for all natural numbers \(j\) with \(16200 \le j < 18900\).

lemma M9_block6 : ∀ k < 2700, G9 (16200 + k) ≤ 3

Uses 1 · Used by 1

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

Used byGrid bound \(G_9 \le 3\)

TheoremGrid bound \(G_9 \le 3\)#✓fully proved

For every natural number \(j < 18900\), the grid function satisfies \(G_9(j) \le 3\).

theorem M9_le : ∀ j < 18900, G9 j ≤ 3

Uses 8 · Used by 1

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

Proof usesGrid bound \(G_9 \le 3\) for \(0 \le j < 2700\) · Grid bound \(G_9 \le 3\) for \(2700 \le j < 5400\) · Grid bound \(G_9 \le 3\) for \(5400 \le j < 8100\) · Grid bound \(G_9 \le 3\) for \(8100 \le j < 10800\) · Grid bound \(G_9 \le 3\) for \(10800 \le j < 13500\) · Grid bound \(G_9 \le 3\) for \(13500 \le j < 16200\) · Grid bound \(G_9 \le 3\) for \(16200 \le j < 18900\)

Used byThe continuous Breusch function is at most 3

TheoremThe grid function reaches \(1\) at \(279\)#✓fully proved

The Breusch grid function \(G_9\) for \(k = 9\) satisfies \(G_9(279) \ge 1\).

theorem jmin1_attained : G9 279 ≥ 1

Uses 1 · Used by 1

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

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

TheoremThe grid function stays below \(1\) on \((10, 279)\)#✓fully proved

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

theorem jmin1_core : ∀ j < 279, 10 ≤ j → G9 j < 1

Uses 1 · Used by 1

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

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

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

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

theorem jmin1 : G9 279 ≥ 1 ∧ ∀ j, 10 ≤ j → j < 279 → G9 j < 1

Uses 3 · Used by 1

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

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

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

TheoremThe grid function reaches \(2\) at \(657\)#✓fully proved

The Breusch grid function \(G_9\) for \(k = 9\) satisfies \(G_9(657) \ge 2\).

theorem jmin2_attained : G9 657 ≥ 2

Uses 1 · Used by 1

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

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

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.