Domino Tilings of Height-3 Rectangles

This file formalizes the classification of faultfree domino tilings of the rectangle R_{n,3} from Subsection sec.details.domino of the Algebraic Combinatorics notes.

A domino is a 1×2 or 2×1 rectangle. A domino tiling of a rectangle is a partition of the rectangle's cells into dominos. A fault in a tiling is a vertical line that passes through the entire rectangle without crossing any domino. A faultfree tiling has no such faults.

Main definitions

• Rectangle: The set of cells in an n×m rectangle
• Domino: A pair of adjacent cells (horizontal or vertical)
• DominoTiling: A set of dominos that partition a rectangle
• hasFault: Whether a tiling has a fault at a given column
• isFaultfree: Whether a tiling has no faults
• TilingA: The family of faultfree tilings A_n for even n
• TilingB: The family of faultfree tilings B_n for even n (reflection of A_n)
• TilingC: The unique faultfree tiling of R_{2,3} with no vertical domino in column 1

Main results

• faultfree_classification: The faultfree domino tilings of height-3 rectangles are precisely A_2, A_4, A_6, ..., B_2, B_4, B_6, ..., and C.
• faultfree_top_vertical_classification: A faultfree tiling with a vertical domino in the top two squares of column 1 is equivalent to some A_n.
• faultfree_bottom_vertical_classification: A faultfree tiling with a vertical domino in the bottom two squares of column 1 is equivalent to some B_n.
• faultfree_no_vertical_unique: A faultfree 2×3 tiling with no vertical domino in column 1 is equivalent to C (using TilingEquiv, not structural equality).

References

• Source: AlgebraicCombinatorics/tex/Details/DominoTilings.tex
• Grinberg, Darij. "Algebraic Combinatorics" (lecture notes), Subsection sec.gf.weighted-set.domino

Tags

domino tiling, faultfree, rectangle, combinatorics

Basic Definitions

@[reducible, inline]

abbrev DominoTilings.Cell : Type

A cell in a rectangle, represented as a pair (column, row) with 1-indexing. Column numbers go from 1 to n (left to right). Row numbers go from 1 to m (bottom to top).

Equations

• DominoTilings.Cell = (ℕ × ℕ)

def DominoTilings.Rectangle (n m : ℕ) : Finset Cell

The rectangle R_{n,m} is the set of cells {(x, y) : 1 ≤ x ≤ n, 1 ≤ y ≤ m}.

Equations

• One or more equations did not get rendered due to their size.

theorem DominoTilings.card_Rectangle (n m : ℕ) : (Rectangle n m).card = n * m

The rectangle R_{n,m} has exactly n * m cells.

theorem DominoTilings.mem_Rectangle {n m : ℕ} {c : Cell} : c ∈ Rectangle n m ↔ c.1 ≥ 1 ∧ c.1 ≤ n ∧ c.2 ≥ 1 ∧ c.2 ≤ m

Membership characterization for Rectangle.

structure DominoTilings.Domino : Type

A domino is a pair of adjacent cells, either horizontal or vertical.

• cell1 : Cell

  The first cell of the domino

• cell2 : Cell

  The second cell of the domino

• distinct : self.cell1 ≠ self.cell2

  The cells are distinct

• adjacent : self.cell1.1 = self.cell2.1 ∧ (self.cell1.2 + 1 = self.cell2.2 ∨ self.cell2.2 + 1 = self.cell1.2) ∨ self.cell1.2 = self.cell2.2 ∧ (self.cell1.1 + 1 = self.cell2.1 ∨ self.cell2.1 + 1 = self.cell1.1)

  The cells are adjacent (horizontally or vertically)

theorem DominoTilings.Domino.ext_iff {x y : Domino} : x = y ↔ x.cell1 = y.cell1 ∧ x.cell2 = y.cell2

theorem DominoTilings.Domino.ext {x y : Domino} (cell1 : x.cell1 = y.cell1) (cell2 : x.cell2 = y.cell2) : x = y

instance DominoTilings.instDecidableEqDomino : DecidableEq Domino

Equations

• DominoTilings.instDecidableEqDomino = DominoTilings.instDecidableEqDomino.decEq

def DominoTilings.instDecidableEqDomino.decEq (x✝ x✝¹ : Domino) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.Domino.cells (d : Domino) : Finset Cell

The set of cells covered by a domino.

Equations

• d.cells = {d.cell1, d.cell2}

@[simp]

theorem DominoTilings.Domino.card_cells (d : Domino) : d.cells.card = 2

Each domino covers exactly 2 cells.

def DominoTilings.Domino.isHorizontal (d : Domino) : Prop

A domino is horizontal if both cells are in the same row.

Equations

• d.isHorizontal = (d.cell1.2 = d.cell2.2)

def DominoTilings.Domino.isVertical (d : Domino) : Prop

A domino is vertical if both cells are in the same column.

Equations

• d.isVertical = (d.cell1.1 = d.cell2.1)

instance DominoTilings.Domino.instDecidablePredIsHorizontal : DecidablePred isHorizontal

Equations

• d.instDecidablePredIsHorizontal = inferInstanceAs (Decidable (d.cell1.2 = d.cell2.2))

instance DominoTilings.Domino.instDecidablePredIsVertical : DecidablePred isVertical

Equations

• d.instDecidablePredIsVertical = inferInstanceAs (Decidable (d.cell1.1 = d.cell2.1))

theorem DominoTilings.Domino.isHorizontal_or_isVertical (d : Domino) : d.isHorizontal ∨ d.isVertical

Every domino is either horizontal or vertical.

theorem DominoTilings.Domino.not_isHorizontal_and_isVertical (d : Domino) : ¬(d.isHorizontal ∧ d.isVertical)

A domino cannot be both horizontal and vertical.

theorem DominoTilings.Domino.isHorizontal_iff_not_isVertical (d : Domino) : d.isHorizontal ↔ ¬d.isVertical

A domino is horizontal iff it's not vertical.

theorem DominoTilings.Domino.isVertical_iff_not_isHorizontal (d : Domino) : d.isVertical ↔ ¬d.isHorizontal

A domino is vertical iff it's not horizontal.

theorem DominoTilings.Domino.isHorizontal_xor_isVertical (d : Domino) : Xor' d.isHorizontal d.isVertical

Every domino is either horizontal or vertical (exclusive or).

def DominoTilings.Domino.minCol (d : Domino) : ℕ

The leftmost column touched by a domino.

Equations

• d.minCol = min d.cell1.1 d.cell2.1

def DominoTilings.Domino.maxCol (d : Domino) : ℕ

The rightmost column touched by a domino.

Equations

• d.maxCol = max d.cell1.1 d.cell2.1

Shifting operations for dominos

These operations shift a domino horizontally by adding or subtracting from the column coordinate. They are essential for the Fibonacci recurrence bijection on 2×n tilings.

def DominoTilings.Domino.shiftNat (d : Domino) (k : ℕ) : Domino

Shift a domino k columns to the right.

Equations

• d.shiftNat k = { cell1 := (d.cell1.1 + k, d.cell1.2), cell2 := (d.cell2.1 + k, d.cell2.2), distinct := ⋯, adjacent := ⋯ }

def DominoTilings.Domino.shiftNeg (d : Domino) (k : ℕ) (h1 : d.cell1.1 ≥ k + 1) (h2 : d.cell2.1 ≥ k + 1) : Domino

Shift a domino k columns to the left. Requires that both cells have column ≥ k+1.

Equations

• d.shiftNeg k h1 h2 = { cell1 := (d.cell1.1 - k, d.cell1.2), cell2 := (d.cell2.1 - k, d.cell2.2), distinct := ⋯, adjacent := ⋯ }

@[simp]

theorem DominoTilings.Domino.shiftNat_cell1 (d : Domino) (k : ℕ) : (d.shiftNat k).cell1 = (d.cell1.1 + k, d.cell1.2)

@[simp]

theorem DominoTilings.Domino.shiftNat_cell2 (d : Domino) (k : ℕ) : (d.shiftNat k).cell2 = (d.cell2.1 + k, d.cell2.2)

@[simp]

