The Generating Function of a Weighted Set

This file formalizes the theory of weighted sets and their weight generating functions, following Section sec.gf.weighted-set of the Algebraic Combinatorics notes.

A weighted set is a set equipped with a weight function to ℕ. When the set is "finite-type" (only finitely many elements of each weight), we can define its weight generating function as a formal power series.

Main Definitions

• WeightedSet: A set with a weight function to ℕ
• WeightedSet.IsFiniteType: Predicate for finite-type weighted sets
• WeightedSet.weightGenFun: The weight generating function of a finite-type weighted set
• WeightedSet.Isomorphism: Weight-preserving bijections between weighted sets
• WeightedSet.disjointUnion: Disjoint union of weighted sets (A + B)
• WeightedSet.prod: Product of weighted sets (A × B) with additive weights
• WeightedSet.pow: Cartesian power of a weighted set
• WeightedSet.tuples: Infinite disjoint union W^0 + W^1 + W^2 + ... (Kleene star)

Main Results

• WeightedSet.weightGenFun_eq_of_isomorphic: Isomorphic weighted sets have equal generating functions
• WeightedSet.weightGenFun_disjointUnion: ḡ(A + B) = ḡ(A) + ḡ(B)
• WeightedSet.weightGenFun_prod: ḡ(A × B) = ḡ(A) · ḡ(B)
• WeightedSet.weightGenFun_pow: ḡ(A^k) = ḡ(A)^k
• DominoTilingsZ.tiling_decomposition_isomorphism: D ≅ F^0 + F^1 + F^2 + ... (Lemma lem.gf.weighted-set.domino.fd)

Applications

The file includes applications to:

• Counting compositions (recovering the formula for the generating function of compositions)
• Domino tilings of height-2 rectangles (connection to Fibonacci numbers)

Note: Height-3 domino tilings are handled in Details/DominoTilings.lean.

References

• [Flajolet and Sedgewick, Analytic Combinatorics, Part A][FlaSed09]
• [Fink, Enumerative Combinatorics, §3.3-§3.4][Fink17]

Tags

weighted set, generating function, combinatorial class, domino tiling

Weighted Sets

structure WeightedSet (α : Type u_2) : Type u_2

A weighted set is a type equipped with a weight function to ℕ. (Definition \ref{def.gf-ws.weighted-sets}(a))

• weight : α → ℕ

  The weight function assigning a natural number to each element

def WeightedSet.IsFiniteType {α : Type u_2} (W : WeightedSet α) : Prop

A weighted set is finite-type if for each n ∈ ℕ, there are only finitely many elements of weight n. (Definition \ref{def.gf-ws.weighted-sets}(b))

Equations

• W.IsFiniteType = ∀ (n : ℕ), {a : α | W.weight a = n}.Finite

def WeightedSet.elementsOfWeight {α : Type u_2} (W : WeightedSet α) (n : ℕ) : Set α

The set of elements of a given weight in a weighted set

Equations

• W.elementsOfWeight n = {a : α | W.weight a = n}

def WeightedSet.countOfWeight {α : Type u_2} (W : WeightedSet α) (hft : W.IsFiniteType) (n : ℕ) : ℕ

For a finite-type weighted set, the count of elements of weight n

Equations

• W.countOfWeight hft n = ⋯.toFinset.card

Weight Generating Function

def WeightedSet.weightGenFun {R : Type u_1} [CommSemiring R] {α : Type u_2} (W : WeightedSet α) (hft : W.IsFiniteType) : PowerSeries R

The weight generating function of a finite-type weighted set is the FPS ∑_{n ∈ ℕ} (# of elements of weight n) · x^n. (Definition \ref{def.gf-ws.weighted-sets}(c))

Equations

• W.weightGenFun hft = PowerSeries.mk fun (n : ℕ) => ↑(W.countOfWeight hft n)

theorem WeightedSet.weightGenFun_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (W : WeightedSet α) (hft : W.IsFiniteType) : W.weightGenFun hft = PowerSeries.mk fun (n : ℕ) => ↑⋯.toFinset.card

Alternative characterization: weightGenFun = ∑_{a ∈ A} x^{|a|}

Isomorphisms of Weighted Sets

structure WeightedSet.Isomorphism {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) : Type (max u_2 u_3)

An isomorphism between weighted sets is a weight-preserving bijection. (Definition \ref{def.gf-ws.weighted-sets}(d))

• toEquiv : α ≃ β

  The underlying bijection

• weight_eq (a : α) : W₂.weight (self.toEquiv a) = W₁.weight a

  The bijection preserves weights

def WeightedSet.AreIsomorphic {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) : Prop

Two weighted sets are isomorphic if there exists an isomorphism between them. (Definition \ref{def.gf-ws.weighted-sets}(e))

Equations

• (W₁ ≅ᵥ W₂) = Nonempty (W₁.Isomorphism W₂)

def WeightedSet.«term_≅ᵥ_» : Lean.TrailingParserDescr

Equations

• WeightedSet.«term_≅ᵥ_» = Lean.ParserDescr.trailingNode `WeightedSet.«term_≅ᵥ_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ᵥ ") (Lean.ParserDescr.cat `term 0))

