Fault-free tilings of 3 × n rectangles

AbbreviationCells of the \(3 \times n\) rectangle#✓fully proved

A cell of the \(3 \times n\) rectangle is a pair \((r, c)\) of a row \(r \in \{0, 1, 2\}\) and a column \(c \in \{0, \dots, n-1\}\).

abbrev TilingCell (n : ℕ) := Fin 3 × Fin n

Used by 7

Used byAdjacent cells · Recurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle · Square-and-domino tilings · Square and domino tiles · Characterization of square and domino tiles · Vertical-fault-free families · Number of vertical-fault-free tilings of the \(3 \times n\) rectangle

DefinitionAdjacent cells#✓fully proved

Two cells \(x\) and \(y\) of the \(3 \times n\) rectangle are adjacent when they share an edge: they lie in the same row and their columns differ by \(1\), or they lie in the same column and their rows differ by \(1\).

def TilingCell.Adjacent {n : ℕ} (x y : TilingCell n) : Prop :=
  (x.1 = y.1 ∧ (x.2.val + 1 = y.2.val ∨ y.2.val + 1 = x.2.val)) ∨
    (x.2 = y.2 ∧ (x.1.val + 1 = y.1.val ∨ y.1.val + 1 = x.1.val))

Uses 1 · Used by 3

Statement usesCells of the \(3 \times n\) rectangle

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle · Square and domino tiles · Characterization of square and domino tiles

DefinitionSquare and domino tiles#✓fully proved

A set \(d\) of cells of the \(3 \times n\) rectangle is a square-or-domino tile when it consists of exactly one cell, or of exactly two cells that are adjacent.

def IsSquareOrDomino {n : ℕ} (d : Finset (TilingCell n)) : Prop :=
  d.card = 1 ∨
    (d.card = 2 ∧ ∀ x ∈ d, ∀ y ∈ d, x ≠ y → TilingCell.Adjacent x y)

Uses 2 · Used by 3

Statement usesCells of the \(3 \times n\) rectangle · Adjacent cells

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle · Square-and-domino tilings · Characterization of square and domino tiles

TheoremCharacterization of square and domino tiles#✓fully proved

A set \(d\) of cells of the \(3 \times n\) rectangle is a square-or-domino tile if and only if either \(d = \{x\}\) for some cell \(x\), or \(d = \{x, y\}\) for some distinct adjacent cells \(x\) and \(y\).

public theorem isSquareOrDomino_iff {n : ℕ} (d : Finset (TilingCell n)) :
    IsSquareOrDomino d ↔
      (∃ x, d = {x}) ∨
        ∃ x y, x ≠ y ∧ TilingCell.Adjacent x y ∧ d = {x, y}

Uses 3 · Used by 1

Statement usesSquare and domino tiles · Cells of the \(3 \times n\) rectangle · Adjacent cells

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle

DefinitionSquare-and-domino tilings#✓fully proved

A square-and-domino tiling of the \(3 \times n\) rectangle is a finite family \(T\) of sets of cells such that every member of \(T\) is a square-or-domino tile (a single cell or two adjacent cells), any two distinct members of \(T\) are disjoint, and every cell of the rectangle lies in some member of \(T\).

def IsSquareDominoTiling {n : ℕ} (T : Finset (Finset (TilingCell n))) : Prop :=
  (∀ d ∈ T, IsSquareOrDomino d) ∧
    (∀ d₁ ∈ T, ∀ d₂ ∈ T, d₁ ≠ d₂ → Disjoint d₁ d₂) ∧
      ∀ x : TilingCell n, ∃ d ∈ T, x ∈ d

Uses 2 · Used by 2

Statement usesSquare and domino tiles · Cells of the \(3 \times n\) rectangle

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle · Number of vertical-fault-free tilings of the \(3 \times n\) rectangle

DefinitionVertical-fault-free families#✓fully proved

A family \(T\) of sets of cells of the \(3 \times n\) rectangle, with columns numbered \(0, \dots, n-1\), is vertical-fault-free when for every natural number \(k\) with \(k + 1 < n\) some member of \(T\) contains two cells of the same row lying in columns \(k\) and \(k + 1\). For a square-and-domino tiling this says that every internal vertical boundary is crossed by a horizontal domino.