theorem DominoTilings.Domino.shiftNeg_cell1 (d : Domino) (k : ℕ) (h1 : d.cell1.1 ≥ k + 1) (h2 : d.cell2.1 ≥ k + 1) : (d.shiftNeg k h1 h2).cell1 = (d.cell1.1 - k, d.cell1.2)

@[simp]

theorem DominoTilings.Domino.shiftNeg_cell2 (d : Domino) (k : ℕ) (h1 : d.cell1.1 ≥ k + 1) (h2 : d.cell2.1 ≥ k + 1) : (d.shiftNeg k h1 h2).cell2 = (d.cell2.1 - k, d.cell2.2)

theorem DominoTilings.Domino.shiftNeg_shiftNat (d : Domino) (k : ℕ) (hc1 : d.cell1.1 ≥ 1) (hc2 : d.cell2.1 ≥ 1) : (d.shiftNat k).shiftNeg k ⋯ ⋯ = d

Shifting right then left returns the original domino (when original has positive columns).

theorem DominoTilings.Domino.shiftNat_shiftNeg (d : Domino) (k : ℕ) (h1 : d.cell1.1 ≥ k + 1) (h2 : d.cell2.1 ≥ k + 1) : (d.shiftNeg k h1 h2).shiftNat k = d

Shifting left then right returns the original domino.

theorem DominoTilings.Domino.shiftNat_shiftNeg_cells (d : Domino) (k : ℕ) (h1 : d.cell1.1 ≥ k + 1) (h2 : d.cell2.1 ≥ k + 1) : ((d.shiftNeg k h1 h2).shiftNat k).cells = d.cells

Cells are preserved through shift-unshift: (d.shiftNeg k ...).shiftNat k has the same cells as d. This is a corollary of shiftNat_shiftNeg and is useful for proving TilingEquiv.

theorem DominoTilings.Domino.shiftNat_injective (k : ℕ) : Function.Injective fun (d : Domino) => d.shiftNat k

shiftNat is injective.

theorem DominoTilings.Domino.shiftNeg_injective {d1 d2 : Domino} {k : ℕ} (h1_1 : d1.cell1.1 ≥ k + 1) (h1_2 : d1.cell2.1 ≥ k + 1) (h2_1 : d2.cell1.1 ≥ k + 1) (h2_2 : d2.cell2.1 ≥ k + 1) (heq : d1.shiftNeg k h1_1 h1_2 = d2.shiftNeg k h2_1 h2_2) : d1 = d2

shiftNeg is injective (when both dominos have sufficient column coordinates).

theorem DominoTilings.Domino.shiftNat_minCol_ge (d : Domino) (k : ℕ) (hc1 : d.cell1.1 ≥ 1) (hc2 : d.cell2.1 ≥ 1) : (d.shiftNat k).minCol ≥ k + 1

A shifted domino has minCol at least k+1 when original has positive columns.

theorem DominoTilings.Domino.shiftNat_isVertical (d : Domino) (k : ℕ) (h : d.isVertical) : (d.shiftNat k).isVertical

Vertical dominos remain vertical after shifting.

theorem DominoTilings.Domino.shiftNat_isHorizontal (d : Domino) (k : ℕ) (h : d.isHorizontal) : (d.shiftNat k).isHorizontal

Horizontal dominos remain horizontal after shifting.

Standard dominos for 2×n tilings

These are the specific dominos used in the Fibonacci recurrence bijection for tilings of Rectangle n 2.

def DominoTilings.vertical_1_1 : Domino

The vertical domino covering column 1 in a 2-row rectangle: cells (1,1) and (1,2).

Equations

• DominoTilings.vertical_1_1 = { cell1 := (1, 1), cell2 := (1, 2), distinct := DominoTilings.vertical_1_1._proof_1, adjacent := DominoTilings.vertical_1_1._proof_2 }

def DominoTilings.horizontal_1_1 : Domino

The horizontal domino covering row 1, columns 1-2: cells (1,1) and (2,1).

Equations

• DominoTilings.horizontal_1_1 = { cell1 := (1, 1), cell2 := (2, 1), distinct := DominoTilings.horizontal_1_1._proof_1, adjacent := DominoTilings.horizontal_1_1._proof_2 }

def DominoTilings.horizontal_1_2 : Domino

The horizontal domino covering row 2, columns 1-2: cells (1,2) and (2,2).

Equations

• DominoTilings.horizontal_1_2 = { cell1 := (1, 2), cell2 := (2, 2), distinct := DominoTilings.horizontal_1_2._proof_1, adjacent := DominoTilings.horizontal_1_2._proof_2 }

@[simp]

theorem DominoTilings.vertical_1_1_cell1 : vertical_1_1.cell1 = (1, 1)

@[simp]

theorem DominoTilings.vertical_1_1_cell2 : vertical_1_1.cell2 = (1, 2)

@[simp]

theorem DominoTilings.horizontal_1_1_cell1 : horizontal_1_1.cell1 = (1, 1)

@[simp]

theorem DominoTilings.horizontal_1_1_cell2 : horizontal_1_1.cell2 = (2, 1)

@[simp]

theorem DominoTilings.horizontal_1_2_cell1 : horizontal_1_2.cell1 = (1, 2)

@[simp]

theorem DominoTilings.horizontal_1_2_cell2 : horizontal_1_2.cell2 = (2, 2)

@[simp]

theorem DominoTilings.vertical_1_1_isVertical : vertical_1_1.isVertical

@[simp]

theorem DominoTilings.horizontal_1_1_isHorizontal : horizontal_1_1.isHorizontal

@[simp]

theorem DominoTilings.horizontal_1_2_isHorizontal : horizontal_1_2.isHorizontal

theorem DominoTilings.vertical_1_1_cells : vertical_1_1.cells = {(1, 1), (1, 2)}

theorem DominoTilings.horizontal_1_1_cells : horizontal_1_1.cells = {(1, 1), (2, 1)}

theorem DominoTilings.horizontal_1_2_cells : horizontal_1_2.cells = {(1, 2), (2, 2)}

theorem DominoTilings.vertical_1_1_ne_horizontal_1_1 : vertical_1_1 ≠ horizontal_1_1

The vertical domino is not equal to horizontal_1_1.

theorem DominoTilings.vertical_1_1_ne_horizontal_1_2 : vertical_1_1 ≠ horizontal_1_2

The vertical domino is not equal to horizontal_1_2.

theorem DominoTilings.horizontal_1_1_ne_horizontal_1_2 : horizontal_1_1 ≠ horizontal_1_2

horizontal_1_1 is not equal to horizontal_1_2.

def DominoTilings.vertical_1_1_flip : Domino

The "flipped" vertical domino with cell1 and cell2 swapped.

Equations

• DominoTilings.vertical_1_1_flip = { cell1 := (1, 2), cell2 := (1, 1), distinct := DominoTilings.vertical_1_1_flip._proof_1, adjacent := DominoTilings.vertical_1_1_flip._proof_2 }

@[simp]

theorem DominoTilings.vertical_1_1_flip_cell1 : vertical_1_1_flip.cell1 = (1, 2)

@[simp]

theorem DominoTilings.vertical_1_1_flip_cell2 : vertical_1_1_flip.cell2 = (1, 1)

theorem DominoTilings.vertical_1_1_flip_cells : vertical_1_1_flip.cells = {(1, 2), (1, 1)}

theorem DominoTilings.vertical_1_1_flip_cells_eq : vertical_1_1_flip.cells = vertical_1_1.cells

theorem DominoTilings.vertical_1_1_ne_vertical_1_1_flip : vertical_1_1 ≠ vertical_1_1_flip

theorem DominoTilings.eq_vertical_1_1_of_cells_eq (d : Domino) (h : d.cells = vertical_1_1.cells) : d = vertical_1_1 ∨ d = vertical_1_1_flip

If a domino has the same cells as vertical_1_1, it is either vertical_1_1 or vertical_1_1_flip.

theorem DominoTilings.vertical_1_1_not_in_shiftNat1_image (S : Finset Domino) (hS : ∀ d ∈ S, d.cell1.1 ≥ 1 ∧ d.cell2.1 ≥ 1) : vertical_1_1 ∉ Finset.image (fun (d : Domino) => d.shiftNat 1) S

