Domino tilings and Fibonacci–Pell products

TheoremFactorization of the domino tiling sequence#✓fully proved

Let \(d\) and \(g\) be sequences of natural numbers with \(d_1 = 1\), \(d_2 = 8\), \(d_3 = 95\), \(d_4 = 1183\) and \(d_{n+4} + 32 d_{n+2} + d_n = 15 d_{n+3} + 15 d_{n+1}\) for all \(n \ge 1\), and with \(g_1 = 1\), \(g_2 = 4\) and \(g_{n+2} + g_n = 5 g_{n+1}\) for all \(n \ge 1\). Then \(d_n = g_n F_{2n-1}\) for every \(n \ge 1\), where \(F_m\) is the \(m\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)).

These recurrences determine \(d_n\) and \(g_n\) for \(n \ge 1\): \(d_n\) is the number of domino tilings of \(P_5 \times P_{2n-2}\) (OEIS A003775) and \(g_n\) is OEIS A004253.

public theorem domino_tiling_sequence_factorization :
    ∀ (d g : Nat → Nat), d 1 = 1 → d 2 = 8 → d 3 = 95 → d 4 = 1183 →
    (∀ n, 1 ≤ n → d (n + 4) + 32 * d (n + 2) + d n = 15 * d (n + 3) + 15 * d (n + 1)) →
    g 1 = 1 → g 2 = 4 →
    (∀ n, 1 ≤ n → g (n + 2) + g n = 5 * g (n + 1)) →
    ∀ n, 1 ≤ n → d n = g n * Nat.fib (2 * n - 1)

Sources

• James A. Sellers, "Domino Tilings and Products of Fibonacci and Pell Numbers," Journal of Integer Sequences 5 (2002), Article 02.1.2, second Theorem (d_n = g_n h_n), lines 153–154, with d defined at lines 146–150 and g at line 164, https://cs.uwaterloo.ca/journals/JIS/VOL5/Sellers/sellers4.tex

TheoremSellers' domino tiling theorem#✓fully proved

Let \(W_4\) be the complete graph \(K_4\) with one edge removed and \(P_{n-1}\) the path graph on \(n - 1\) vertices. For every natural number \(n \ge 2\), the number of perfect matchings (domino tilings) of the Cartesian product \(W_4 \square P_{n-1}\) equals \(f_n p_n\), where \(f_n\) is the \(n\)-th Fibonacci number (\(f_0 = 0\), \(f_1 = 1\)) and \(p_n\) is the \(n\)-th Pell number (\(p_0 = 0\), \(p_1 = 1\), \(p_{k+2} = 2 p_{k+1} + p_k\)).

theorem boxProd_tiling_card_eq_fib_mul_pellNumber :
    ∀ (n : ℕ) (_hn : 2 ≤ n),
      Nat.card { M : (((SimpleGraph.completeGraph (Fin 4)).deleteEdges
        {Sym2.mk (0 : Fin 4) (1 : Fin 4)} □
        SimpleGraph.pathGraph (n - 1)).Subgraph) // M.IsPerfectMatching } =
        Nat.fib n * pellNumber n

Uses 1 · Used by 1

Statement usesPell numbers

Used bySellers' domino tiling theorem, recursive Pell form

TheoremSellers' domino tiling theorem, recursive Pell form#✓fully proved

Let \(W_4\) be the complete graph \(K_4\) with one edge removed and \(P_{n-1}\) the path graph on \(n - 1\) vertices. For every natural number \(n \ge 2\), the number of perfect matchings (domino tilings) of the Cartesian product \(W_4 \square P_{n-1}\) equals \(f_n p_n\), where \(f_n\) is the \(n\)-th Fibonacci number (\(f_0 = 0\), \(f_1 = 1\)) and \(p_n\) is defined by \(p_0 = 0\), \(p_1 = 1\) and \(p_{k+2} = 2 p_{k+1} + p_k\).

The Cartesian product \(\square\) is the paper's \(\times\), following Faase. The paper writes \(c_n\) for this number of tilings; its values \(c_2 = 2\), \(c_3 = 10\), \(c_4 = 36\) match \(f_n p_n\).

theorem boxProd_tiling_card_eq_fib_mul_pell :
    ∀ (n : ℕ) (_hn : 2 ≤ n),
      Nat.card { M : (((SimpleGraph.completeGraph (Fin 4)).deleteEdges
        {Sym2.mk (0 : Fin 4) (1 : Fin 4)} □
        SimpleGraph.pathGraph (n - 1)).Subgraph) // M.IsPerfectMatching } =
        Nat.fib n *
          ((Nat.rec (motive := fun (_ : ℕ) => ℕ × ℕ) (0, 1)
            (fun (_ : ℕ) (ih : ℕ × ℕ) => (ih.2, 2 * ih.2 + ih.1)) n).1)

Sources

• James A. Sellers, "Domino Tilings and Products of Fibonacci and Pell Numbers," Journal of Integer Sequences 5 (2002), Article 02.1.2, Theorem, lines 105–108, https://cs.uwaterloo.ca/journals/JIS/VOL5/Sellers/sellers4.tex

Uses 2

Proof usesSellers' domino tiling theorem · Pell numbers

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.