def IsVerticalFaultFree {n : ℕ} (T : Finset (Finset (TilingCell n))) : Prop :=
  ∀ k : ℕ, k + 1 < n →
    ∃ d ∈ T, ∃ x ∈ d, ∃ y ∈ d,
      x.1 = y.1 ∧ x.2.val = k ∧ y.2.val = k + 1

Uses 1 · Used by 2

Statement usesCells of the \(3 \times n\) rectangle

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle · Number of vertical-fault-free tilings of the \(3 \times n\) rectangle

DefinitionNumber of vertical-fault-free tilings of the \(3 \times n\) rectangle#✓fully proved

For every natural number \(n\), this is the number of square-and-domino tilings of the \(3 \times n\) rectangle that are vertical-fault-free.

noncomputable def verticalFaultFreeTilingCount (n : ℕ) : ℕ :=
  Nat.card {T : Finset (Finset (TilingCell n)) //
    IsSquareDominoTiling T ∧ IsVerticalFaultFree T}

Uses 3 · Used by 1

Statement usesSquare-and-domino tilings · Vertical-fault-free families · Cells of the \(3 \times n\) rectangle

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle

DefinitionRecurrence sequence for vertical-fault-free \(3 \times n\) tilings#✓fully proved

The integer sequence \((V_n)_{n \ge 0}\) is defined by \(V_0 = 0\), \(V_1 = 3\), \(V_2 = 13\), \(V_3 = 26\), \(V_4 = 66\), \(V_5 = 154\), \(V_6 = 380\) and \(V_n = V_{n-1} + 4 V_{n-2} - V_{n-3} - V_{n-4}\) for \(n \ge 7\).

The value \(V_0 = 0\) is a placeholder; the source considers only \(n \ge 1\).

def tilingCount : ℕ → ℤ
  | 0 => 0
  | 1 => 3
  | 2 => 13
  | 3 => 26
  | 4 => 66
  | 5 => 154
  | 6 => 380
  | (n + 7) => tilingCount (n + 6) + 4 * tilingCount (n + 5)
      - tilingCount (n + 4) - tilingCount (n + 3)

Used by 1

Used byRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle

TheoremRecurrence for vertical-fault-free tilings of the \(3 \times n\) rectangle#✓fully proved

For \(n \ge 1\), let \(V_n\) be the number of vertical-fault-free tilings of the \(3 \times n\) rectangle by unit squares and dominoes. Then \(V_1 = 3\), \(V_2 = 13\), \(V_3 = 26\), \(V_4 = 66\), \(V_5 = 154\), \(V_6 = 380\), and \(V_n = V_{n-1} + 4 V_{n-2} - V_{n-3} - V_{n-4}\) for every \(n \ge 7\).

Here \(V_n\) counts the tilings directly; the recurrence is a theorem, not its definition.

Proof: The count is encoded by a transfer matrix over column profiles. An annihilating polynomial for that matrix gives the recurrence after the six initial values.

public theorem fault_free_3xn_tiling_recursion :
    ∀ n : ℕ, 1 ≤ n → (verticalFaultFreeTilingCount n : ℤ) = tilingCount n

Sources

• Oluwatobi Jemima Alabi and Greg Dresden, "Fault-Free Tilings of the 3 × n Rectangle With Squares and Dominos," Journal of Integer Sequences 24 (2021), Article 21.1.2, theorem on vertical-fault-free V_n (unlabeled), lines 358–364, https://cs.uwaterloo.ca/journals/JIS/VOL24/Dresden/dresden7.tex.

Uses 8

Statement usesRecurrence sequence for vertical-fault-free \(3 \times n\) tilings · Number of vertical-fault-free tilings of the \(3 \times n\) rectangle

Proof usesSquare-and-domino tilings · Square and domino tiles · Vertical-fault-free families · Cells of the \(3 \times n\) rectangle · Adjacent cells · Characterization of square and domino tiles

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.