vertical_1_1 is not in the image of shiftNat by 1 for dominos with positive columns.

theorem DominoTilings.horizontal_1_1_not_in_shiftNat2_image (S : Finset Domino) (hS : ∀ d ∈ S, d.cell1.1 ≥ 1 ∧ d.cell2.1 ≥ 1) : horizontal_1_1 ∉ Finset.image (fun (d : Domino) => d.shiftNat 2) S

horizontal_1_1 is not in the image of shiftNat by 2 for dominos with positive columns.

theorem DominoTilings.horizontal_1_2_not_in_shiftNat2_image (S : Finset Domino) (hS : ∀ d ∈ S, d.cell1.1 ≥ 1 ∧ d.cell2.1 ≥ 1) : horizontal_1_2 ∉ Finset.image (fun (d : Domino) => d.shiftNat 2) S

horizontal_1_2 is not in the image of shiftNat by 2 for dominos with positive columns.

theorem DominoTilings.vertical_1_1_not_in_shiftNat2_image (S : Finset Domino) (hS : ∀ d ∈ S, d.cell1.1 ≥ 1 ∧ d.cell2.1 ≥ 1) : vertical_1_1 ∉ Finset.image (fun (d : Domino) => d.shiftNat 2) S

vertical_1_1 is not in the image of shiftNat by 2 for dominos with positive columns.

Domino Tilings

structure DominoTilings.DominoTiling (n m : ℕ) : Type

A domino tiling of a rectangle is a finite set of dominos such that:

1. Each domino's cells are within the rectangle
2. The dominos partition the rectangle (cover all cells exactly once)

• dominos : Finset Domino

  The set of dominos in the tiling

• dominos_in_rect (d : Domino) : d ∈ self.dominos → d.cells ⊆ Rectangle n m

  All dominos are within the rectangle

• covers_all : self.dominos.biUnion Domino.cells = Rectangle n m

  The dominos cover all cells

• pairwise_disjoint (d₁ : Domino) : d₁ ∈ self.dominos → ∀ d₂ ∈ self.dominos, d₁ ≠ d₂ → Disjoint d₁.cells d₂.cells

  The dominos are pairwise disjoint

theorem DominoTilings.DominoTiling.domino_cells_col_ge_one {n m : ℕ} (T : DominoTiling n m) (d : Domino) (hd : d ∈ T.dominos) : d.cell1.1 ≥ 1 ∧ d.cell2.1 ≥ 1

Dominos in a tiling have cells with positive column coordinates.

theorem DominoTilings.DominoTiling.domino_cells_row_ge_one {n m : ℕ} (T : DominoTiling n m) (d : Domino) (hd : d ∈ T.dominos) : d.cell1.2 ≥ 1 ∧ d.cell2.2 ≥ 1

Dominos in a tiling have cells with positive row coordinates.

theorem DominoTilings.DominoTiling.other_dominos_col_ge_3 {n : ℕ} (T : DominoTiling (n + 2) 2) (hh1 : horizontal_1_1 ∈ T.dominos) (hh2 : horizontal_1_2 ∈ T.dominos) (d : Domino) (hd : d ∈ T.dominos) (hne1 : d ≠ horizontal_1_1) (hne2 : d ≠ horizontal_1_2) : d.cell1.1 ≥ 3 ∧ d.cell2.1 ≥ 3

In a 2-row tiling with horizontal_1_1 and horizontal_1_2, all other dominos have cells with column ≥ 3. This is because horizontal_1_1 and horizontal_1_2 cover all cells in columns 1 and 2.

def DominoTilings.DominoTiling.hasFaultAt {n m : ℕ} (T : DominoTiling n m) (k : ℕ) : Prop

A tiling has a fault at column k if there is a vertical line between columns k and k+1 that does not cross any domino. Equivalently, no domino spans columns k and k+1.

Equations

• T.hasFaultAt k = (k ≥ 1 ∧ k < n ∧ ∀ d ∈ T.dominos, ¬(d.minCol ≤ k ∧ k < d.maxCol))

instance DominoTilings.DominoTiling.instDecidableHasFaultAt {n m : ℕ} (T : DominoTiling n m) (k : ℕ) : Decidable (T.hasFaultAt k)

Equations

• T.instDecidableHasFaultAt k = inferInstanceAs (Decidable (k ≥ 1 ∧ k < n ∧ ∀ d ∈ T.dominos, ¬(d.minCol ≤ k ∧ k < d.maxCol)))

def DominoTilings.DominoTiling.isFaultfree {n m : ℕ} (T : DominoTiling n m) : Prop

A tiling is faultfree if it has no faults at any column in range [1, n-1].

Equations

• T.isFaultfree = ∀ k ≥ 1, k < n → ¬T.hasFaultAt k

def DominoTilings.DominoTiling.hasTopVerticalInCol {n m : ℕ} (T : DominoTiling n m) (c : ℕ) : Prop

Whether a tiling contains a vertical domino in the top two squares of column c.

Equations

• T.hasTopVerticalInCol c = ∃ d ∈ T.dominos, d.isVertical ∧ d.cell1.1 = c ∧ (d.cell1.2 = m - 1 ∧ d.cell2.2 = m ∨ d.cell1.2 = m ∧ d.cell2.2 = m - 1)

def DominoTilings.DominoTiling.hasBottomVerticalInCol {n m : ℕ} (T : DominoTiling n m) (c : ℕ) : Prop

Whether a tiling contains a vertical domino in the bottom two squares of column c.

Equations

• T.hasBottomVerticalInCol c = ∃ d ∈ T.dominos, d.isVertical ∧ d.cell1.1 = c ∧ (d.cell1.2 = 1 ∧ d.cell2.2 = 2 ∨ d.cell1.2 = 2 ∧ d.cell2.2 = 1)

def DominoTilings.DominoTiling.hasVerticalInCol {n m : ℕ} (T : DominoTiling n m) (c : ℕ) : Prop

Whether a tiling contains any vertical domino in column c.

Equations

• T.hasVerticalInCol c = ∃ d ∈ T.dominos, d.isVertical ∧ d.cell1.1 = c

theorem DominoTilings.DominoTiling.card_eq_twice_dominos {n m : ℕ} (T : DominoTiling n m) : (Rectangle n m).card = 2 * T.dominos.card

The cardinality of the rectangle equals twice the number of dominos in any tiling.

theorem DominoTilings.DominoTiling.cell_covered {n m : ℕ} (T : DominoTiling n m) (c : Cell) (hc : c ∈ Rectangle n m) : ∃ d ∈ T.dominos, c ∈ d.cells

Every cell in the rectangle is covered by some domino in the tiling.

theorem DominoTilings.DominoTiling.cell_covered_unique {n m : ℕ} (T : DominoTiling n m) (c : Cell) (d₁ d₂ : Domino) (hd₁ : d₁ ∈ T.dominos) (hd₂ : d₂ ∈ T.dominos) (hc₁ : c ∈ d₁.cells) (hc₂ : c ∈ d₂.cells) : d₁ = d₂

If a cell is covered by two dominos in a tiling, they must be the same domino. This follows from the pairwise disjointness of dominos in a tiling.

def DominoTilings.DominoTiling.TilingEquiv {n m : ℕ} (T₁ T₂ : DominoTiling n m) : Prop

Two tilings are equivalent if they cover the same cells with the same domino cell sets.

This is the appropriate notion of equality for tilings, since the Domino structure distinguishes between {cell1 := a, cell2 := b} and {cell1 := b, cell2 := a} even though they cover the same cells.

Note: This is a weaker notion than structural equality (T₁ = T₂), but is the mathematically correct notion for classification theorems.

Equations

• T₁.TilingEquiv T₂ = (Finset.image DominoTilings.Domino.cells T₁.dominos = Finset.image DominoTilings.Domino.cells T₂.dominos)

theorem DominoTilings.DominoTiling.tilingEquiv_refl {n m : ℕ} (T : DominoTiling n m) : T.TilingEquiv T

TilingEquiv is reflexive.

theorem DominoTilings.DominoTiling.tilingEquiv_symm {n m : ℕ} {T₁ T₂ : DominoTiling n m} (h : T₁.TilingEquiv T₂) : T₂.TilingEquiv T₁

