Fubini numbers modulo an integer

TheoremFalling factorial in terms of signed Stirling numbers#●ready to prove

For every natural number \(n\), the identity of polynomials with integer coefficients

\[x (x - 1) \cdots (x - n + 1) = \sum_{k=0}^{n} s(n, k)\, x^k\]

holds, where \(s(n, k)\) is the signed Stirling number of the first kind.

public theorem_wanted descPochhammer_eq_sum_signedStirlingFirst (n : ℕ) :
    descPochhammer ℤ n =
      ∑ k ∈ Finset.range (n + 1), C (signedStirlingFirst n k) * X ^ k
Sources
  • Benjamin Schreyer, Rigged Horse Numbers and their Modular Periodicity, Journal of Integer Sequences 28 (2025), Article 25.4.1, Proposition 2 (jis-2025-25.4.1-prop-2).
Uses 1
Statement usesSigned Stirling numbers of the first kind

TheoremA Carmichael congruence for all residues modulo \(K\)#●ready to prove

Let \(K\) be a natural number, let \(\lambda(K)\) be the value of the Carmichael function at \(K\), and let \(R\) be the largest exponent in the prime factorization of \(K\) (\(R = 0\) for \(K \le 1\)). Then \(a^R \equiv a^{\lambda(K) + R} \pmod K\) for every natural number \(a < K\).

public theorem_wanted pow_add_carmichael_modEq_of_lt (K a : ℕ) (ha : a < K) :
    let R := K.factorization.support.sup K.factorization
    a ^ R ≡ a ^ (carmichael K + R) [MOD K]
Sources
  • Benjamin Schreyer, Rigged Horse Numbers and their Modular Periodicity, Journal of Integer Sequences 28 (2025), Article 25.4.1, Proposition 4 (jis-2025-25.4.1-prop-4).

TheoremEventual periodicity of the Fubini numbers modulo \(K\)#●ready to prove

Let \(K\) be a natural number, let \(\lambda(K)\) be the value of the Carmichael function at \(K\), and let \(R\) be the largest exponent in the prime factorization of \(K\) (\(R = 0\) for \(K \le 1\)). Then the Fubini numbers \(F(n)\) satisfy \(F(n + \lambda(K)) \equiv F(n) \pmod K\) for every natural number \(n \ge R\).

public theorem_wanted fubiniNumber_add_carmichael_modEq (K n : ℕ)
    (hn : K.factorization.support.sup K.factorization ≤ n) :
    fubiniNumber (n + carmichael K) ≡ fubiniNumber n [MOD K]
Sources
  • Benjamin Schreyer, Rigged Horse Numbers and their Modular Periodicity, Journal of Integer Sequences 28 (2025), Article 25.4.1, Corollary 10 (jis-2025-25.4.1-cor-10).
Uses 1
Statement usesFubini numbers

TheoremEventual periods of the Fubini numbers modulo an odd number#●ready to prove

Let \(K\) be an odd natural number and let \(\lambda(K)\) be the value of the Carmichael function at \(K\). Then a natural number \(p\) is divisible by \(\lambda(K)\) if and only if there is a natural number \(N\) such that the Fubini numbers \(F(n)\) satisfy \(F(n + p) \equiv F(n) \pmod K\) for all \(n \ge N\). In particular, the eventual period of the Fubini numbers modulo \(K\) is exactly \(\lambda(K)\).

public theorem_wanted fubiniNumber_eventuallyPeriodic_iff_carmichael_dvd (K : ℕ) (hK : Odd K)
    (p : ℕ) :
    (∃ N, ∀ n ≥ N, fubiniNumber (n + p) ≡ fubiniNumber n [MOD K]) ↔ carmichael K ∣ p
Sources
  • Benjamin Schreyer, Rigged Horse Numbers and their Modular Periodicity, Journal of Integer Sequences 28 (2025), Article 25.4.1, Corollary 11 (jis-2025-25.4.1-cor-11).
Uses 1
Statement usesFubini numbers

TheoremEventual periodicity of the \(r\)-Fubini numbers modulo \(K\)#●ready to prove

For a natural number \(r \ge 1\) and a natural number \(m\), let \(F_r(m)\) be the number of pairs \((k, f)\) of a natural number \(k \le m\) and a surjection \(f : \{0, \dots, m - 1\} \to \{0, \dots, k - 1\}\) that is injective on the elements less than \(r\); equivalently, \(F_r(m)\) counts the weak orderings of \(m\) elements in which the elements less than \(r\) are pairwise untied. Let \(K\) be a natural number, let \(\lambda(K)\) be the value of the Carmichael function at \(K\), and let \(R\) be the largest exponent in the prime factorization of \(K\) (\(R = 0\) for \(K \le 1\)). Then \(F_r(n + \lambda(K)) \equiv F_r(n) \pmod K\) for every natural number \(n \ge r - 1 + R\).

public theorem_wanted rFubini_add_carmichael_modEq (K r n : ℕ) (hr : 1 ≤ r)
    (hn : r - 1 + K.factorization.support.sup K.factorization ≤ n) :
    let rFubini : ℕ → ℕ := fun m => ∑ k ∈ Finset.range (m + 1),
      Nat.card { f : Fin m → Fin k // Function.Surjective f ∧
        ∀ i j : Fin m, (i : ℕ) < r → (j : ℕ) < r → f i = f j → i = j }
    rFubini (n + carmichael K) ≡ rFubini n [MOD K]
Sources
  • Benjamin Schreyer, Rigged Horse Numbers and their Modular Periodicity, Journal of Integer Sequences 28 (2025), Article 25.4.1, Corollary 12 (jis-2025-25.4.1-cor-12).
5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.