Factorials that are Fibonacci integers

TheoremThe largest factorial that is a Fibonacci integer is \(36!\)#●ready to prove

For every natural number \(n\), the factorial \(n!\) lies in the subgroup of the multiplicative group \(\mathbb{Q}^\times\) generated by the Fibonacci numbers \(F_m\) with \(m \ge 1\) if and only if \(n \le 36\).

Calling a positive integer in this subgroup a Fibonacci integer, the statement records both the paper's claim that \(36!\) is a Fibonacci integer and that no \(n!\) with \(n \ge 37\) is.

public theorem_wanted factorial_mem_fibonacciIntegers_iff (n : ℕ) :
    (∃ u ∈ Subgroup.closure {u : ℚˣ | ∃ m : ℕ, 0 < m ∧ (u : ℚ) = Nat.fib m},
      (u : ℚ) = n.factorial) ↔ n ≤ 36

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Theorem 1.

TheoremCarmichael's congruence for primitive prime divisors of Fibonacci numbers#●ready to prove

Let \(F_n\) denote the \(n\)-th Fibonacci number. For every natural number \(m > 12\), every primitive prime divisor \(p\) of \(F_m\) (a prime \(p\) that divides \(F_m\) but divides no \(F_n\) with \(0 < n < m\)) satisfies \(p \equiv \pm 1 \pmod{m}\), that is, \(p \equiv 1 \pmod{m}\) or \(p + 1 \equiv 0 \pmod{m}\).

This is the congruence half of Carmichael's theorem; the existence of a primitive prime divisor of \(F_m\) for \(m > 12\) is a separate statement.

public theorem_wanted primitive_prime_dvd_fib_modEq_one_or_neg_one {m p : ℕ} (hm : 12 < m)
    (hp : IntegerSequence.IsPrimitivePrimeDivisor (fun n => (Nat.fib n : ℤ)) m p) :
    p ≡ 1 [MOD m] ∨ p + 1 ≡ 0 [MOD m]

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Theorem 2 (Primitive Divisor Theorem, quoting R. D. Carmichael).

Uses 1

Statement usesPrimitive prime divisor of an integer sequence

DefinitionEntry point in the Fibonacci sequence#✓fully proved

The entry point (rank of apparition) \(z(k)\) of a natural number \(k\) is the least \(m > 0\) such that \(k\) divides the Fibonacci number \(F_m\), and \(z(k) = 0\) if there is no such \(m\).

public noncomputable def fibEntryPoint (k : ℕ) : ℕ :=
  sInf {m : ℕ | 0 < m ∧ k ∣ Nat.fib m}

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2.

Used by 6

Used byBound on denominator indices of \(p\)-adic valuation one · Prime factors of the primitive parts of the denominator indices · Fibonacci entry point of \(5\) · Fibonacci entry point of \(2\) · Primitive part of a Fibonacci number · Primitive part of \(F_6\)

TheoremFibonacci entry point of \(2\)#✓fully proved

The least \(m > 0\) such that \(2\) divides the Fibonacci number \(F_m\) is \(3\), that is, the Fibonacci entry point of \(2\) is \(z(2) = 3\).

public theorem fibEntryPoint_two : fibEntryPoint 2 = 3

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2 (6 = 2 z(2)).

Uses 1 · Used by 1

Statement usesEntry point in the Fibonacci sequence

Used byPrimitive part of \(F_6\)

TheoremFibonacci entry point of \(5\)#✓fully proved

The least \(m > 0\) such that \(5\) divides the Fibonacci number \(F_m\) is \(5\), that is, the Fibonacci entry point of \(5\) is \(z(5) = 5\).

public theorem fibEntryPoint_five : fibEntryPoint 5 = 5

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2 (the exceptional index m = 5).

Uses 1

Statement usesEntry point in the Fibonacci sequence

DefinitionFibonacci cyclotomic values#✓fully proved