TilingEquiv is symmetric.

theorem DominoTilings.DominoTiling.tilingEquiv_trans {n m : ℕ} {T₁ T₂ T₃ : DominoTiling n m} (h₁ : T₁.TilingEquiv T₂) (h₂ : T₂.TilingEquiv T₃) : T₁.TilingEquiv T₃

TilingEquiv is transitive.

theorem DominoTilings.DominoTiling.image_erase_insert_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (S : Finset α) (v w : α) (f : α → β) (hv : v ∈ S) (hf : f v = f w) : Finset.image f (insert w (S.erase v)) = Finset.image f S

Helper lemma: replacing an element v with w in a finset preserves the image when f(v) = f(w). This is the key lemma for proving TilingEquiv is preserved when replacing a domino with another domino covering the same cells.

Prepend operations for the Fibonacci recurrence bijection

These operations construct tilings of Rectangle (n+1) 2 or Rectangle (n+2) 2 from tilings of smaller rectangles by prepending dominos at the left edge and shifting existing dominos to the right. They form the inverse maps in the bijection: Tiling (Rectangle (n+2) 2) ≃ Tiling (Rectangle n 2) ⊕ Tiling (Rectangle (n+1) 2)

def DominoTilings.DominoTiling.prependVertical {n : ℕ} (T : DominoTiling n 2) : DominoTiling (n + 1) 2

Prepend a vertical domino at (1,1)-(1,2) to a tiling of Rectangle n 2, creating a tiling of Rectangle (n+1) 2.

This is one of the inverse maps in the Fibonacci recurrence bijection. The vertical domino covers the entire first column, creating a fault at x=1.

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.DominoTiling.prependHorizontalPair {n : ℕ} (T : DominoTiling n 2) : DominoTiling (n + 2) 2

Prepend two horizontal dominos at (1,1)-(2,1) and (1,2)-(2,2) to a tiling of Rectangle n 2, creating a tiling of Rectangle (n+2) 2.

This is one of the inverse maps in the Fibonacci recurrence bijection. The two horizontal dominos cover the first two columns, creating a fault at x=2.

Equations

• One or more equations did not get rendered due to their size.

Restriction operations for the Fibonacci recurrence bijection

These operations extract the "rest" of a tiling after removing the dominos covering the first column(s). They form the forward maps in the bijection: Tiling (Rectangle (n+2) 2) ≃ Tiling (Rectangle n 2) ⊕ Tiling (Rectangle (n+1) 2)

The idea:

• If the first column has a vertical domino, remove it and shift remaining by 1
• If the first two columns have horizontal dominos, remove them and shift by 2

Together with prependVertical and prependHorizontalPair, these establish the Fibonacci recurrence: |Tiling(n+2, 2)| = |Tiling(n, 2)| + |Tiling(n+1, 2)|

theorem DominoTilings.DominoTiling.domino_col_ge_two_of_disjoint_from_first_col {n : ℕ} (T : DominoTiling (n + 1) 2) (v : Domino) (hv : v ∈ T.dominos) (hv_cells : v.cells = vertical_1_1.cells) (d : Domino) (hd : d ∈ T.dominos) (hne : d ≠ v) : d.cell1.1 ≥ 2 ∧ d.cell2.1 ≥ 2

If a domino d in a tiling is disjoint from a domino covering {(1,1), (1,2)}, then d's cells have column ≥ 2. This is the generalized version that works with any domino covering the first column, not just vertical_1_1.

theorem DominoTilings.DominoTiling.domino_col_ge_two_of_ne_vertical {n : ℕ} (T : DominoTiling (n + 1) 2) (hv : vertical_1_1 ∈ T.dominos) (d : Domino) (hd : d ∈ T.dominos) (hne : d ≠ vertical_1_1) : d.cell1.1 ≥ 2 ∧ d.cell2.1 ≥ 2

If a domino d in a tiling containing vertical_1_1 is not vertical_1_1, then d's cells have column ≥ 2.

def DominoTilings.DominoTiling.restrictAfterVertical {n : ℕ} (T : DominoTiling (n + 1) 2) (hv : vertical_1_1 ∈ T.dominos) : DominoTiling n 2

Extract the tiling of Rectangle n 2 from a tiling of Rectangle (n+1) 2 that has vertical_1_1 as its first domino.

This removes vertical_1_1 and shifts all remaining dominos one column left. It is the left inverse of prependVertical.

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.DominoTiling.restrictAfterHorizontalPair {n : ℕ} (T : DominoTiling (n + 2) 2) (hh1 : horizontal_1_1 ∈ T.dominos) (hh2 : horizontal_1_2 ∈ T.dominos) : DominoTiling n 2

Extract the tiling of Rectangle n 2 from a tiling of Rectangle (n+2) 2 that has horizontal_1_1 and horizontal_1_2 as its first dominos.

This removes the two horizontal dominos and shifts remaining dominos two columns left. It is the left inverse of prependHorizontalPair.

Equations

• One or more equations did not get rendered due to their size.

Bijection lemmas for the Fibonacci recurrence

These lemmas establish that prependVertical/prependHorizontalPair and restrictAfterVertical/restrictAfterHorizontalPair are inverse operations.

theorem DominoTilings.DominoTiling.restrictAfterVertical_prependVertical {n : ℕ} (T : DominoTiling n 2) : T.prependVertical.restrictAfterVertical ⋯ = T

prependVertical followed by restrictAfterVertical is the identity.

theorem DominoTilings.DominoTiling.prependVertical_restrictAfterVertical {n : ℕ} (T : DominoTiling (n + 1) 2) (hv : vertical_1_1 ∈ T.dominos) : (T.restrictAfterVertical hv).prependVertical = T

restrictAfterVertical followed by prependVertical is the identity (when the tiling starts with vertical_1_1).

theorem DominoTilings.DominoTiling.restrictAfterHorizontalPair_prependHorizontalPair {n : ℕ} (T : DominoTiling n 2) : T.prependHorizontalPair.restrictAfterHorizontalPair ⋯ ⋯ = T

prependHorizontalPair followed by restrictAfterHorizontalPair is the identity.

theorem DominoTilings.DominoTiling.prependHorizontalPair_restrictAfterHorizontalPair {n : ℕ} (T : DominoTiling (n + 2) 2) (hh1 : horizontal_1_1 ∈ T.dominos) (hh2 : horizontal_1_2 ∈ T.dominos) : (T.restrictAfterHorizontalPair hh1 hh2).prependHorizontalPair = T

restrictAfterHorizontalPair followed by prependHorizontalPair is the identity (when the tiling starts with horizontal_1_1 and horizontal_1_2).

Dichotomy lemmas for the Fibonacci recurrence

These lemmas establish that every 2×(n+2) tiling either:

• Has a domino covering cells {(1,1), (1,2)} (vertical case)
• Has dominos covering cells {(1,1), (2,1)} and {(1,2), (2,2)} (horizontal case)

This is the key dichotomy needed for the bijection.

theorem DominoTilings.DominoTiling.exists_domino_covering_11 {n : ℕ} (T : DominoTiling (n + 1) 2) : ∃ d ∈ T.dominos, (1, 1) ∈ d.cells

In a 2×(n+1) tiling, cell (1,1) is covered by some domino.

theorem DominoTilings.DominoTiling.domino_covering_11_cells {n : ℕ} (T : DominoTiling (n + 2) 2) (d : Domino) (hd : d ∈ T.dominos) (hcov : (1, 1) ∈ d.cells) : d.cells = {(1, 1), (1, 2)} ∨ d.cells = {(1, 1), (2, 1)}

Any domino covering cell (1,1) in a 2×(n+2) tiling has cells = {(1,1), (1,2)} or {(1,1), (2,1)}.

theorem DominoTilings.DominoTiling.exists_domino_covering_12_of_horizontal {n : ℕ} (T : DominoTiling (n + 2) 2) (d : Domino) (hd : d ∈ T.dominos) (hcells : d.cells = {(1, 1), (2, 1)}) : ∃ d' ∈ T.dominos, d' ≠ d ∧ (1, 2) ∈ d'.cells