theorem WeightedSet.weightGenFun_eq_of_isomorphic {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (hft₁ : W₁.IsFiniteType) (hft₂ : W₂.IsFiniteType) (h : W₁ ≅ᵥ W₂) : W₁.weightGenFun hft₁ = W₂.weightGenFun hft₂

Isomorphic finite-type weighted sets have equal weight generating functions. (Proposition \ref{prop.gf-ws.iso})

Disjoint Union of Weighted Sets

def WeightedSet.disjointUnion {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) : WeightedSet (α ⊕ β)

The disjoint union of two weighted sets, with weights inherited from each component. (Definition \ref{def.gf-ws.djun})

Equations

• W₁ +ᵥ W₂ = { weight := Sum.elim W₁.weight W₂.weight }

def WeightedSet.«term_+ᵥ_» : Lean.TrailingParserDescr

Equations

• WeightedSet.«term_+ᵥ_» = Lean.ParserDescr.trailingNode `WeightedSet.«term_+ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +ᵥ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem WeightedSet.disjointUnion_weight_inl {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (a : α) : (W₁ +ᵥ W₂).weight (Sum.inl a) = W₁.weight a

@[simp]

theorem WeightedSet.disjointUnion_weight_inr {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (b : β) : (W₁ +ᵥ W₂).weight (Sum.inr b) = W₂.weight b

theorem WeightedSet.disjointUnion_isFiniteType {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (hft₁ : W₁.IsFiniteType) (hft₂ : W₂.IsFiniteType) : (W₁ +ᵥ W₂).IsFiniteType

The disjoint union of finite-type weighted sets is finite-type.

theorem WeightedSet.weightGenFun_disjointUnion {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (hft₁ : W₁.IsFiniteType) (hft₂ : W₂.IsFiniteType) : (W₁ +ᵥ W₂).weightGenFun ⋯ = W₁.weightGenFun hft₁ + W₂.weightGenFun hft₂

The weight generating function of a disjoint union is the sum of the generating functions. (Proposition \ref{prop.gf-ws.djun})

Product of Weighted Sets

def WeightedSet.prod {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) : WeightedSet (α × β)

The product of two weighted sets, with weight defined as the sum of component weights. (Definition \ref{def.gf-ws.prod})

Equations

• W₁ ×ᵥ W₂ = { weight := fun (x : α × β) => match x with | (a, b) => W₁.weight a + W₂.weight b }

def WeightedSet.«term_×ᵥ_» : Lean.TrailingParserDescr

Equations

• WeightedSet.«term_×ᵥ_» = Lean.ParserDescr.trailingNode `WeightedSet.«term_×ᵥ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ᵥ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem WeightedSet.prod_weight {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (p : α × β) : (W₁ ×ᵥ W₂).weight p = W₁.weight p.1 + W₂.weight p.2

theorem WeightedSet.prod_isFiniteType {α : Type u_2} {β : Type u_3} (W₁ : WeightedSet α) (W₂ : WeightedSet β) (hft₁ : W₁.IsFiniteType) (hft₂ : W₂.IsFiniteType) : (W₁ ×ᵥ W₂).IsFiniteType

The product of finite-type weighted sets is finite-type. (Proof of first part of Proposition \ref{prop.gf-ws.prod})

theorem WeightedSet.weightGenFun_prod {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq β] (W₁ : WeightedSet α) (W₂ : WeightedSet β) (hft₁ : W₁.IsFiniteType) (hft₂ : W₂.IsFiniteType) : (W₁ ×ᵥ W₂).weightGenFun ⋯ = W₁.weightGenFun hft₁ * W₂.weightGenFun hft₂

The weight generating function of a product is the product of the generating functions. (Proposition \ref{prop.gf-ws.prod})

This is the key theorem showing that the weight generating function respects Cartesian products: ḡ(A × B) = ḡ(A) · ḡ(B). The proof partitions the pairs of total weight n by the weight of the first component, showing this equals the convolution sum that defines multiplication of power series.

Cartesian Powers

def WeightedSet.pow {α : Type u_2} (W : WeightedSet α) (k : ℕ) : WeightedSet (Fin k → α)

The k-th Cartesian power of a weighted set. Weight of (a₁, ..., aₖ) is |a₁| + ... + |aₖ|.

Equations

• W.pow k = { weight := fun (f : Fin k → α) => ∑ i : Fin k, W.weight (f i) }

theorem WeightedSet.pow_isFiniteType {α : Type u_2} (W : WeightedSet α) (hft : W.IsFiniteType) (k : ℕ) : (W.pow k).IsFiniteType

The k-th power of a finite-type weighted set is finite-type.

def WeightedSet.pow_succ_equiv {α : Type u_2} (W : WeightedSet α) (n : ℕ) : (W.pow (n + 1)).Isomorphism (W ×ᵥ W.pow n)

Helper: pow (n+1) is isomorphic to W × pow n

Equations

• W.pow_succ_equiv n = { toEquiv := (Fin.succFunEquiv α n).trans (Equiv.prodComm (Fin n → α) α), weight_eq := ⋯ }

theorem WeightedSet.weightGenFun_pow {R : Type u_1} [CommSemiring R] {α : Type u_2} (W : WeightedSet α) (hft : W.IsFiniteType) (k : ℕ) : (W.pow k).weightGenFun ⋯ = W.weightGenFun hft ^ k

The weight generating function of A^k is (ḡ(A))^k. (Proposition \ref{prop.gf-ws.pow})

Infinite Disjoint Union (Tuples)

def WeightedSet.tuples {α : Type u_2} (W : WeightedSet α) : WeightedSet ((n : ℕ) × (Fin n → α))

The infinite disjoint union W^0 + W^1 + W^2 + ... of all tuples of elements. This is the "Kleene star" construction on weighted sets. An element is a pair (k, f) where k ∈ ℕ and f : Fin k → α is a k-tuple. The weight of (k, f) is the sum of weights of the entries: ∑ᵢ |f(i)|.

Equations

• W.tuples = { weight := fun (x : (n : ℕ) × (Fin n → α)) => match x with | ⟨n, f⟩ => ∑ i : Fin n, W.weight (f i) }

theorem WeightedSet.tuples_weight_eq_pow {α : Type u_2} (W : WeightedSet α) (n : ℕ) (f : Fin n → α) : W.tuples.weight ⟨n, f⟩ = (W.pow n).weight f

The weight in the tuples weighted set equals the weight in the corresponding power

def WeightedSet.HasPositiveWeights {α : Type u_2} (W : WeightedSet α) : Prop

A weighted set has positive weights if every element has weight ≥ 1

Equations

• W.HasPositiveWeights = ∀ (a : α), W.weight a ≥ 1

theorem WeightedSet.tuples_isFiniteType {α : Type u_2} (W : WeightedSet α) (hft : W.IsFiniteType) (hpos : W.HasPositiveWeights) : W.tuples.IsFiniteType

The tuples weighted set is finite-type if the original is finite-type and has positive weights.

Note: The hypothesis hpos : W.HasPositiveWeights is necessary. Without it, the theorem is false: if W has elements of weight 0, then for any weight m, there are infinitely many tuples of weight m (we can have arbitrarily many weight-0 elements in a tuple). For example, if W = ℕ with weight = id, then tuples of weight 2 include ⟨1, ![2]⟩, ⟨2, ![0, 2]⟩, ⟨3, ![0, 0, 2]⟩, etc.

The key insight is that with positive weights, a tuple of length n has weight ≥ n, so for weight m, we only need to consider tuples of length ≤ m.

Examples and Applications

Binary Strings (Example \ref{exa.ws.bin-string1})

def WeightedSetExamples.BinaryStrings : WeightedSet (List (Fin 2))

Binary strings (finite tuples of 0s and 1s) with weight = length

Equations

• WeightedSetExamples.BinaryStrings = { weight := List.length }

theorem WeightedSetExamples.binaryStrings_isFiniteType : BinaryStrings.IsFiniteType

The binary strings weighted set is finite-type

theorem WeightedSetExamples.weightGenFun_binaryStrings : BinaryStrings.weightGenFun binaryStrings_isFiniteType = PowerSeries.mk fun (n : ℕ) => 2 ^ n

The generating function of binary strings is 1/(1-2x). Since (mk 1) represents 1 + x + x² + ... = 1/(1-x), we express 1/(1-2x) differently.

Positive Integers

def WeightedSetExamples.PositiveIntegers : WeightedSet ℕ+

The positive integers with weight = value

Equations

• WeightedSetExamples.PositiveIntegers = { weight := fun (n : ℕ+) => ↑n }

theorem WeightedSetExamples.positiveIntegers_isFiniteType : PositiveIntegers.IsFiniteType

Positive integers form a finite-type weighted set

theorem WeightedSetExamples.weightGenFun_positiveIntegers : PositiveIntegers.weightGenFun positiveIntegers_isFiniteType = PowerSeries.X * ↑(PowerSeries.invOneSubPow ℚ 1)

The generating function of positive integers is x + x² + x³ + ... = x/(1-x)

Compositions

def WeightedSetExamples.Compositions (k : ℕ) : WeightedSet (Fin k → ℕ+)

Compositions of length k are k-tuples of positive integers

Equations

• WeightedSetExamples.Compositions k = WeightedSetExamples.PositiveIntegers.pow k

theorem WeightedSetExamples.compositions_isFiniteType (k : ℕ) : (Compositions k).IsFiniteType

Compositions form a finite-type weighted set

theorem WeightedSetExamples.weightGenFun_compositions (k : ℕ) : (Compositions k).weightGenFun ⋯ = (PowerSeries.X * ↑(PowerSeries.invOneSubPow ℚ 1)) ^ k

The generating function of compositions of length k is (x/(1-x))^k

Domino Tilings

Shapes and Dominos (Definition \ref{def.domino.shapes-and-tilings})

@[reducible, inline]

abbrev DominoTilingsZ.Shape : Type

A shape is a subset of ℤ² (Definition \ref{def.domino.shapes-and-tilings}(a))

Equations

• DominoTilingsZ.Shape = Set (ℤ × ℤ)

def DominoTilingsZ.Rectangle (n m : ℕ) : Shape

The n × m rectangle (Definition \ref{def.domino.shapes-and-tilings}(b))

Equations

• DominoTilingsZ.Rectangle n m = {p : ℤ × ℤ | 1 ≤ p.1 ∧ p.1 ≤ ↑n ∧ 1 ≤ p.2 ∧ p.2 ≤ ↑m}

theorem DominoTilingsZ.mem_rectangle_iff {n m : ℕ} {p : ℤ × ℤ} : p ∈ Rectangle n m ↔ 1 ≤ p.1 ∧ p.1 ≤ ↑n ∧ 1 ≤ p.2 ∧ p.2 ≤ ↑m

Membership in a rectangle

@[simp]

theorem DominoTilingsZ.Rectangle_zero_left (m : ℕ) : Rectangle 0 m = ∅

The 0 × m rectangle is empty

@[simp]

theorem DominoTilingsZ.Rectangle_zero_right (n : ℕ) : Rectangle n 0 = ∅

The n × 0 rectangle is empty

theorem DominoTilingsZ.Rectangle_ncard (n m : ℕ) : Set.ncard (Rectangle n m) = n * m

The rectangle has n * m cells

inductive DominoTilingsZ.Domino : Type

A domino is either horizontal or vertical (Definition \ref{def.domino.shapes-and-tilings}(c))

• horizontal (i j : ℤ) : Domino
• vertical (i j : ℤ) : Domino

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

Equations

• One or more equations did not get rendered due to their size.
• DominoTilingsZ.instDecidableEqDomino.decEq (DominoTilingsZ.Domino.horizontal i j) (DominoTilingsZ.Domino.vertical i_1 j_1) = isFalse ⋯
• DominoTilingsZ.instDecidableEqDomino.decEq (DominoTilingsZ.Domino.vertical i j) (DominoTilingsZ.Domino.horizontal i_1 j_1) = isFalse ⋯

instance DominoTilingsZ.instDecidableEqDomino : DecidableEq Domino

Equations

• DominoTilingsZ.instDecidableEqDomino = DominoTilingsZ.instDecidableEqDomino.decEq

def DominoTilingsZ.Domino.toShape : Domino → Shape

The cells covered by a domino

Equations

• (DominoTilingsZ.Domino.horizontal i j).toShape = {(i, j), (i + 1, j)}
• (DominoTilingsZ.Domino.vertical i j).toShape = {(i, j), (i, j + 1)}

theorem DominoTilingsZ.Domino.toShape_ncard (d : Domino) : Set.ncard d.toShape = 2

A domino covers exactly 2 cells

@[simp]

theorem DominoTilingsZ.Domino.horizontal_toShape (i j : ℤ) : (horizontal i j).toShape = {(i, j), (i + 1, j)}

A horizontal domino covers the cells (i,j) and (i+1,j)

@[simp]

theorem DominoTilingsZ.Domino.vertical_toShape (i j : ℤ) : (vertical i j).toShape = {(i, j), (i, j + 1)}

A vertical domino covers the cells (i,j) and (i,j+1)

theorem DominoTilingsZ.Domino.toShape_nonempty (d : Domino) : Set.Nonempty d.toShape

The shape of a domino is nonempty

theorem DominoTilingsZ.Domino.toShape_finite (d : Domino) : Set.Finite d.toShape

The shape of a domino is finite

theorem DominoTilingsZ.Domino.eq_of_toShape_eq {d1 d2 : Domino} (h : d1.toShape = d2.toShape) : d1 = d2

Two dominos with the same shape are equal. This follows from the fact that a domino's shape uniquely determines its type and position.

structure DominoTilingsZ.Tiling (S : Shape) : Type

A domino tiling of a shape S is a set partition of S into dominos (Definition \ref{def.domino.shapes-and-tilings}(d))

• dominos : Set Domino

  The set of dominos in the tiling

• pairwise_disjoint : self.dominos.PairwiseDisjoint Domino.toShape

  The dominos are pairwise disjoint

• cover : ⋃ d ∈ self.dominos, d.toShape = S

  The union of dominos equals the shape

theorem DominoTilingsZ.Tiling.ext {S : Shape} (T1 T2 : Tiling S) (h : T1.dominos = T2.dominos) : T1 = T2

Two tilings are equal iff they have the same dominos

theorem DominoTilingsZ.Tiling.ext_iff {S : Shape} {T1 T2 : Tiling S} : T1 = T2 ↔ T1.dominos = T2.dominos

def DominoTilingsZ.Tiling.empty : Tiling ∅

The empty tiling of an empty shape

Equations

• DominoTilingsZ.Tiling.empty = { dominos := ∅, pairwise_disjoint := DominoTilingsZ.Tiling.empty._proof_1, cover := DominoTilingsZ.Tiling.empty._proof_2 }

theorem DominoTilingsZ.Tiling.unique_empty (T : Tiling ∅) : T.dominos = ∅

The empty shape has exactly one tiling (the empty tiling)

def DominoTilingsZ.numTilings (n m : ℕ) : ℕ

The number of domino tilings of the n × m rectangle (Definition \ref{def.domino.shapes-and-tilings}(e))

This is defined as the cardinality of the type of all tilings. Note: For this to be meaningful, the set of tilings must be finite, which holds for any finite rectangle.

Equations

• d_[n,m] = Nat.card (DominoTilingsZ.Tiling (DominoTilingsZ.Rectangle n m))

def DominoTilingsZ.«termD_[_,_]» : Lean.ParserDescr

Equations

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

Height-2 Rectangle Tilings

def DominoTilingsZ.TilingsHeight2 : WeightedSet ((n : ℕ) × Tiling (Rectangle n 2))

Domino tilings of height-2 rectangles, with weight = width of rectangle

Equations

• DominoTilingsZ.TilingsHeight2 = { weight := fun (x : (n : ℕ) × DominoTilingsZ.Tiling (DominoTilingsZ.Rectangle n 2)) => match x with | ⟨n, snd⟩ => n }

theorem DominoTilingsZ.tilingsHeight2_isFiniteType : TilingsHeight2.IsFiniteType

TilingsHeight2 is a finite-type weighted set

def DominoTilingsZ.hasFault (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) : Prop

A fault in a domino tiling is a vertical line that no domino straddles

Equations

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

theorem DominoTilingsZ.hasFault_eq_of_dominos_eq {n : ℕ} {T1 T2 : Tiling (Rectangle n 2)} (h : T1.dominos = T2.dominos) (k : ℕ) : hasFault n T1 k ↔ hasFault n T2 k

hasFault only depends on the dominos set

def DominoTilingsZ.isFaultfree (n : ℕ) (T : Tiling (Rectangle n 2)) : Prop

A tiling is faultfree if it is nonempty and has no fault

Equations

• DominoTilingsZ.isFaultfree n T = (n > 0 ∧ ∀ (k : ℕ), ¬DominoTilingsZ.hasFault n T k)

theorem DominoTilingsZ.isFaultfree_eq_of_dominos_eq {n : ℕ} {T1 T2 : Tiling (Rectangle n 2)} (h : T1.dominos = T2.dominos) : isFaultfree n T1 ↔ isFaultfree n T2

isFaultfree only depends on the dominos set

def DominoTilingsZ.FaultfreeTilingsHeight2 : WeightedSet ((n : ℕ) × { T : Tiling (Rectangle n 2) // isFaultfree n T })

Faultfree tilings of height-2 rectangles

Equations

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

theorem DominoTilingsZ.faultfreeTilingsHeight2_isFiniteType : FaultfreeTilingsHeight2.IsFiniteType

FaultfreeTilingsHeight2 is finite-type

Helper lemmas for faultfree classification

theorem DominoTilingsZ.exists_domino_covering_11 (n : ℕ) (hn : n ≥ 1) (T : Tiling (Rectangle n 2)) : ∃ d ∈ T.dominos, (1, 1) ∈ d.toShape

theorem DominoTilingsZ.domino_covering_11_valid (n : ℕ) (T : Tiling (Rectangle n 2)) (d : Domino) (hd : d ∈ T.dominos) (h : (1, 1) ∈ d.toShape) : d = Domino.vertical 1 1 ∨ d = Domino.horizontal 1 1

theorem DominoTilingsZ.fault_at_1_if_vertical (n : ℕ) (hn : n ≥ 2) (T : Tiling (Rectangle n 2)) (hv : Domino.vertical 1 1 ∈ T.dominos) : hasFault n T 1

theorem DominoTilingsZ.horizontal_12_if_horizontal_11 (n : ℕ) (hn : n ≥ 1) (T : Tiling (Rectangle n 2)) (hh : Domino.horizontal 1 1 ∈ T.dominos) : Domino.horizontal 1 2 ∈ T.dominos

theorem DominoTilingsZ.fault_at_2_if_horizontal (n : ℕ) (hn : n ≥ 3) (T : Tiling (Rectangle n 2)) (hh : Domino.horizontal 1 1 ∈ T.dominos) : hasFault n T 2

theorem DominoTilingsZ.faultfree_height2_classification (n : ℕ) (T : Tiling (Rectangle n 2)) (hff : isFaultfree n T) : n = 1 ∨ n = 2

The only faultfree tilings of height-2 rectangles have width 1 or 2

def DominoTilingsZ.tiling_1_2 : Tiling (Rectangle 1 2)

The unique tiling of the 1×2 rectangle (one vertical domino)

Equations

• DominoTilingsZ.tiling_1_2 = { dominos := {DominoTilingsZ.Domino.vertical 1 1}, pairwise_disjoint := DominoTilingsZ.tiling_1_2._proof_1, cover := DominoTilingsZ.tiling_1_2._proof_2 }

theorem DominoTilingsZ.tiling_1_2_faultfree : isFaultfree 1 tiling_1_2

The 1×2 tiling is faultfree

theorem DominoTilingsZ.tiling_1_2_unique (T : Tiling (Rectangle 1 2)) : T = tiling_1_2

Every tiling of the 1×2 rectangle equals tiling_1_2

def DominoTilingsZ.faultfreeTiling_1_2 : { T : Tiling (Rectangle 1 2) // isFaultfree 1 T }

The faultfree tiling of the 1×2 rectangle as a Subtype element

Equations

• DominoTilingsZ.faultfreeTiling_1_2 = ⟨DominoTilingsZ.tiling_1_2, DominoTilingsZ.tiling_1_2_faultfree⟩

theorem DominoTilingsZ.faultfreeTilingsHeight2_weight1_unique (x : (n : ℕ) × { T : Tiling (Rectangle n 2) // isFaultfree n T }) (hx : FaultfreeTilingsHeight2.weight x = 1) : x = ⟨1, faultfreeTiling_1_2⟩

Every element of FaultfreeTilingsHeight2 with weight 1 equals faultfreeTiling_1_2

theorem DominoTilingsZ.countOfWeight_faultfreeHeight2_one : FaultfreeTilingsHeight2.countOfWeight faultfreeTilingsHeight2_isFiniteType 1 = 1

There is exactly one faultfree tiling of width 1 (one vertical domino)

def DominoTilingsZ.twoHorizontalDominos : Tiling (Rectangle 2 2)

The unique faultfree tiling of width 2: two horizontal dominos

Equations

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

theorem DominoTilingsZ.twoHorizontalDominos_isFaultfree : isFaultfree 2 twoHorizontalDominos

The two horizontal dominos tiling is faultfree

theorem DominoTilingsZ.faultfree_tiling_width2_unique (T : Tiling (Rectangle 2 2)) (hff : isFaultfree 2 T) : T = twoHorizontalDominos

Any faultfree tiling of Rectangle 2 2 equals twoHorizontalDominos

theorem DominoTilingsZ.countOfWeight_faultfreeHeight2_two : FaultfreeTilingsHeight2.countOfWeight faultfreeTilingsHeight2_isFiniteType 2 = 1

There is exactly one faultfree tiling of width 2 (two horizontal dominos)

theorem DominoTilingsZ.countOfWeight_faultfreeHeight2_eq_zero (n : ℕ) (hn1 : n ≠ 1) (hn2 : n ≠ 2) : FaultfreeTilingsHeight2.countOfWeight faultfreeTilingsHeight2_isFiniteType n = 0

For n ≠ 1 and n ≠ 2, there are no faultfree tilings of width n

theorem DominoTilingsZ.weightGenFun_faultfreeHeight2 : FaultfreeTilingsHeight2.weightGenFun faultfreeTilingsHeight2_isFiniteType = PowerSeries.X + PowerSeries.X ^ 2

The generating function of faultfree height-2 tilings is x + x²

Decomposition Lemma (lem.gf.weighted-set.domino.fd)

Helper definitions for tiling composition/decomposition

def DominoTilingsZ.Domino.shift (d : Domino) (offset : ℤ) : Domino

Shift a domino horizontally by an offset

Equations

• (DominoTilingsZ.Domino.horizontal i j).shift offset = DominoTilingsZ.Domino.horizontal (i + offset) j
• (DominoTilingsZ.Domino.vertical i j).shift offset = DominoTilingsZ.Domino.vertical (i + offset) j

theorem DominoTilingsZ.Domino.shift_toShape (d : Domino) (offset : ℤ) : (d.shift offset).toShape = (fun (p : ℤ × ℤ) => (p.1 + offset, p.2)) '' d.toShape

Shifting preserves the shape structure

def DominoTilingsZ.shiftDominos (ds : Set Domino) (offset : ℤ) : Set Domino

Shift a set of dominos

Equations

• DominoTilingsZ.shiftDominos ds offset = (fun (d : DominoTilingsZ.Domino) => d.shift offset) '' ds

theorem DominoTilingsZ.Domino.shift_injective (offset : ℤ) : Function.Injective fun (d : Domino) => d.shift offset

Shifting is injective

@[simp]

theorem DominoTilingsZ.Domino.shift_zero (d : Domino) : d.shift 0 = d

Shifting by 0 is the identity

theorem DominoTilingsZ.Domino.shift_shift (d : Domino) (a b : ℤ) : (d.shift a).shift b = d.shift (a + b)

Shifting twice is the same as shifting by the sum

theorem DominoTilingsZ.Rectangle_shift (n m : ℕ) (offset : ℤ) : (fun (p : ℤ × ℤ) => (p.1 + offset, p.2)) '' Rectangle n m = {p : ℤ × ℤ | 1 + offset ≤ p.1 ∧ p.1 ≤ ↑n + offset ∧ 1 ≤ p.2 ∧ p.2 ≤ ↑m}

Rectangle shift lemma

def DominoTilingsZ.Tiling.shift {n m : ℕ} (T : Tiling (Rectangle n m)) (offset : ℤ) : Tiling {p : ℤ × ℤ | 1 + offset ≤ p.1 ∧ p.1 ≤ ↑n + offset ∧ 1 ≤ p.2 ∧ p.2 ≤ ↑m}

Shift a tiling to a new position

Equations

• T.shift offset = { dominos := DominoTilingsZ.shiftDominos T.dominos offset, pairwise_disjoint := ⋯, cover := ⋯ }

def DominoTilingsZ.emptyTiling2 : Tiling (Rectangle 0 2)

The tiling of the empty rectangle (width 0)

Equations

• DominoTilingsZ.emptyTiling2 = DominoTilingsZ.emptyTiling2._proof_1.mpr DominoTilingsZ.Tiling.empty

def DominoTilingsZ.Tiling.cast {S S' : Shape} (h : S = S') (T : Tiling S) : Tiling S'

Cast a tiling along rectangle equality

Equations

• DominoTilingsZ.Tiling.cast h T = { dominos := T.dominos, pairwise_disjoint := ⋯, cover := ⋯ }

@[simp]

theorem DominoTilingsZ.Tiling.cast_dominos {S S' : Shape} (h : S = S') (T : Tiling S) : (cast h T).dominos = T.dominos

Casting a tiling preserves its dominos

@[simp]

theorem DominoTilingsZ.Tiling.subst_dominos {n m : ℕ} (h : n = m) (T : Tiling (Rectangle n 2)) : (h ▸ T).dominos = T.dominos

Subst (▸) on a tiling preserves dominos

Composition: Concatenating faultfree tilings

def DominoTilingsZ.partialWidthSum (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (i : Fin k) : ℕ

The partial sum of widths up to (but not including) index i

Equations

• DominoTilingsZ.partialWidthSum k ts i = ∑ j : Fin ↑i, (ts ⟨↑j, ⋯⟩).fst

@[simp]

theorem DominoTilingsZ.partialWidthSum_zero (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (i : Fin k) (hi : ↑i = 0) : partialWidthSum k ts i = 0

The partial width sum at index with val = 0 is always 0

def DominoTilingsZ.Domino.shiftNat (d : Domino) (offset : ℕ) : Domino

Shift a domino by a natural number offset (for composition)

Equations

• d.shiftNat offset = d.shift ↑offset

@[simp]

theorem DominoTilingsZ.Domino.shiftNat_zero (d : Domino) : d.shiftNat 0 = d

Shifting by natural 0 is the identity

theorem DominoTilingsZ.Domino.shiftNat_toShape (d : Domino) (offset : ℕ) : (d.shiftNat offset).toShape = (fun (p : ℤ × ℤ) => (p.1 + ↑offset, p.2)) '' d.toShape

Shifting by natural number preserves shape structure

theorem DominoTilingsZ.Domino.shiftNat_shiftNat (d : Domino) (a b : ℕ) : (d.shiftNat a).shiftNat b = d.shiftNat (a + b)

Shifting twice by natural numbers is the same as shifting by the sum

def DominoTilingsZ.composeTilings_component_dominos (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (i : Fin k) : Set Domino

The set of dominos for the i-th component in the composition, shifted appropriately

Equations

• DominoTilingsZ.composeTilings_component_dominos k ts i = (fun (d : DominoTilingsZ.Domino) => d.shiftNat (DominoTilingsZ.partialWidthSum k ts i)) '' (↑(ts i).snd).dominos

def DominoTilingsZ.composeTilings_dominos (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : Set Domino

The union of all shifted dominos for composition

Equations

• DominoTilingsZ.composeTilings_dominos k ts = ⋃ (i : Fin k), DominoTilingsZ.composeTilings_component_dominos k ts i

theorem DominoTilingsZ.composeTilings_component_dominos_disjoint (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (i1 i2 : Fin k) (hi : i1 ≠ i2) (d1 : Domino) (hd1 : d1 ∈ composeTilings_component_dominos k ts i1) (d2 : Domino) (hd2 : d2 ∈ composeTilings_component_dominos k ts i2) : Disjoint d1.toShape d2.toShape

Helper: Dominos from different components have disjoint x-coordinate ranges

def DominoTilingsZ.composeTilings (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : (n : ℕ) × Tiling (Rectangle n 2)

The composition function: given a tuple of faultfree tilings, concatenate them horizontally to produce a single tiling.

Each faultfree tiling is shifted by the cumulative width of the previous tilings, and the union of all shifted dominos forms the composed tiling.

This is the inverse of decomposeTiling.

Equations

• DominoTilingsZ.composeTilings k ts = ⟨∑ i : Fin k, (ts i).fst, { dominos := DominoTilingsZ.composeTilings_dominos k ts, pairwise_disjoint := ⋯, cover := ⋯ }⟩

theorem DominoTilingsZ.composeTilings_dominos_one (ts : Fin 1 → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : composeTilings_dominos 1 ts = (↑(ts 0).snd).dominos

For k = 1, the composed dominos equal the original dominos (shifted by 0)

theorem DominoTilingsZ.composeTilings_one_dominos (ts : Fin 1 → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : (composeTilings 1 ts).snd.dominos = (↑(ts 0).snd).dominos

For k = 1, the composed tiling has the same dominos as the original

theorem DominoTilingsZ.composeTilings_one_width (ts : Fin 1 → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : (composeTilings 1 ts).fst = (ts 0).fst

For k = 1, the width of the composed tiling equals the width of the single component

theorem DominoTilingsZ.composeTilings_one_tiling (ts : Fin 1 → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : (composeTilings 1 ts).snd = ↑(ts 0).snd

For k = 1, the composed tiling equals the single component (as Tilings)

theorem DominoTilingsZ.composeTilings_one_isFaultfree (ts : Fin 1 → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : isFaultfree (composeTilings 1 ts).fst (composeTilings 1 ts).snd

For k = 1, the composed tiling is faultfree

theorem DominoTilingsZ.composeTilings_prepend_width (m first_width : ℕ) (first : { T' : Tiling (Rectangle first_width 2) // isFaultfree first_width T' }) (rest : Fin m → (w : ℕ) × { T' : Tiling (Rectangle w 2) // isFaultfree w T' }) (ts : Fin (m + 1) → (w : ℕ) × { T' : Tiling (Rectangle w 2) // isFaultfree w T' }) (hts : ts = fun (i : Fin (m + 1)) => if hi : ↑i = 0 then ⟨first_width, first⟩ else rest ⟨↑i - 1, ⋯⟩) : (composeTilings (m + 1) ts).fst = first_width + ∑ j : Fin m, (rest j).fst

Helper lemma: The width of composeTilings with a prepended element equals the first width plus the sum of the remaining widths. This is used in proving composeTilings_decomposeTiling.

theorem DominoTilingsZ.composeTilings_prepend_width' (m first_width rest_width : ℕ) (first : { T' : Tiling (Rectangle first_width 2) // isFaultfree first_width T' }) (rest : Fin m → (w : ℕ) × { T' : Tiling (Rectangle w 2) // isFaultfree w T' }) (hrest : (composeTilings m rest).fst = rest_width) (ts : Fin (m + 1) → (w : ℕ) × { T' : Tiling (Rectangle w 2) // isFaultfree w T' }) (hts : ts = fun (i : Fin (m + 1)) => if hi : ↑i = 0 then ⟨first_width, first⟩ else rest ⟨↑i - 1, ⋯⟩) : (composeTilings (m + 1) ts).fst = first_width + rest_width

Helper lemma: When we compose with a prepended element, if the rest composes to a specific width and tiling, then the total width equals first_width + rest_width.

Decomposition: Cutting at faults

Infrastructure for restricting tilings at faults

def DominoTilingsZ.Domino.shiftNeg (d : Domino) (offset : ℕ) : Domino

Shift a domino by a negative offset (for decomposition)

Equations

• d.shiftNeg offset = d.shift (-↑offset)

theorem DominoTilingsZ.Domino.shiftNeg_toShape (d : Domino) (offset : ℕ) : (d.shiftNeg offset).toShape = (fun (p : ℤ × ℤ) => (p.1 - ↑offset, p.2)) '' d.toShape

Shifting by negative offset preserves shape structure

theorem DominoTilingsZ.Domino.shiftNeg_shiftNat (d : Domino) (k : ℕ) : (d.shiftNat k).shiftNeg k = d

Shifting by k then by -k returns the original domino

theorem DominoTilingsZ.Domino.shiftNat_shiftNeg (d : Domino) (k : ℕ) : (d.shiftNeg k).shiftNat k = d

Shifting by -k then by k returns the original domino

def DominoTilingsZ.Domino.inLeftPart (d : Domino) (k : ℕ) : Prop

A domino is in the left part (all x-coordinates ≤ k)

Equations

• d.inLeftPart k = ∀ p ∈ d.toShape, p.1 ≤ ↑k

def DominoTilingsZ.Domino.inRightPart (d : Domino) (k : ℕ) : Prop

A domino is in the right part (all x-coordinates ≥ k+1)

Equations

• d.inRightPart k = ∀ p ∈ d.toShape, p.1 ≥ ↑k + 1

theorem DominoTilingsZ.domino_left_or_right_at_fault {n : ℕ} {T : Tiling (Rectangle n 2)} {k : ℕ} (hk : hasFault n T k) (d : Domino) (hd : d ∈ T.dominos) : d.inLeftPart k ∨ d.inRightPart k

At a fault, each domino is either entirely left or entirely right

def DominoTilingsZ.restrictTilingLeft (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) : Tiling (Rectangle k 2)

Restrict a tiling to the left part at a fault position

Equations

• DominoTilingsZ.restrictTilingLeft n T k hk = { dominos := {d : DominoTilingsZ.Domino | d ∈ T.dominos ∧ d.inLeftPart k}, pairwise_disjoint := ⋯, cover := ⋯ }

def DominoTilingsZ.restrictTilingRight (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) : Tiling (Rectangle (n - k) 2)

Restrict a tiling to the right part at a fault position, shifted to origin

Equations

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

@[simp]

theorem DominoTilingsZ.restrictTilingLeft_proof_irrel (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk1 hk2 : hasFault n T k) : restrictTilingLeft n T k hk1 = restrictTilingLeft n T k hk2

restrictTilingLeft does not depend on the proof of hasFault

@[simp]

theorem DominoTilingsZ.restrictTilingRight_proof_irrel (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk1 hk2 : hasFault n T k) : restrictTilingRight n T k hk1 = restrictTilingRight n T k hk2

restrictTilingRight does not depend on the proof of hasFault

theorem DominoTilingsZ.restrictTilingLeft_isFaultfree (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) (hmin : ∀ j < k, ¬hasFault n T j) : isFaultfree k (restrictTilingLeft n T k hk)

The left restriction at a fault is faultfree if k is the smallest fault

theorem DominoTilingsZ.dominos_eq_leftPart_union_rightPart (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) : T.dominos = {d : Domino | d ∈ T.dominos ∧ d.inLeftPart k} ∪ {d : Domino | d ∈ T.dominos ∧ d.inRightPart k}

At a fault position, the tiling's dominos split into left and right parts

theorem DominoTilingsZ.dominos_eq_left_union_shifted_right (n : ℕ) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) : T.dominos = (restrictTilingLeft n T k hk).dominos ∪ (fun (d : Domino) => d.shiftNat k) '' (restrictTilingRight n T k hk).dominos

The original dominos equal the union of left part and shifted right part

def DominoTilingsZ.faultPositions (n : ℕ) (T : Tiling (Rectangle n 2)) : Set ℕ

The set of fault positions in a tiling

Equations

• DominoTilingsZ.faultPositions n T = {k : ℕ | DominoTilingsZ.hasFault n T k}

theorem DominoTilingsZ.faultPositions_finite (n : ℕ) (T : Tiling (Rectangle n 2)) : (faultPositions n T).Finite

The fault positions form a finite set (bounded by n)

noncomputable def DominoTilingsZ.minFault (n : ℕ) (T : Tiling (Rectangle n 2)) (hne : (faultPositions n T).Nonempty) : ℕ

The minimum fault position in a tiling (when faults exist)

Equations

• DominoTilingsZ.minFault n T hne = ⋯.toFinset.min' ⋯

theorem DominoTilingsZ.minFault_mem (n : ℕ) (T : Tiling (Rectangle n 2)) (hne : (faultPositions n T).Nonempty) : minFault n T hne ∈ faultPositions n T

The minimum fault is indeed a fault

theorem DominoTilingsZ.minFault_hasFault (n : ℕ) (T : Tiling (Rectangle n 2)) (hne : (faultPositions n T).Nonempty) : hasFault n T (minFault n T hne)

The minimum fault is a hasFault

theorem DominoTilingsZ.minFault_le (n : ℕ) (T : Tiling (Rectangle n 2)) (hne : (faultPositions n T).Nonempty) (j : ℕ) (hj : j ∈ faultPositions n T) : minFault n T hne ≤ j

The minimum fault is less than or equal to any other fault

noncomputable instance DominoTilingsZ.faultPositions_nonempty_decidable (n : ℕ) (T : Tiling (Rectangle n 2)) : Decidable (faultPositions n T).Nonempty

Decidability instance for faultPositions.Nonempty

Equations

• DominoTilingsZ.faultPositions_nonempty_decidable n T = ⋯.mp Finset.decidableNonempty

theorem DominoTilingsZ.faultPositions_empty_of_isFaultfree (n : ℕ) (T : Tiling (Rectangle n 2)) (hff : isFaultfree n T) : faultPositions n T = ∅

A faultfree tiling has no faults, so faultPositions is empty

theorem DominoTilingsZ.faultPositions_not_nonempty_of_isFaultfree (n : ℕ) (T : Tiling (Rectangle n 2)) (hff : isFaultfree n T) : ¬(faultPositions n T).Nonempty

A faultfree tiling has non-nonempty faultPositions

Helper lemmas for k >= 2 case of decomposeTiling_composeTilings

theorem DominoTilingsZ.partialWidthSum_one (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : partialWidthSum k ts ⟨1, ⋯⟩ = (ts ⟨0, ⋯⟩).fst

The partial width sum at index 1 equals the width of the first component

theorem DominoTilingsZ.composeTilings_hasFault_at_boundary (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : hasFault (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst

For k >= 2, the composed tiling has a fault at position (ts 0).1

theorem DominoTilingsZ.composeTilings_no_fault_before_boundary (k : ℕ) (hk : k ≥ 1) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (p : ℕ) (hp : p < (ts ⟨0, hk⟩).fst) : ¬hasFault (composeTilings k ts).fst (composeTilings k ts).snd p

For k >= 1, there are no faults at positions less than (ts 0).1 in the composed tiling

theorem DominoTilingsZ.composeTilings_minFault_eq (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (hne : (faultPositions (composeTilings k ts).fst (composeTilings k ts).snd).Nonempty) : minFault (composeTilings k ts).fst (composeTilings k ts).snd hne = (ts ⟨0, ⋯⟩).fst

The minimum fault in a composed tiling with k >= 2 components is at (ts 0).1

Lemmas relating restrictTiling to composeTilings

def DominoTilingsZ.faultfreeTilingsTail (k : ℕ) (hk : k ≥ 1) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : Fin (k - 1) → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }

The tail of a tuple of faultfree tilings

Equations

• DominoTilingsZ.faultfreeTilingsTail k hk ts i = ts ⟨↑i + 1, ⋯⟩

theorem DominoTilingsZ.composeTilings_tail_width (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : (composeTilings (k - 1) (faultfreeTilingsTail k ⋯ ts)).fst = (composeTilings k ts).fst - (ts ⟨0, ⋯⟩).fst

The width of composing the tail equals the total width minus the first component width

theorem DominoTilingsZ.composeTilings_component0_inLeftPart (k : ℕ) (hk : k ≥ 1) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (d : Domino) (hd : d ∈ (↑(ts ⟨0, hk⟩).snd).dominos) : d.inLeftPart (ts ⟨0, hk⟩).fst

Dominos from component 0 are in the left part at position (ts 0).1

theorem DominoTilingsZ.composeTilings_componentPos_inRightPart (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (i : Fin k) (hi : ↑i ≥ 1) (d : Domino) (hd : d ∈ (↑(ts i).snd).dominos) : (d.shiftNat (partialWidthSum k ts i)).inRightPart (ts ⟨0, ⋯⟩).fst

Dominos from component i >= 1 are in the right part at position (ts 0).1

theorem DominoTilingsZ.restrictTilingLeft_composeTilings_dominos (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (hfault : hasFault (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst) : (restrictTilingLeft (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst hfault).dominos = (↑(ts ⟨0, ⋯⟩).snd).dominos

The left restriction of a composed tiling at the first boundary has the same dominos as the first component

theorem DominoTilingsZ.restrictTilingLeft_composeTilings_eq (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (hfault : hasFault (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst) : restrictTilingLeft (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst hfault = ↑(ts ⟨0, ⋯⟩).snd

The left restriction of a composed tiling equals the first component's tiling. This follows from restrictTilingLeft_composeTilings_dominos via Tiling.ext.

theorem DominoTilingsZ.composeTilings_componentPos_dominos_unshift (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (i : Fin k) (hi : ↑i ≥ 1) (d : Domino) (hd : d ∈ (↑(ts i).snd).dominos) : (d.shiftNat (partialWidthSum k ts i)).shiftNeg (ts ⟨0, ⋯⟩).fst = d.shiftNat (partialWidthSum k ts i - (ts ⟨0, ⋯⟩).fst)

Dominos from component i shifted and then unshifted by k gives back the original

theorem DominoTilingsZ.partialWidthSum_tail (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (j : Fin (k - 1)) : partialWidthSum (k - 1) (faultfreeTilingsTail k ⋯ ts) j = partialWidthSum k ts ⟨↑j + 1, ⋯⟩ - (ts ⟨0, ⋯⟩).fst

The partial width sum for the tail equals the original minus (ts 0).1

theorem DominoTilingsZ.restrictTilingRight_composeTilings_dominos (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (hfault : hasFault (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst) : (restrictTilingRight (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst hfault).dominos = (composeTilings (k - 1) (faultfreeTilingsTail k ⋯ ts)).snd.dominos

The right restriction of a composed tiling at the first boundary has the same dominos as the composition of the tail

theorem DominoTilingsZ.restrictTilingRight_composeTilings_dominos_eq (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (hfault : hasFault (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst) : (restrictTilingRight (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst hfault).dominos = (composeTilings (k - 1) (faultfreeTilingsTail k ⋯ ts)).snd.dominos

The right restriction of a composed tiling has the same dominos as the composition of the tail. Note: The tilings have different types (different width parameters), so we state this as a domino equality rather than a tiling equality. Use Tiling.ext with the width equality composeTilings_tail_width to convert to tiling equality when needed.

theorem DominoTilingsZ.restrictTilingRight_composeTilings_eq (k : ℕ) (hk : k ≥ 2) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) (hfault : hasFault (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst) : restrictTilingRight (composeTilings k ts).fst (composeTilings k ts).snd (ts ⟨0, ⋯⟩).fst hfault = ⋯ ▸ (composeTilings (k - 1) (faultfreeTilingsTail k ⋯ ts)).snd

The right restriction of a composed tiling equals the composition of the tail. This combines the width equality composeTilings_tail_width with the domino equality restrictTilingRight_composeTilings_dominos_eq to give a full tiling equality.

Note: The two tilings have the same type because:

• restrictTilingRight has width (composeTilings k ts).1 - (ts 0).1
• composeTilings (k-1) (tail ts) has width (composeTilings k ts).1 - (ts 0).1 (by composeTilings_tail_width)

@[irreducible]

noncomputable def DominoTilingsZ.decomposeTiling (n : ℕ) (T : Tiling (Rectangle n 2)) : (k : ℕ) × (Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' })

The decomposition function: given a tiling of a height-2 rectangle, produce a tuple of faultfree tilings by cutting along all faults.

For example, a tiling with faults at positions k₁ < k₂ < ... < kₘ decomposes into m+1 faultfree tilings of widths k₁, k₂-k₁, ..., n-kₘ.

The empty tiling (n=0) decomposes into the empty tuple (k=0).

Implementation: We recursively find the minimum fault position, cut the tiling there, and decompose the right part. The left part at a minimum fault is always faultfree. If no faults exist, the entire tiling is faultfree and returned as a singleton.

Equations

• One or more equations did not get rendered due to their size.
• DominoTilingsZ.decomposeTiling 0 x_2 = ⟨0, Fin.elim0⟩

theorem DominoTilingsZ.decomposeTiling_hasFault (n : ℕ) (T : Tiling (Rectangle (n + 1) 2)) (hne : (faultPositions (n + 1) T).Nonempty) : let k := minFault (n + 1) T hne; have hk := ⋯; have hk_min := ⋯; let left := restrictTilingLeft (n + 1) T k hk; have left_ff := ⋯; have right := restrictTilingRight (n + 1) T k hk; match decomposeTiling (n + 1 - k) right with | ⟨m, ts⟩ => decomposeTiling (n + 1) T = ⟨m + 1, fun (i : Fin (m + 1)) => if hi : ↑i = 0 then ⟨k, ⟨left, left_ff⟩⟩ else ts ⟨↑i - 1, ⋯⟩⟩

Decomposing a tiling with faults at the minimum fault position. This characterizes the structure of decomposeTiling when faults exist.

theorem DominoTilingsZ.decomposeTiling_hasFault_fst (n : ℕ) (T : Tiling (Rectangle (n + 1) 2)) (hne : (faultPositions (n + 1) T).Nonempty) : let k := minFault (n + 1) T hne; have hk := ⋯; have right := restrictTilingRight (n + 1) T k hk; (decomposeTiling (n + 1) T).fst = (decomposeTiling (n + 1 - k) right).fst + 1

The width of decomposeTiling when faults exist equals m+1 where m is the count from decomposing the right part. This is useful for proving composeTilings_decomposeTiling.

theorem DominoTilingsZ.composeTilings_decomposeTiling (n : ℕ) (T : Tiling (Rectangle n 2)) : match decomposeTiling n T with | ⟨k, ts⟩ => composeTilings k ts = ⟨n, T⟩

Decomposition followed by composition gives back the original tiling

theorem DominoTilingsZ.decomposeTiling_faultfree (n : ℕ) (T : Tiling (Rectangle (n + 1) 2)) (hff : isFaultfree (n + 1) T) : decomposeTiling (n + 1) T = ⟨1, fun (x : Fin 1) => ⟨n + 1, ⟨T, hff⟩⟩⟩

Decomposing a faultfree tiling returns a singleton tuple containing the original tiling. This is a key helper for proving decomposeTiling_composeTilings.

theorem DominoTilingsZ.decomposeTiling_subst {n m : ℕ} (h : n = m) (T : Tiling (Rectangle n 2)) : decomposeTiling n T = decomposeTiling m (h ▸ T)

Decomposition is invariant under type cast (subst). This is key for handling dependent types in the inverse proofs.

theorem DominoTilingsZ.decomposeTiling_eq_of_dominos_eq {n m : ℕ} (h : n = m) (T1 : Tiling (Rectangle n 2)) (T2 : Tiling (Rectangle m 2)) (hdom : T1.dominos = T2.dominos) : decomposeTiling n T1 = decomposeTiling m T2

Decomposition depends only on width and dominos. If two tilings have the same width and dominos, their decompositions are equal.

theorem DominoTilingsZ.restrictTilingLeft_subst {n m : ℕ} (h : n = m) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) : restrictTilingLeft m (h ▸ T) k ⋯ = restrictTilingLeft n T k hk

The left restriction of a subst'd tiling equals the left restriction of the original.

theorem DominoTilingsZ.restrictTilingRight_subst_dominos {n m : ℕ} (h : n = m) (T : Tiling (Rectangle n 2)) (k : ℕ) (hk : hasFault n T k) : (restrictTilingRight m (h ▸ T) k ⋯).dominos = (restrictTilingRight n T k hk).dominos

The right restriction of a subst'd tiling has the same dominos as the original.

theorem DominoTilingsZ.decomposeTiling_composeTilings (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : decomposeTiling (composeTilings k ts).fst (composeTilings k ts).snd = ⟨k, ts⟩

Composition followed by decomposition gives back the original tuple.

This theorem proves that composing faultfree tilings and then decomposing recovers the original tuple of tilings.

The proof handles two cases:

1. If k = 0 (empty tuple), the composed tiling is empty (width 0), and decomposeTiling returns the empty tuple by definition.
2. If k > 0, the composed tiling has positive width, and we need to show that the faults in the composed tiling occur exactly at the partial width sums, so decomposing at those faults recovers the original pieces.

theorem DominoTilingsZ.composeTilings_width (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }) : (composeTilings k ts).fst = ∑ i : Fin k, (ts i).fst

The width of the composed tiling equals the sum of widths of the components. This follows from the definition of composeTilings as horizontal concatenation.

theorem DominoTilingsZ.decomposeTiling_weight_sum (n : ℕ) (T : Tiling (Rectangle n 2)) : match decomposeTiling n T with | ⟨k, ts⟩ => ∑ i : Fin k, (ts i).fst = n

The sum of widths of the faultfree tilings equals the width of the original. This is the key property that makes the decomposition weight-preserving.

def DominoTilingsZ.tiling_decomposition_isomorphism : TilingsHeight2.Isomorphism FaultfreeTilingsHeight2.tuples

Main decomposition isomorphism (Lemma \ref{lem.gf.weighted-set.domino.fd}):

Any domino tiling of a height-2 rectangle can be decomposed uniquely into a tuple of faultfree tilings of (usually smaller) height-2 rectangles, by cutting it along its faults.

This gives an isomorphism of weighted sets: D ≅ F⁰ + F¹ + F² + F³ + ... where D = TilingsHeight2 and F = FaultfreeTilingsHeight2.

The isomorphism preserves weights: the sum of the widths of the faultfree tilings in the tuple equals the width of the original tiling.

Equations

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

theorem DominoTilingsZ.tiling_decomposition (n : ℕ) (T : Tiling (Rectangle n 2)) : ∃ (k : ℕ) (ts : Fin k → (m : ℕ) × { T' : Tiling (Rectangle m 2) // isFaultfree m T' }), ∑ i : Fin k, (ts i).fst = n

Corollary: Any tiling decomposes into a tuple of faultfree tilings with matching total weight

Helper definitions for the Fibonacci recurrence bijection

def DominoTilingsZ.prependVertical (m : ℕ) (T : Tiling (Rectangle m 2)) : Tiling (Rectangle (m + 1) 2)

Prepend a vertical domino to a tiling of Rectangle m 2, giving a tiling of Rectangle (m+1) 2.

The new tiling has dominos = {vertical 1 1} ∪ (T.dominos shifted right by 1). This is the inverse of restricting at fault 1 when a vertical domino is present.

Equations

• DominoTilingsZ.prependVertical m T = { dominos := {DominoTilingsZ.Domino.vertical 1 1} ∪ (fun (d : DominoTilingsZ.Domino) => d.shiftNat 1) '' T.dominos, pairwise_disjoint := ⋯, cover := ⋯ }

theorem DominoTilingsZ.vertical_11_not_in_shiftNat_image (m : ℕ) (T : Tiling (Rectangle m 2)) : Domino.vertical 1 1 ∉ (fun (d : Domino) => d.shiftNat 1) '' T.dominos

The vertical domino is not in the image of shifted dominos from Rectangle m 2.

def DominoTilingsZ.prependHorizontalPair (m : ℕ) (T : Tiling (Rectangle m 2)) : Tiling (Rectangle (m + 2) 2)

Prepend a pair of horizontal dominos to a tiling of Rectangle m 2, giving a tiling of Rectangle (m+2) 2.

The new tiling has dominos = {horizontal 1 1, horizontal 1 2} ∪ (T.dominos shifted right by 2). This is the inverse of restricting at fault 2 when horizontal dominos are present.

Equations

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

theorem DominoTilingsZ.horizontal_11_not_in_shiftNat2_image (m : ℕ) (T : Tiling (Rectangle m 2)) : Domino.horizontal 1 1 ∉ (fun (d : Domino) => d.shiftNat 2) '' T.dominos

The horizontal dominos are not in the image of shifted dominos from Rectangle m 2.

theorem DominoTilingsZ.horizontal_12_not_in_shiftNat2_image (m : ℕ) (T : Tiling (Rectangle m 2)) : Domino.horizontal 1 2 ∉ (fun (d : Domino) => d.shiftNat 2) '' T.dominos

theorem DominoTilingsZ.vertical_11_not_in_shiftNat2_image (m : ℕ) (T : Tiling (Rectangle m 2)) : Domino.vertical 1 1 ∉ (fun (d : Domino) => d.shiftNat 2) '' T.dominos

The vertical domino at (1,1) is not in the image of dominos shifted by 2.

@[simp]

theorem DominoTilingsZ.numTilings_0_2 : d_[0,2] = 1

The empty rectangle has exactly one tiling

@[simp]

theorem DominoTilingsZ.numTilings_1_2 : d_[1,2] = 1

The 1×2 rectangle has exactly one tiling

theorem DominoTilingsZ.numTilings_recurrence (n : ℕ) : d_[n + 2,2] = d_[n,2] + d_[n + 1,2]

The Fibonacci recurrence for tiling counts: d_{n+2,2} = d_{n,2} + d_{n+1,2}.

This follows from the bijection: Tiling (Rectangle (n+2) 2) ≃ Tiling (Rectangle n 2) ⊕ Tiling (Rectangle (n+1) 2)

The bijection classifies tilings based on what covers the first column:

• If a vertical domino covers (1,1)-(1,2): removing it and shifting gives a tiling of Rectangle (n+1) 2
• If horizontal dominos cover (1,1)-(2,1) and (1,2)-(2,2): removing them and shifting gives a tiling of Rectangle n 2

This is a classical result in combinatorics.

theorem DominoTilingsZ.numTilings_2_n (n : ℕ) : d_[n,2] = Nat.fib (n + 1)

The number of domino tilings of a 2×n rectangle equals the (n+1)-th Fibonacci number

theorem DominoTilingsZ.countOfWeight_tilingsHeight2_eq (n : ℕ) : TilingsHeight2.countOfWeight tilingsHeight2_isFiniteType n = d_[n,2]

The count of tilings at weight n equals the number of tilings of R_{n,2}

theorem DominoTilingsZ.weightGenFun_tilingsHeight2 : TilingsHeight2.weightGenFun tilingsHeight2_isFiniteType = PowerSeries.mk fun (n : ℕ) => ↑(Nat.fib (n + 1))

The generating function of height-2 tilings equals 1/(1-x-x²), which is the Fibonacci generating function

Height-3 Rectangle Tilings

def DominoTilingsZ.DominosInRectangle (n m : ℕ) : Set Domino

The set of dominos that fit within a rectangle

Equations

• DominoTilingsZ.DominosInRectangle n m = {d : DominoTilingsZ.Domino | d.toShape ⊆ DominoTilingsZ.Rectangle n m}

theorem DominoTilingsZ.dominosInRectangle_finite (n m : ℕ) : (DominosInRectangle n m).Finite

The set of dominos in a rectangle is finite

theorem DominoTilingsZ.tiling_dominos_subset (n m : ℕ) (T : Tiling (Rectangle n m)) : T.dominos ⊆ DominosInRectangle n m

A tiling's dominos are contained in DominosInRectangle

theorem DominoTilingsZ.tilings_finite (n m : ℕ) : Set.univ.Finite

The set of tilings of a rectangle is finite