For a natural number \(m\), \(\Phi_m\) is the rational number \(\prod_{d \mid m} F_{m/d}^{\mu(d)}\), where \(d\) runs over the positive divisors of \(m\), \(F_k\) is the \(k\)-th Fibonacci number and \(\mu\) is the Möbius function. For \(m > 1\) this is the value \(\Phi_m(\alpha, \beta)\) of the homogenized \(m\)-th cyclotomic polynomial at the roots \(\alpha, \beta\) of \(x^2 - x - 1\).

At \(m = 1\) the formula gives \(1\), not \(\Phi_1(\alpha, \beta) = \alpha - \beta = \sqrt{5}\), and \(m = 0\) is treated as having no divisors, so \(\Phi_0 = 1\).

public noncomputable def fibCyclotomicValue (m : ℕ) : ℚ :=
  ∏ d ∈ m.divisors, (Nat.fib (m / d) : ℚ) ^ (ArithmeticFunction.moebius d)

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2.

Used by 3

Used byBound on denominator indices of \(p\)-adic valuation one · Prime factors of the primitive parts of the denominator indices · Fibonacci cyclotomic value at \(2\)

TheoremFibonacci cyclotomic value at \(2\)#✓fully proved

The Fibonacci cyclotomic value \(\Phi_2 = \prod_{d \mid 2} F_{2/d}^{\mu(d)} = F_2 / F_1\), where \(F_k\) is the \(k\)-th Fibonacci number and \(\mu\) is the Möbius function, equals \(1\).

public theorem fibCyclotomicValue_two : fibCyclotomicValue 2 = 1

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2, Equation (1).

Uses 1

Statement usesFibonacci cyclotomic values

DefinitionPrimitive part of a Fibonacci number#✓fully proved

For a natural number \(m\), the primitive part of the Fibonacci number \(F_m\) is \(\Psi_m = \prod_p p^{a_p}\), where the product runs over the primes \(p\) dividing \(F_m\) whose Fibonacci entry point is \(z(p) = m\), and \(a_p\) is the exponent of \(p\) in \(F_m\).

public noncomputable def fibPrimitivePart (m : ℕ) : ℕ :=
  ∏ p ∈ (Nat.fib m).primeFactors with fibEntryPoint p = m, p ^ (Nat.fib m).factorization p

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2.

Uses 1 · Used by 3

Statement usesEntry point in the Fibonacci sequence

Used byBound on denominator indices of \(p\)-adic valuation one · Prime factors of the primitive parts of the denominator indices · Primitive part of \(F_6\)

TheoremPrimitive part of \(F_6\)#✓fully proved

The primitive part of the Fibonacci number \(F_6\) is \(\Psi_6 = 1\): \(F_6 = 8 = 2^3\) and the Fibonacci entry point of \(2\) is \(z(2) = 3 \ne 6\), so \(F_6\) has no prime factor \(p\) with \(z(p) = 6\).

public theorem fibPrimitivePart_six : fibPrimitivePart 6 = 1

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Section 2.

Uses 3

Statement usesPrimitive part of a Fibonacci number

Proof usesEntry point in the Fibonacci sequence · Fibonacci entry point of \(2\)

TheoremPrime factors of the primitive parts of the denominator indices#●ready to prove

Let \(I\) and \(J\) be finite multisets of natural numbers, every element of which is at least \(3\) and different from \(6\) and \(12\), such that no element of \(I\) equals an element of \(J\) and \(\prod_{a \in I} \Phi_a / \prod_{b \in J} \Phi_b\) is a natural number, where \(\Phi_m\) is the \(m\)-th Fibonacci cyclotomic value. Let \(\Psi_m\) be the primitive part of the Fibonacci number \(F_m\) and \(z(p)\) the Fibonacci entry point of \(p\). Then there is a finite multiset \(e\) of pairs \((p, k)\) of natural numbers such that the multiset of first coordinates of \(e\) is the multiset of prime factors of \(\prod_{b \in J} \Psi_b\), counted with multiplicity, and the multiset of the numbers \(p^k z(p)\) for \((p, k) \in e\) is a sub-multiset of \(I\).