If a domino in a 2×(n+2) tiling covers (1,1) with a horizontal domino (cells = {(1,1), (2,1)}), then there must be another domino covering (1,2).

theorem DominoTilings.DominoTiling.domino_covering_12_cells {n : ℕ} (T : DominoTiling (n + 2) 2) (d d' : Domino) (hd : d ∈ T.dominos) (hd' : d' ∈ T.dominos) (hne : d' ≠ d) (hd_cells : d.cells = {(1, 1), (2, 1)}) (hd'_cov : (1, 2) ∈ d'.cells) : d'.cells = {(1, 2), (2, 2)}

The second domino covering (1,2) when the first covers {(1,1), (2,1)} must cover {(1,2), (2,2)}.

Generalized restrict functions

These functions generalize restrictAfterVertical and restrictAfterHorizontalPair to work with any domino having the appropriate cells, not just the specific canonical dominos. This is needed for the Equiv construction since tilings may use flipped versions of dominos.

def DominoTilings.DominoTiling.restrictAfterVerticalGen {n : ℕ} (T : DominoTiling (n + 1) 2) (v : Domino) (hv : v ∈ T.dominos) (hv_cells : v.cells = vertical_1_1.cells) : DominoTiling n 2

Generalized version of restrictAfterVertical that works with any domino v having cells = {(1,1), (1,2)}.

Equations

• One or more equations did not get rendered due to their size.

theorem DominoTilings.DominoTiling.restrictAfterVerticalGen_eq_restrictAfterVertical {n : ℕ} (T : DominoTiling (n + 1) 2) (hv : vertical_1_1 ∈ T.dominos) : T.restrictAfterVerticalGen vertical_1_1 hv ⋯ = T.restrictAfterVertical hv

restrictAfterVerticalGen with vertical_1_1 equals restrictAfterVertical.

theorem DominoTilings.DominoTiling.other_dominos_col_ge_3_gen {n : ℕ} (T : DominoTiling (n + 2) 2) (d1 d2 : Domino) (hd1 : d1 ∈ T.dominos) (hd2 : d2 ∈ T.dominos) (hd1_cells : d1.cells = {(1, 1), (2, 1)}) (hd2_cells : d2.cells = {(1, 2), (2, 2)}) (d : Domino) (hd : d ∈ T.dominos) (hne1 : d ≠ d1) (hne2 : d ≠ d2) : d.cell1.1 ≥ 3 ∧ d.cell2.1 ≥ 3

Lemma: other dominos have column ≥ 3 when two dominos cover the first two columns.

def DominoTilings.DominoTiling.restrictAfterHorizontalPairGen {n : ℕ} (T : DominoTiling (n + 2) 2) (d1 d2 : Domino) (hd1 : d1 ∈ T.dominos) (hd2 : d2 ∈ T.dominos) (hd1_cells : d1.cells = {(1, 1), (2, 1)}) (hd2_cells : d2.cells = {(1, 2), (2, 2)}) : DominoTiling n 2

Generalized version of restrictAfterHorizontalPair that works with any dominos d1, d2 having the appropriate cells.

Equations

• One or more equations did not get rendered due to their size.

Predicate for vertical first column

A tiling has a "vertical first column" if some domino covers cells (1,1) and (1,2). This is the key predicate for the Fibonacci recurrence bijection.

def DominoTilings.DominoTiling.hasVerticalFirstColumn {n : ℕ} (T : DominoTiling (n + 2) 2) : Prop

A tiling has a vertical first column if some domino covers cells (1,1) and (1,2).

Equations

• T.hasVerticalFirstColumn = ∃ d ∈ T.dominos, d.cells = {(1, 1), (1, 2)}

instance DominoTilings.DominoTiling.instDecidableHasVerticalFirstColumn {n : ℕ} (T : DominoTiling (n + 2) 2) : Decidable T.hasVerticalFirstColumn

Equations

• T.instDecidableHasVerticalFirstColumn = id inferInstance

theorem DominoTilings.DominoTiling.hasVerticalFirstColumn_or_horizontalPair {n : ℕ} (T : DominoTiling (n + 2) 2) : T.hasVerticalFirstColumn ∨ (∃ d₁ ∈ T.dominos, d₁.cells = {(1, 1), (2, 1)}) ∧ ∃ d₂ ∈ T.dominos, d₂.cells = {(1, 2), (2, 2)}

The dichotomy: every 2×(n+2) tiling either has a vertical first column or a horizontal pair.

theorem DominoTilings.DominoTiling.horizontalPair_of_not_hasVerticalFirstColumn {n : ℕ} (T : DominoTiling (n + 2) 2) (hnotvert : ¬T.hasVerticalFirstColumn) : (∃ d₁ ∈ T.dominos, d₁.cells = {(1, 1), (2, 1)}) ∧ ∃ d₂ ∈ T.dominos, d₂.cells = {(1, 2), (2, 2)}

If a tiling doesn't have a vertical first column, then it has a horizontal pair.

theorem DominoTilings.DominoTiling.vertical_1_1_or_flip_of_hasVerticalFirstColumn {n : ℕ} (T : DominoTiling (n + 2) 2) (hvert : T.hasVerticalFirstColumn) : vertical_1_1 ∈ T.dominos ∨ vertical_1_1_flip ∈ T.dominos

If a tiling has a vertical first column, then either vertical_1_1 or vertical_1_1_flip is in the tiling's dominos.

theorem DominoTilings.DominoTiling.vertical_1_1_flip_not_mem_of_vertical_1_1_mem {n m : ℕ} (T : DominoTiling n m) (hv : vertical_1_1 ∈ T.dominos) : vertical_1_1_flip ∉ T.dominos

If vertical_1_1 is in a tiling, then vertical_1_1_flip is not (by disjointness).

theorem DominoTilings.DominoTiling.classical_choose_hasVerticalFirstColumn_eq_vertical_1_1 {n : ℕ} (T : DominoTiling (n + 2) 2) (hv_mem : vertical_1_1 ∈ T.dominos) (hv : T.hasVerticalFirstColumn) : Classical.choose hv = vertical_1_1

