Tilings, dimers and board placements

Covering and placement problems on lattices and boards: domino and lozenge tilings and perfect matchings of grid regions (Aztec diamonds, Möbius grids, cylinders and tori), polyominoes and polycubes, tilings of groups by translates and the periodic tiling conjecture, nonattacking chess pieces, rook and file placements on Ferrers boards, and self-avoiding walks on lattices.

• Aztec dragon tilings
• Domino tilings and Fibonacci–Pell products
• Fault-free tilings of 3 × n rectangles
• Fence tilings and bi-periodic Fibonacci numbers
• Fixed polycubes
• Lozenge tilings of hexagons
• Nonattacking bishops and anassas
• Perfect matchings of the Möbius grid
• Periodic tiling conjecture
• Self-avoiding walks on the honeycomb lattice
• Tilings of grids, cylinders and tori up to symmetry
• Tilings of the symmetric group by transpositions
• Weighted file placements on Ferrers boards

TheoremQuarter-period factorizations of the triangular tiling numbers#✓fully proved

Let \(Q \colon \mathbb{N} \to \mathbb{N}\) satisfy \(Q(0) = Q(1) = 1\), \(Q(2) = 4\) and \(Q(n) = Q(n-1) + 3Q(n-2) + Q(n-3)\) for every \(n \ge 3\). Then for every \(m \ge 1\),

\[Q(4m) = (2Q(2m-1) + 1)(2Q(2m) - 1),\]

\[Q(4m+1) = (2Q(2m) - 1)^2,\]

\[Q(4m+2) = 2(Q(2m-1) + Q(2m))(Q(2m) + Q(2m+1)),\]

\[Q(4m+3) = 2(Q(2m) + Q(2m+1))^2.\]

All values of \(Q\) are at least \(1\), so the subtractions above are exact. In the source, \(Q(n)\) is the number of tilings of a triangular strip.

MetaMathlibExt.quarter_period_factorizations · 17 lines

theorem quarter_period_factorizations
    (Q : ℕ → ℕ)
    (hQ0 : Q 0 = 1)
    (hQ1 : Q 1 = 1)
    (hQ2 : Q 2 = 4)
    (hQrec : ∀ n : ℕ, 3 ≤ n →
      Q n = Q (n - 1) + 3 * Q (n - 2) + Q (n - 3))
    (m : ℕ)
    (hm : 1 ≤ m) :
    Q (4 * m) =
        (2 * Q (2 * m - 1) + 1) * (2 * Q (2 * m) - 1) ∧
      Q (4 * m + 1) = (2 * Q (2 * m) - 1) ^ 2 ∧
      Q (4 * m + 2) =
        2 * (Q (2 * m - 1) + Q (2 * m)) *
          (Q (2 * m) + Q (2 * m + 1)) ∧
      Q (4 * m + 3) =
        2 * (Q (2 * m) + Q (2 * m + 1)) ^ 2

Sources

• Mark Shattuck, "Combinatorial Proofs of Some Formulas for Triangular Tilings," Journal of Integer Sequences 17 (2014), Article 14.5.5, Theorem (due to Bodeen et al.), lines 103–112, https://cs.uwaterloo.ca/journals/JIS/VOL17/Shattuck/shattuck8.tex

TheoremTauraso's Cassini-type identity#●ready to prove

Let \(f_n\) be the Fibonacci numbers, with \(f_0 = 0\) and \(f_1 = 1\). For natural numbers \(n, m\) put \(L_{n,m} = f_{n+1} f_m + f_n f_{m+1}\) and \(a_n = f_{n+1} f_{n-1} + f_n^2\), where \(n - 1\) is truncated subtraction. Then \(L_{n,m} = f_{n+1} f_m + f_n f_{m+1}\) for all \(n, m \ge 1\), \(L_{n,n-1} = a_n\) for all \(n \ge 2\), and \(L_{n,n-1}^2 = L_{n,n} L_{n-1,n-1} + 1\) for all \(n \ge 2\).

In the source \(L_{n,m}\) is the number of domino tilings of the L-grid, and the Fibonacci formula for it is a theorem. Here \(L_{n,m}\) is defined by that formula, so the first two equations hold by definition and the content is the Cassini-type identity.

public theorem_wanted domino_tilings_L_grid_via_fibonacci :
    let L : ℕ → ℕ → ℕ := fun n m =>
      Nat.fib (n + 1) * Nat.fib m + Nat.fib n * Nat.fib (m + 1)
    let a : ℕ → ℕ := fun n =>
      Nat.fib (n + 1) * Nat.fib (n - 1) + Nat.fib n ^ 2
    (∀ n m : ℕ, 1 ≤ n → 1 ≤ m →
      L n m = Nat.fib (n + 1) * Nat.fib m +
        Nat.fib n * Nat.fib (m + 1)) ∧
    (∀ n : ℕ, 2 ≤ n → L n (n - 1) = a n) ∧
    (∀ n : ℕ, 2 ≤ n →
      (L n (n - 1)) ^ 2 = L n n * L (n - 1) (n - 1) + 1)

Sources

• Roberto Tauraso, "A New Domino Tiling Sequence," Journal of Integer Sequences 7 (2004), Article 04.2.3, Lemma (Section 2, equations Lformula and Lcassini), lines 200–221, https://cs.uwaterloo.ca/journals/JIS/VOL7/Tauraso/tauraso3.tex

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.