In other words, there is an injection from the prime factors \(p_1, \dots, p_r\) of \(\prod_{b \in J} \Psi_b\), counted with multiplicity, into \(I\) that sends each \(p_l\) to an element of the form \(p_l^{k_l} z(p_l)\).

public theorem_wanted exists_injection_primeFactors_fibPrimitivePart (I J : Multiset ℕ)
    (hI : ∀ n ∈ I, 3 ≤ n ∧ n ≠ 6 ∧ n ≠ 12) (hJ : ∀ m ∈ J, 3 ≤ m ∧ m ≠ 6 ∧ m ≠ 12)
    (hIJ : ∀ n ∈ I, ∀ m ∈ J, n ≠ m)
    (hnat : ∃ N : ℕ, (I.map fibCyclotomicValue).prod / (J.map fibCyclotomicValue).prod = N) :
    ∃ e : Multiset (ℕ × ℕ),
      e.map Prod.fst = ((J.map fibPrimitivePart).prod.primeFactorsList : Multiset ℕ) ∧
        e.map (fun pk => pk.1 ^ pk.2 * fibEntryPoint pk.1) ≤ I

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Lemma 1.

Uses 3

Statement usesFibonacci cyclotomic values · Entry point in the Fibonacci sequence · Primitive part of a Fibonacci number

TheoremBound on denominator indices of \(p\)-adic valuation one#●ready to prove

Let \(n \ge 37\) and let \(I\) and \(J\) be finite multisets of natural numbers, every element of which is at least \(3\) and different from \(6\) and \(12\), such that no element of \(I\) equals an element of \(J\) and \(n! = \prod_{a \in I} \Phi_a / \prod_{b \in J} \Phi_b\), where \(\Phi_m\) is the \(m\)-th Fibonacci cyclotomic value. Let \(p\) be a prime whose Fibonacci entry point \(z(p)\) exceeds \(12\), and let \(N_p\) be the number of elements \(m\) of \(J\), counted with multiplicity, such that the \(p\)-adic valuation of \(\Phi_m / \Psi_m\) is \(1\), where \(\Psi_m\) is the primitive part of the Fibonacci number \(F_m\). Then \(N_p < \frac{2n}{z(p)\, p\, (p - 2)}\).

public theorem_wanted card_padicValRat_fibDelta_eq_one_lt {n : ℕ} (hn : 37 ≤ n)
    (I J : Multiset ℕ) (hI : ∀ n ∈ I, 3 ≤ n ∧ n ≠ 6 ∧ n ≠ 12)
    (hJ : ∀ m ∈ J, 3 ≤ m ∧ m ≠ 6 ∧ m ≠ 12) (hIJ : ∀ a ∈ I, ∀ b ∈ J, a ≠ b)
    (hfact : (n.factorial : ℚ) =
      (I.map fibCyclotomicValue).prod / (J.map fibCyclotomicValue).prod)
    {p : ℕ} (hp : p.Prime) (hz : 12 < fibEntryPoint p) :
    ((J.filter fun m => padicValRat p (fibCyclotomicValue m / fibPrimitivePart m) = 1).card : ℚ) <
      2 * n / (fibEntryPoint p * p * ((p : ℚ) - 2))

Sources

• Florian Luca, F_4 F_5^6 F_7 F_8^4 F_9 F_{10}^2 F_{12}^5 F_{14} F_{15}^{-1} F_{18} F_{24} F_{30} = 36!, INTEGERS 24 (2024), Article A72, Lemma 2.

Uses 3

Statement usesFibonacci cyclotomic values · Entry point in the Fibonacci sequence · Primitive part of a Fibonacci number

7 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.