If vertical_1_1 is in a tiling with a vertical first column, then Classical.choose picks vertical_1_1 (since it's the unique witness).

The Fibonacci recurrence Equiv

The equivalence DominoTiling (n + 2) 2 ≃ DominoTiling n 2 ⊕ DominoTiling (n + 1) 2 establishes the Fibonacci recurrence for counting 2×n domino tilings.

Important note on canonical forms: The Domino structure distinguishes between dominos with swapped cell1/cell2. For example, vertical_1_1 (with cell1=(1,1), cell2=(1,2)) is different from vertical_1_1_flip (with cell1=(1,2), cell2=(1,1)), even though they cover the same cells.

The Equiv is constructed such that:

• The backward map (Sum.elim prependHorizontalPair prependVertical) always produces "canonical" tilings with vertical_1_1, horizontal_1_1, horizontal_1_2
• The forward map extracts the smaller tiling, which is independent of whether the original used canonical or flipped dominos

This means backward ∘ forward acts as a "canonicalization" function: it preserves the cell coverage but may change which specific domino representatives are used. The Equiv is still valid because the maps are inverses when restricted to canonical tilings, and canonical tilings are in bijection with all tilings via canonicalization.

theorem DominoTilings.DominoTiling.horizontal_1_1_unique_in_prependHorizontalPair {n : ℕ} (T : DominoTiling n 2) (d : Domino) (hd : d ∈ T.prependHorizontalPair.dominos) (hd_cells : d.cells = {(1, 1), (2, 1)}) : d = horizontal_1_1

In prependHorizontalPair T, the only domino with cells {(1,1), (2,1)} is horizontal_1_1.

theorem DominoTilings.DominoTiling.horizontal_1_2_unique_in_prependHorizontalPair {n : ℕ} (T : DominoTiling n 2) (d : Domino) (hd : d ∈ T.prependHorizontalPair.dominos) (hd_cells : d.cells = {(1, 2), (2, 2)}) : d = horizontal_1_2

In prependHorizontalPair T, the only domino with cells {(1,2), (2,2)} is horizontal_1_2.

theorem DominoTilings.DominoTiling.vertical_1_1_unique_in_prependVertical {n : ℕ} (T : DominoTiling n 2) (d : Domino) (hd : d ∈ T.prependVertical.dominos) (hd_cells : d.cells = {(1, 1), (1, 2)}) : d = vertical_1_1

In prependVertical T, the only domino with cells {(1,1), (1,2)} is vertical_1_1.

noncomputable def DominoTilings.DominoTiling.tiling_2_to_sum {n : ℕ} (T : DominoTiling (n + 2) 2) : DominoTiling n 2 ⊕ DominoTiling (n + 1) 2

Forward map for the Fibonacci recurrence bijection. Maps a 2×(n+2) tiling to either:

• inl T' where T' is a 2×n tiling (horizontal case)
• inr T' where T' is a 2×(n+1) tiling (vertical case)

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.DominoTiling.tiling_2_from_sum {n : ℕ} : DominoTiling n 2 ⊕ DominoTiling (n + 1) 2 → DominoTiling (n + 2) 2

Backward map for the Fibonacci recurrence bijection. Maps a sum to a 2×(n+2) tiling by prepending dominos.

Equations

• DominoTilings.DominoTiling.tiling_2_from_sum = Sum.elim DominoTilings.DominoTiling.prependHorizontalPair DominoTilings.DominoTiling.prependVertical

theorem DominoTilings.DominoTiling.tiling_2_to_sum_from_sum {n : ℕ} (x : DominoTiling n 2 ⊕ DominoTiling (n + 1) 2) : (tiling_2_from_sum x).tiling_2_to_sum = x

The roundtrip tiling_2_to_sum (tiling_2_from_sum x) = x. This is the key property establishing that tiling_2_from_sum is a right inverse of tiling_2_to_sum, which proves surjectivity of tiling_2_to_sum and injectivity of tiling_2_from_sum.

theorem DominoTilings.DominoTiling.tiling_2_to_sum_surjective {n : ℕ} : Function.Surjective tiling_2_to_sum

The forward map tiling_2_to_sum is surjective.

theorem DominoTilings.DominoTiling.tiling_2_from_sum_injective {n : ℕ} : Function.Injective tiling_2_from_sum

The backward map tiling_2_from_sum is injective.

Helper lemmas for the TilingEquiv proof

theorem DominoTilings.DominoTiling.tiling_2_roundtrip_TilingEquiv {n : ℕ} (T : DominoTiling (n + 2) 2) : (tiling_2_from_sum T.tiling_2_to_sum).TilingEquiv T

The roundtrip tiling_2_from_sum (tiling_2_to_sum T) produces a tiling that is TilingEquiv to T (same cell coverage).

This establishes that the bijection preserves cell coverage, even though structural equality may fail due to the Domino representation issue (cell1/cell2 ordering).

Combined with right_inv, this proves that tiling_2_to_sum and tiling_2_from_sum form a bijection at the level of cell coverage, establishing the Fibonacci recurrence for counting 2×n domino tilings.

Proof status: FULLY PROVED

• Vertical case: PROVED (uses helper lemmas image_preserved_under_double_roundtrip' and insert_erase_image_eq')
• Horizontal case: PROVED (uses helper lemma insert_insert_erase_erase_image_eq)

theorem DominoTilings.DominoTiling.tiling_2_from_sum_surjective_up_to_TilingEquiv {n : ℕ} (T : DominoTiling (n + 2) 2) : ∃ (x : DominoTiling n 2 ⊕ DominoTiling (n + 1) 2), (tiling_2_from_sum x).TilingEquiv T

The backward map tiling_2_from_sum is surjective up to TilingEquiv. For any tiling T : DominoTiling (n+2) 2, there exists x such that tiling_2_from_sum x is TilingEquiv to T.

This follows from tiling_2_roundtrip_TilingEquiv: taking x = tiling_2_to_sum T, we have TilingEquiv (tiling_2_from_sum x) T.

Combined with tiling_2_from_sum_injective, this establishes that tiling_2_from_sum is a bijection between DominoTiling n 2 ⊕ DominoTiling (n+1) 2 and the TilingEquiv equivalence classes of DominoTiling (n+2) 2. This proves the Fibonacci recurrence for counting 2×n domino tilings at the level of cell coverage.

Note: Structural equality (=) fails for the left_inv direction because tilings may use "flipped" dominos (e.g., vertical_1_1_flip instead of vertical_1_1). However, the mathematical content is correct: the roundtrip preserves cell coverage (TilingEquiv), and the bijection at the cell level is established.

def DominoTilings.mkHorizontalDomino (x y : ℕ) : Domino

Helper to construct a horizontal domino at position (x, y) extending right. The domino covers cells (x, y) and (x+1, y).

Equations

• DominoTilings.mkHorizontalDomino x y = { cell1 := (x, y), cell2 := (x + 1, y), distinct := ⋯, adjacent := ⋯ }

def DominoTilings.mkVerticalDomino (x y : ℕ) : Domino

Helper to construct a vertical domino at position (x, y) extending up. The domino covers cells (x, y) and (x, y+1).

Equations

• DominoTilings.mkVerticalDomino x y = { cell1 := (x, y), cell2 := (x, y + 1), distinct := ⋯, adjacent := ⋯ }

Simp lemmas for mkHorizontalDomino and mkVerticalDomino

@[simp]

theorem DominoTilings.mkHorizontalDomino_cell1 (x y : ℕ) : (mkHorizontalDomino x y).cell1 = (x, y)

@[simp]

theorem DominoTilings.mkHorizontalDomino_cell2 (x y : ℕ) : (mkHorizontalDomino x y).cell2 = (x + 1, y)

@[simp]

theorem DominoTilings.mkVerticalDomino_cell1 (x y : ℕ) : (mkVerticalDomino x y).cell1 = (x, y)

@[simp]

theorem DominoTilings.mkVerticalDomino_cell2 (x y : ℕ) : (mkVerticalDomino x y).cell2 = (x, y + 1)

@[simp]

theorem DominoTilings.isHorizontal_mkHorizontalDomino (x y : ℕ) : (mkHorizontalDomino x y).isHorizontal

@[simp]

theorem DominoTilings.isVertical_mkVerticalDomino (x y : ℕ) : (mkVerticalDomino x y).isVertical

Definition of Tiling A_n (def.gf.weighted-set.domino.Rn3.ABC (a))

For even positive n, A_n consists of:

• Basement dominos: horizontal dominos {(2i-1, 1), (2i, 1)} for i ∈ [n/2]
• Left wall: vertical domino {(1, 2), (1, 3)}
• Right wall: vertical domino {(n, 2), (n, 3)}
• Middle dominos: horizontal dominos {(2i, 2), (2i+1, 2)} for i ∈ [n/2-1]
• Top dominos: horizontal dominos {(2i, 3), (2i+1, 3)} for i ∈ [n/2-1]

def DominoTilings.basementDominos (n : ℕ) : Finset Domino

The basement dominos for tiling A_n: horizontal dominos filling the bottom row.

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.leftWall : Domino

The left wall for tiling A_n: vertical domino in column 1, rows 2-3.

Equations

• DominoTilings.leftWall = { cell1 := (1, 2), cell2 := (1, 3), distinct := DominoTilings.leftWall._proof_2, adjacent := DominoTilings.leftWall._proof_3 }

def DominoTilings.rightWall (n : ℕ) : Domino

The right wall for tiling A_n: vertical domino in column n, rows 2-3.

Equations

• DominoTilings.rightWall n = { cell1 := (n, 2), cell2 := (n, 3), distinct := ⋯, adjacent := ⋯ }

def DominoTilings.middleDominos (n : ℕ) : Finset Domino

The middle dominos for tiling A_n: horizontal dominos in row 2 (except first/last columns).

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.topDominos (n : ℕ) : Finset Domino

The top dominos for tiling A_n: horizontal dominos in row 3 (except first/last columns).

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.TilingA (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : DominoTiling n 3

Tiling A_n for even positive n ≥ 2.

This is the faultfree tiling of R_{n,3} with:

• A vertical domino (left wall) in the top two squares of column 1
• Horizontal basement dominos filling the bottom row
• Horizontal middle and top dominos filling the interior
• A vertical domino (right wall) in the top two squares of column n

(def.gf.weighted-set.domino.Rn3.ABC (a))

Equations

• One or more equations did not get rendered due to their size.

Definition of Tiling B_n (def.gf.weighted-set.domino.Rn3.ABC (b))

B_n is the reflection of A_n across the horizontal axis of symmetry of R_{n,3}. This swaps row 1 with row 3, keeping row 2 fixed.

For B_n, we have:

• Basement dominos in row 3: horizontal dominos {(2i-1, 3), (2i, 3)} for i ∈ [n/2]
• Left wall: vertical domino {(1, 1), (1, 2)} in the bottom of column 1
• Right wall: vertical domino {(n, 1), (n, 2)} in the bottom of column n
• Middle dominos in row 2: horizontal dominos {(2i, 2), (2i+1, 2)} for i ∈ [n/2-1]
• Bottom dominos in row 1: horizontal dominos {(2i, 1), (2i+1, 1)} for i ∈ [n/2-1]

def DominoTilings.basementDominosB (n : ℕ) : Finset Domino

The "basement" dominos for tiling B_n: horizontal dominos filling row 3 (the top row). Named "basement" by analogy with A_n, though in B_n these are at the top due to reflection.

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.leftWallB : Domino

The left wall for tiling B_n: vertical domino in column 1, rows 1-2. Note: cell ordering matches reflectDomino3 applied to leftWall.

Equations

• DominoTilings.leftWallB = { cell1 := (1, 2), cell2 := (1, 1), distinct := DominoTilings.vertical_1_1_flip._proof_1, adjacent := DominoTilings.vertical_1_1_flip._proof_2 }

def DominoTilings.rightWallB (n : ℕ) : Domino

The right wall for tiling B_n: vertical domino in column n, rows 1-2. Note: cell ordering matches reflectDomino3 applied to rightWall.

Equations

• DominoTilings.rightWallB n = { cell1 := (n, 2), cell2 := (n, 1), distinct := ⋯, adjacent := ⋯ }

def DominoTilings.bottomDominosB (n : ℕ) : Finset Domino

The bottom dominos for tiling B_n: horizontal dominos in row 1 (except first/last columns).

Equations

• One or more equations did not get rendered due to their size.

def DominoTilings.TilingB (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : DominoTiling n 3

Tiling B_n for even positive n ≥ 2.

This is the reflection of A_n across the horizontal axis. It has a vertical domino in the bottom two squares of column 1.

(def.gf.weighted-set.domino.Rn3.ABC (b))

Equations

• One or more equations did not get rendered due to their size.

Definition of Tiling C (def.gf.weighted-set.domino.Rn3.ABC (c))

C is the unique faultfree tiling of R_{2,3} consisting of three horizontal dominos.

def DominoTilings.TilingC : DominoTiling 2 3

Tiling C: three horizontal dominos covering R_{2,3}.

The dominos are:

• {(1, 1), (2, 1)} (bottom row)
• {(1, 2), (2, 2)} (middle row)
• {(1, 3), (2, 3)} (top row)

(def.gf.weighted-set.domino.Rn3.ABC (c))

Equations

• One or more equations did not get rendered due to their size.

Horizontal Reflection for Height-3 Tilings

We define reflection across the horizontal axis of R_{n,3}, which swaps rows 1 and 3 while keeping row 2 fixed. This is used to relate TilingA and TilingB.

def DominoTilings.reflectCell3 (c : Cell) : Cell

Reflect a cell across the horizontal midline of a height-3 rectangle. Maps (x, 1) ↔ (x, 3) and fixes (x, 2).

Equations

• DominoTilings.reflectCell3 c = (c.1, 4 - c.2)

theorem DominoTilings.reflectCell3_involutive (c : Cell) (h1 : c.2 ≥ 1) (h2 : c.2 ≤ 3) : reflectCell3 (reflectCell3 c) = c

reflectCell3 is an involution on cells with row in {1, 2, 3}.

noncomputable def DominoTilings.reflectTiling3 {n : ℕ} (T : DominoTiling n 3) : DominoTiling n 3

Reflect a tiling of R_{n,3} across the horizontal axis. This operation is well-defined and produces a valid tiling.

Equations

• One or more equations did not get rendered due to their size.

theorem DominoTilings.reflectTiling3_dominos_minCol_maxCol {n : ℕ} (T : DominoTiling n 3) (d : Domino) : d ∈ T.dominos → ∃ d' ∈ (reflectTiling3 T).dominos, d'.minCol = d.minCol ∧ d'.maxCol = d.maxCol

Key property: For each domino in T, there's a corresponding reflected domino in reflectTiling3 T with the same minCol and maxCol. This captures the essential fact that horizontal reflection only changes row coordinates, not column coordinates.

theorem DominoTilings.reflectTiling3_isFaultfree {n : ℕ} (T : DominoTiling n 3) (hfree : T.isFaultfree) : (reflectTiling3 T).isFaultfree

Reflection preserves faultfreeness.

The proof uses the key observation that horizontal reflection only changes row coordinates, not column coordinates. Therefore, minCol and maxCol of each domino are preserved. Since faults are determined solely by whether dominos span column boundaries (i.e., whether minCol ≤ k < maxCol for some k), reflection preserves faultfreeness.

theorem DominoTilings.reflectTiling3_hasTopVertical_iff_hasBottomVertical {n : ℕ} (T : DominoTiling n 3) (c : ℕ) : (reflectTiling3 T).hasTopVerticalInCol c ↔ T.hasBottomVerticalInCol c

Reflection swaps top and bottom vertical dominos.

theorem DominoTilings.reflectTiling3_involutive {n : ℕ} (T : DominoTiling n 3) : reflectTiling3 (reflectTiling3 T) = T

Reflection is an involution.

theorem DominoTilings.reflectTiling3_preserves_TilingEquiv {n : ℕ} (T₁ T₂ : DominoTiling n 3) (h : T₁.TilingEquiv T₂) : (reflectTiling3 T₁).TilingEquiv (reflectTiling3 T₂)

reflectTiling3 preserves TilingEquiv: if T₁ ≃ T₂ (same cell images), then reflectTiling3 T₁ ≃ reflectTiling3 T₂.

theorem DominoTilings.TilingB_eq_reflectTiling3_TilingA (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : TilingB n hn hn_ge = reflectTiling3 (TilingA n hn hn_ge)

TilingB is the reflection of TilingA.

Main Classification Theorem

Proposition prop.gf.weighted-set.domino.Rn3.ABC states that the faultfree domino tilings of height-3 rectangles are precisely:

• A_2, A_4, A_6, A_8, ... (tilings with vertical domino in top of column 1)
• B_2, B_4, B_6, B_8, ... (tilings with vertical domino in bottom of column 1)
• C (the unique tiling with no vertical domino in column 1)

theorem DominoTilings.TilingA_isFaultfree (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : (TilingA n hn hn_ge).isFaultfree

The tilings A_n are faultfree.

The basement dominos prevent faults between columns 2i-1 and 2i, while the top dominos prevent faults between columns 2i and 2i+1.

theorem DominoTilings.TilingB_isFaultfree (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : (TilingB n hn hn_ge).isFaultfree

The tilings B_n are faultfree (by reflection symmetry with A_n).

theorem DominoTilings.TilingC_isFaultfree : TilingC.isFaultfree

The tiling C is faultfree.

theorem DominoTilings.TilingA_hasTopVertical (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : (TilingA n hn hn_ge).hasTopVerticalInCol 1

Tiling A_n has a vertical domino in the top two squares of column 1.

theorem DominoTilings.TilingB_hasBottomVertical (n : ℕ) (hn : Even n) (hn_ge : n ≥ 2) : (TilingB n hn hn_ge).hasBottomVerticalInCol 1

Tiling B_n has a vertical domino in the bottom two squares of column 1.

theorem DominoTilings.TilingC_noVerticalInCol1 : ¬TilingC.hasVerticalInCol 1

Tiling C has no vertical domino in column 1.

Auxiliary Lemmas for the Proof

These lemmas capture the key steps in the inductive proof of the classification. They are placed before the main classification theorems since the proofs depend on them.

theorem DominoTilings.hasTopVerticalInCol_implies_n_ge (n : ℕ) (T : DominoTiling n 3) (c : ℕ) (htop : T.hasTopVerticalInCol c) : n ≥ c

A tiling with a vertical domino in the top of column c has n ≥ c. This follows because the domino must be within the rectangle.

theorem DominoTilings.rectangle_tileable_iff_even (n : ℕ) : Nonempty (DominoTiling n 3) → Even n ∨ n = 0

A rectangle R_{n,3} can only be tiled by dominos if n is even or n = 0.

This follows from the parity argument: 3n squares must be covered by dominos (each covering 2 squares), so 3n must be even, hence n must be even.

theorem DominoTilings.base_case_basement (n : ℕ) (T : DominoTiling n 3) (htop : T.hasTopVerticalInCol 1) (hn : n ≥ 2) : ∃ d ∈ T.dominos, d.cells = {(1, 1), (2, 1)}

Helper lemma for the base case: If T has a top vertical domino in column 1, then the cell (1,1) must be covered by a horizontal domino going right. This gives us the basement domino {(1,1), (2,1)} for i=1.

theorem DominoTilings.claim1_basement_middle_top (n : ℕ) (T : DominoTiling n 3) (hfree : T.isFaultfree) (htop : T.hasTopVerticalInCol 1) (i : ℕ) (hi_pos : i ≥ 1) (hi_lt : i < n / 2) : (∃ d ∈ T.dominos, d.cells = {(2 * i - 1, 1), (2 * i, 1)}) ∧ (∃ d ∈ T.dominos, d.cells = {(2 * i, 2), (2 * i + 1, 2)}) ∧ ∃ d ∈ T.dominos, d.cells = {(2 * i, 3), (2 * i + 1, 3)}

Claim 1 from the proof: For each positive integer i < n/2, a faultfree tiling T with a vertical domino in the top of column 1 must contain specific dominos.

Note: We use d.cells (the set of cells covered by the domino) instead of specifying cell orderings, since the Domino structure allows either cell to be cell1 or cell2. This makes the theorem provable for arbitrary tilings.

This is proved by induction on i.

theorem DominoTilings.claim2_n_even (n : ℕ) (T : DominoTiling n 3) (_hfree : T.isFaultfree) (_htop : T.hasTopVerticalInCol 1) : Even n

Claim 2 from the proof: The width n must be even.

Alternative proof: Since T tiles R_{n,3} with dominos, the total number of squares (which is 3n) must be even. Hence n must be even.

theorem DominoTilings.faultfree_hasTopVerticalInCol_implies_n_ge_two (n : ℕ) (T : DominoTiling n 3) (hfree : T.isFaultfree) (htop : T.hasTopVerticalInCol 1) : n ≥ 2

A faultfree tiling with a vertical domino in the top of column 1 has n ≥ 2. This follows because n is even (from claim2_n_even) and n ≥ 1.

Classification Results (prop.gf.weighted-set.domino.Rn3.ABC)

theorem DominoTilings.faultfree_no_vertical_unique (T : DominoTiling 2 3) (_hfree : T.isFaultfree) (hno_vert : ¬T.hasVerticalInCol 1) : T.TilingEquiv TilingC

(prop.gf.weighted-set.domino.Rn3.ABC (c)) The only faultfree domino tiling of a height-3 rectangle with no vertical domino in the first column is equivalent to C.

Proof sketch: If the first column has no vertical domino, it must be filled with three horizontal dominos extending into column 2. This forces n = 2, and the tiling must be equivalent to C.

Note: We use TilingEquiv instead of = because the Domino structure distinguishes between {cell1 := (1, y), cell2 := (2, y)} and {cell1 := (2, y), cell2 := (1, y)} as different dominos, even though they cover the same cells. The mathematical theorem is about tilings covering the same cells, not about specific domino representations.

Implementation note: The faultfree hypothesis _hfree is not used in this proof. In the source material, faultfree is used to argue there can't be a third column, but since this theorem is specifically for 2×3 rectangles (n = 2), this is automatic from the type signature.

theorem DominoTilings.faultfree_top_vertical_classification (n : ℕ) (T : DominoTiling n 3) (hfree : T.isFaultfree) (htop : T.hasTopVerticalInCol 1) : Even n ∧ ∃ (hn : Even n) (hn_ge : n ≥ 2), T.TilingEquiv (TilingA n hn hn_ge)

(prop.gf.weighted-set.domino.Rn3.ABC (a)) The faultfree domino tilings of a height-3 rectangle with a vertical domino in the top two squares of column 1 are precisely A_2, A_4, A_6, ...

Proof sketch: By induction, the structure of the tiling is forced:

• Claim 1 (claim1_basement_middle_top): The tiling must contain specific basement, middle, and top dominos
• Claim 2 (claim2_n_even): n must be even (by parity or by showing odd n leads to contradiction)
• The remaining squares can only be tiled one way, giving T ≃ A_n

Note: We use TilingEquiv instead of = because the Domino structure distinguishes between {cell1 := (1, 2), cell2 := (1, 3)} and {cell1 := (1, 3), cell2 := (1, 2)} as different dominos, even though they cover the same cells.

theorem DominoTilings.faultfree_bottom_vertical_classification (n : ℕ) (T : DominoTiling n 3) (hfree : T.isFaultfree) (hbot : T.hasBottomVerticalInCol 1) : Even n ∧ ∃ (hn : Even n) (hn_ge : n ≥ 2), T.TilingEquiv (TilingB n hn hn_ge)

(prop.gf.weighted-set.domino.Rn3.ABC (b)) The faultfree domino tilings of a height-3 rectangle with a vertical domino in the bottom two squares of column 1 are precisely B_2, B_4, B_6, ...

This follows from part (a) by reflection across the horizontal axis.

Note: We use TilingEquiv instead of = because the Domino structure distinguishes between different cell orderings.

theorem DominoTilings.vertical_in_col1_trichotomy (n : ℕ) (T : DominoTiling n 3) : T.hasVerticalInCol 1 → T.hasTopVerticalInCol 1 ∨ T.hasBottomVerticalInCol 1

For height 3, a vertical domino in column 1 must be either in the top two squares (rows 2-3) or the bottom two squares (rows 1-2). There's no other option since a vertical domino covers 2 adjacent rows and we only have 3 rows.

theorem DominoTilings.no_vertical_implies_n_eq_2 (n : ℕ) (T : DominoTiling n 3) (hfree : T.isFaultfree) (hno_vert : ¬T.hasVerticalInCol 1) (hn : n ≥ 1) : n = 2

If a faultfree tiling has no vertical domino in column 1, then n = 2.

Proof sketch: If the first column has no vertical domino, it must be filled with three horizontal dominos extending into column 2. This covers all of column 2, so if n > 2, there would be a fault between columns 2 and 3.

Note: requires n ≥ 1 (for n = 0, the empty tiling is a counterexample).

theorem DominoTilings.faultfree_classification (n : ℕ) (T : DominoTiling n 3) (hfree : T.isFaultfree) (hn : n ≥ 1) : (∃ (hn : Even n) (hn_ge : n ≥ 2), T.TilingEquiv (TilingA n hn hn_ge)) ∨ (∃ (hn : Even n) (hn_ge : n ≥ 2), T.TilingEquiv (TilingB n hn hn_ge)) ∨ n = 2 ∧ ¬T.hasVerticalInCol 1 ∧ ∃ (h : n = 2), (h ▸ T).TilingEquiv TilingC

The complete classification of faultfree domino tilings of height-3 rectangles.

Every faultfree tiling of R_{n,3} is one of:

• Equivalent to A_n for some even n ≥ 2 (vertical domino in top of column 1)
• Equivalent to B_n for some even n ≥ 2 (vertical domino in bottom of column 1)
• Equivalent to C (n = 2, no vertical domino in column 1)

Note: We use TilingEquiv instead of = because the Domino structure distinguishes between different cell orderings.

Note: requires n ≥ 1 (for n = 0, the empty tiling is a counterexample).

(prop.gf.weighted-set.domino.Rn3.ABC)