Tilings of grids, cylinders and tori up to symmetry

DefinitionCell map of the reflection f#✓fully proved

For natural numbers \(n\) and \(m\), the reflection \(f\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid by \((x, y) \mapsto (-1 - x, y)\), that is, \((x, y) \mapsto (n - 1 - x, y)\) with the first coordinate taken modulo \(n\).

public def cellF (n m : ℕ) (c : ZMod n × ZMod m) : ZMod n × ZMod m :=
  (-1 - c.1, c.2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 17

Used byThe reflection f of grid cells is an involution · Fixed cylinder tilings of the reflection f, n even · Cylinder fixed-tiling count for the reflection \(f\) when \(n\) is odd · Fixed tilings of the \(2 \times 1\) grid under reflection and a design swap · Action of the rectangle group on grid cells · Rectangle-group cell action of the reflection r²f · Rectangle-group cell action of the reflection f · Rectangular-grid tilings fixed by the reflection \(f\), \(n\) even · Rectangular-grid tilings fixed by the reflection \(f\), \(n\) odd · Torus fixed-tiling sum for the reflection \(f\), \(n\) even · Torus fixed-tiling sum for the reflection \(f\), \(n\) odd · The dihedral action on the cells of the square grid · The reflection \(sr_0\) acts on the square grid as \(f\) · Square-grid tilings fixed by the reflection \(f\) for even \(n\) · Square-grid tilings fixed by the reflection \(f\) for odd \(n\) · Square-torus fixed points of the reflection \(f\), even \(n\) · Square-torus fixed points of the reflection \(f\), odd \(n\)

DefinitionCell map of the half-turn r²#✓fully proved

For natural numbers \(n\) and \(m\), the half-turn \(r^2\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid by \((x, y) \mapsto (-1 - x, -1 - y)\), that is, \((x, y) \mapsto (n - 1 - x, m - 1 - y)\) with the coordinates taken modulo \(n\) and \(m\).

public def cellR2 (n m : ℕ) (c : ZMod n × ZMod m) : ZMod n × ZMod m :=
  (-1 - c.1, -1 - c.2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 15

Used byCylinder fixed-tiling count for the half-turn when \(m\) is even · Cylinder fixed-tiling count for the half-turn when \(m\) is odd and \(n\) is even · Cylinder fixed-tiling count for the half-turn when \(m\) and \(n\) are odd · Action of the rectangle group on grid cells · Rectangle-group cell action of the half-turn · Rectangular-grid tilings fixed by the half-turn, \(nm\) even · Rectangular-grid tilings fixed by the half-turn, \(nm\) odd · Half-turn fixed points on the rectangular torus, both sides even · Half-turn fixed points on the rectangular torus, \(n\) even and \(m\) odd · Half-turn fixed points on the rectangular torus, \(n\) odd and \(m\) even · Half-turn fixed points on the rectangular torus, both sides odd · Square-grid tilings fixed by the half-turn for even \(n\) · Square-grid tilings fixed by the half-turn for odd \(n\) · Fixed tilings of the even square torus under a half-turn · Fixed tilings of the odd square torus under a half-turn

DefinitionCell map of the reflection r²f#✓fully proved

For natural numbers \(n\) and \(m\), the reflection \(r^2 f\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid by \((x, y) \mapsto (x, -1 - y)\), that is, \((x, y) \mapsto (x, m - 1 - y)\) with the second coordinate taken modulo \(m\).

public def cellR2F (n m : ℕ) (c : ZMod n × ZMod m) : ZMod n × ZMod m :=
  (c.1, -1 - c.2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 12

Used byCylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is even · Cylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is odd · Action of the rectangle group on grid cells · Rectangle-group cell action of the reflection r²f · Rectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) even · Rectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) odd · Fixed points of \(r^2 f\) on the rectangular torus, \(m\) even · Fixed points of \(r^2 f\) on the rectangular torus, \(m\) odd · Square-grid tilings fixed by the reflection \(r^2 f\) for even \(n\) · Square-grid tilings fixed by the reflection \(r^2f\), odd \(n\) · Fixed tilings of the even square torus under the reflection \(r^2 f\) · Fixed tilings of the odd square torus under the reflection \(r^2 f\)

DefinitionCell map of the quarter-turn r#✓fully proved

For a natural number \(n\), the quarter-turn \(r\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\) of the \(n \times n\) grid by \((x, y) \mapsto (-1 - y, x)\), that is, \((x, y) \mapsto (n - 1 - y, x)\) modulo \(n\).

public def cellR (n : ℕ) (c : ZMod n × ZMod n) : ZMod n × ZMod n :=
  (-1 - c.2, c.1)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 6

Used byThe dihedral action on the cells of the square grid · The rotation \(r\) acts on the square grid as the quarter-turn · Square-grid tilings fixed by the quarter-turn for even \(n\) · Square-grid tilings fixed by the quarter-turn for odd \(n\) · Square-torus fixed points of the rotation \(r\), even \(n\) · Fixed tilings of the odd square torus under a quarter-turn

DefinitionCell map of the three-quarter turn r³#✓fully proved

For a natural number \(n\), the three-quarter turn \(r^3\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\) of the \(n \times n\) grid by \((x, y) \mapsto (y, -1 - x)\), that is, \((x, y) \mapsto (y, n - 1 - x)\) modulo \(n\).

public def cellR3 (n : ℕ) (c : ZMod n × ZMod n) : ZMod n × ZMod n :=
  (c.2, -1 - c.1)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 4

Used bySquare-grid tilings fixed by the rotation \(r^3\), even \(n\) · Square-grid tilings fixed by the rotation \(r^3\), odd \(n\) · Fixed tilings of the even square torus under a three-quarter turn · Fixed tilings of the odd square torus under a three-quarter turn

DefinitionCell map of the diagonal reflection rf#✓fully proved

For a natural number \(n\), the diagonal reflection \(rf\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\) of the \(n \times n\) grid by \((x, y) \mapsto (y, x)\).

public def cellRF (n : ℕ) (c : ZMod n × ZMod n) : ZMod n × ZMod n :=
  (c.2, c.1)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 2

Used bySquare-grid tilings fixed by the diagonal reflection \(rf\) · Fixed tilings of the square torus under the diagonal reflection

DefinitionCell map of the antidiagonal reflection r³f#✓fully proved

For a natural number \(n\), the antidiagonal reflection \(r^3 f\) acts on the cells \((x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\) of the \(n \times n\) grid by \((x, y) \mapsto (-1 - y, -1 - x)\), that is, \((x, y) \mapsto (n - 1 - y, n - 1 - x)\) modulo \(n\).

public def cellR3F (n : ℕ) (c : ZMod n × ZMod n) : ZMod n × ZMod n :=
  (-1 - c.2, -1 - c.1)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 2

Used bySquare-grid tilings fixed by the diagonal reflection \(r^3f\) · Fixed tilings of the square torus under the anti-diagonal reflection

DefinitionNumber of fixed tilings#✓fully proved

Let \(\alpha\) (the cells) and \(T\) (the tile designs) be finite sets, let \(\varphi : \alpha \to \alpha\) be a map and let \(\sigma\) be a permutation of \(T\). The number of tilings fixed by \((\varphi, \sigma)\) is the number of maps \(F : \alpha \to T\) such that \(F(\varphi(c)) = \sigma(F(c))\) for every \(c \in \alpha\).

This is the paper's fixed-point condition \(F(c \cdot s) = F(c) \cdot g\), with \(\varphi\) encoding the action on cells and \(\sigma\) the action on designs. No ambient group action is assumed, since each fixed-point formula involves a single symmetry.

public def fixedTilingCount {α T : Type*} [Fintype α] [DecidableEq α]
    [Fintype T] [DecidableEq T] (φ : α → α) (σ : Equiv.Perm T) : ℕ :=
  Fintype.card {F : α → T // ∀ c, F (φ c) = σ (F c)}

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 25

Used byCylinder shift sum · Fixed tilings of the \(2 \times 1\) grid under reflection and a design swap · Fixed tilings as a product over orbits · Fixed tilings of two cells under the identity · Rectangular-grid tilings fixed by the reflection \(f\), \(n\) even · Rectangular-grid tilings fixed by the reflection \(f\), \(n\) odd · Rectangular-grid tilings fixed by the identity · Rectangular-grid tilings fixed by the half-turn, \(nm\) even · Rectangular-grid tilings fixed by the half-turn, \(nm\) odd · Rectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) even · Rectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) odd · Square-grid tilings fixed by the reflection \(f\) for even \(n\) · Square-grid tilings fixed by the reflection \(f\) for odd \(n\) · Square-grid tilings fixed by the identity · Square-grid tilings fixed by the quarter-turn for even \(n\) · Square-grid tilings fixed by the quarter-turn for odd \(n\) · Square-grid tilings fixed by the half-turn for even \(n\) · Square-grid tilings fixed by the half-turn for odd \(n\) · Square-grid tilings fixed by the reflection \(r^2 f\) for even \(n\) · Square-grid tilings fixed by the reflection \(r^2f\), odd \(n\) · Square-grid tilings fixed by the rotation \(r^3\), even \(n\) · Square-grid tilings fixed by the rotation \(r^3\), odd \(n\) · Square-grid tilings fixed by the diagonal reflection \(r^3f\) · Square-grid tilings fixed by the diagonal reflection \(rf\) · Torus shift sum

DefinitionTile designs fixed by a power of a permutation#✓fully proved

For a finite set \(T\) of tile designs, a permutation \(\sigma\) of \(T\) and a natural number \(k\), this is the number of designs \(d \in T\) with \(\sigma^k(d) = d\).

When \(\sigma\) is the action of a symmetry \(g\) on tile designs, this is the paper's \(t_{g^k}\); for \(k = 0\) it is \(t_{\mathrm{id}} = |T|\).

public def tileFixedCount {T : Type*} [Fintype T] [DecidableEq T]
    (σ : Equiv.Perm T) (k : ℕ) : ℕ :=
  Fintype.card {d : T // (σ ^ k) d = d}

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Used by 36

Used byFixed cylinder tilings of the reflection f, n even · Cylinder fixed-tiling count for the reflection \(f\) when \(n\) is odd · Cylinder fixed-tiling count for the half-turn when \(m\) is odd and \(n\) is even · Cylinder fixed-tiling count for the half-turn when \(m\) and \(n\) are odd · Cylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is odd · Fixed tilings as a product over orbits · Rectangular-grid tilings fixed by the reflection \(f\), \(n\) odd · Rectangular-grid tilings fixed by the half-turn, \(nm\) odd · Rectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) odd · Torus fixed-tiling sum for the reflection \(f\), \(n\) even · Torus fixed-tiling sum for the reflection \(f\), \(n\) odd · Half-turn fixed points on the rectangular torus, both sides even · Half-turn fixed points on the rectangular torus, \(n\) even and \(m\) odd · Half-turn fixed points on the rectangular torus, \(n\) odd and \(m\) even · Half-turn fixed points on the rectangular torus, both sides odd · Fixed points of \(r^2 f\) on the rectangular torus, \(m\) even · Fixed points of \(r^2 f\) on the rectangular torus, \(m\) odd · Square-grid tilings fixed by the reflection \(f\) for odd \(n\) · Square-grid tilings fixed by the quarter-turn for odd \(n\) · Square-grid tilings fixed by the half-turn for odd \(n\) · Square-grid tilings fixed by the reflection \(r^2f\), odd \(n\) · Square-grid tilings fixed by the rotation \(r^3\), odd \(n\) · Square-grid tilings fixed by the diagonal reflection \(r^3f\) · Square-grid tilings fixed by the diagonal reflection \(rf\) · Square-torus fixed points of the reflection \(f\), even \(n\) · Square-torus fixed points of the reflection \(f\), odd \(n\) · Square-torus fixed points of the rotation \(r\), even \(n\) · Fixed tilings of the odd square torus under a quarter-turn · Fixed tilings of the even square torus under a half-turn · Fixed tilings of the odd square torus under a half-turn · Fixed tilings of the even square torus under the reflection \(r^2 f\) · Fixed tilings of the odd square torus under the reflection \(r^2 f\) · Fixed tilings of the even square torus under a three-quarter turn · Fixed tilings of the odd square torus under a three-quarter turn · Fixed tilings of the square torus under the anti-diagonal reflection · Fixed tilings of the square torus under the diagonal reflection

DefinitionOrbit of a cell under a permutation#✓fully proved

Let \(\alpha\) be a finite set, \(\varphi\) a permutation of \(\alpha\) and \(c \in \alpha\). The orbit of \(c\) under \(\varphi\) is the finite set \(\{\varphi^k(c) : k \in \mathbb{N}\}\) of images of \(c\) under the nonnegative powers of \(\varphi\). Since \(\alpha\) is finite, this is the orbit of \(c\) under the cyclic group generated by \(\varphi\).

A fixed point \(c\) of \(\varphi\) has the singleton orbit \(\{c\}\); these one-cycles are kept.

public noncomputable def permOrbit {α : Type*} [Fintype α] [DecidableEq α]
    (φ : Equiv.Perm α) (c : α) : Finset α := by
  classical
  exact Finset.univ.filter fun d => ∃ k : ℕ, (φ ^ k) c = d

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 20.

Used by 1

Used byOrbits of a permutation

DefinitionOrbits of a permutation#✓fully proved

Let \(\alpha\) be a finite set and \(\varphi\) a permutation of \(\alpha\). For \(c \in \alpha\) let \(O(c) = \{\varphi^k(c) : k \in \mathbb{N}\}\) be the orbit of \(c\) under \(\varphi\). The set of orbits of \(\varphi\) is the set \(\{O(c) : c \in \alpha\}\) of subsets of \(\alpha\), in which each orbit occurs once.

Fixed points of \(\varphi\) contribute singleton orbits, which the paper's Theorem 20 needs.

public noncomputable def permOrbits {α : Type*} [Fintype α] [DecidableEq α]
    (φ : Equiv.Perm α) : Finset (Finset α) := by
  classical
  exact Finset.univ.image (permOrbit φ)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 20.

Uses 1 · Used by 1

Statement usesOrbit of a cell under a permutation

Used byFixed tilings as a product over orbits

DefinitionCylinder shift sum#✓fully proved

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\), let \(g\) be a map from the cells \(\mathbb{Z}/n \times \mathbb{Z}/m\) to themselves, and let \(\sigma\) be a permutation of \(T\). The cylinder shift sum of \(g\) and \(\sigma\) is the sum, over all shifts \(a \in \mathbb{Z}/n\), of the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(g(x + a, y)) = \sigma(F(x, y))\) for every cell \((x, y)\).

The shift is applied before \(g\), following the paper's right-action convention, and \(\sigma\) is the action of \(g\) on tile designs.

public noncomputable def cylinderShiftSum {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m]
    (cellG : ZMod n × ZMod m → ZMod n × ZMod m) (σ : Equiv.Perm T) : ℕ :=
  ∑ a : ZMod n,
    fixedTilingCount (fun c => cellG (c.1 + a, c.2)) σ

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Uses 1 · Used by 9

Statement usesNumber of fixed tilings

Used byBurnside count of cylinder tilings under rectangle symmetries · Fixed cylinder tilings of the reflection f, n even · Cylinder fixed-tiling count for the reflection \(f\) when \(n\) is odd · Cylinder fixed-tiling count for the identity · Cylinder fixed-tiling count for the half-turn when \(m\) is even · Cylinder fixed-tiling count for the half-turn when \(m\) is odd and \(n\) is even · Cylinder fixed-tiling count for the half-turn when \(m\) and \(n\) are odd · Cylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is even · Cylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is odd

DefinitionTorus shift sum#✓fully proved

Let \(n, m \ge 1\), let \(T\) be a finite set of tile designs, let \(g\) be a map from \(\mathbb{Z}/n \times \mathbb{Z}/m\) (the cells of the \(n \times m\) torus) to itself and let \(\sigma\) be a permutation of \(T\). For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the tilings \(F \colon \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(g(x + a, y + b)) = \sigma(F(x, y))\) for every cell \((x, y)\). The torus shift sum is the sum of these counts over all \(nm\) shifts \((a, b)\).

Shifting the cell first and applying \(g\) afterwards follows the right-action convention of the source; shifts act trivially on tile designs.

public noncomputable def torusShiftSum {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m]
    (cellG : ZMod n × ZMod m → ZMod n × ZMod m) (σ : Equiv.Perm T) : ℕ :=
  ∑ a : ZMod n, ∑ b : ZMod m,
    fixedTilingCount (fun c => cellG (c.1 + a, c.2 + b)) σ

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Uses 1 · Used by 24

Statement usesNumber of fixed tilings

Used byBurnside count of torus tilings under the rectangle group · Torus fixed-tiling sum for the reflection \(f\), \(n\) even · Torus fixed-tiling sum for the reflection \(f\), \(n\) odd · Torus fixed-tiling sum for the identity · Half-turn fixed points on the rectangular torus, both sides even · Half-turn fixed points on the rectangular torus, \(n\) even and \(m\) odd · Half-turn fixed points on the rectangular torus, \(n\) odd and \(m\) even · Half-turn fixed points on the rectangular torus, both sides odd · Fixed points of \(r^2 f\) on the rectangular torus, \(m\) even · Fixed points of \(r^2 f\) on the rectangular torus, \(m\) odd · Burnside count of tilings of the square torus · Square-torus fixed points of the reflection \(f\), even \(n\) · Square-torus fixed points of the reflection \(f\), odd \(n\) · Square-torus fixed points of the identity · Square-torus fixed points of the rotation \(r\), even \(n\) · Fixed tilings of the odd square torus under a quarter-turn · Fixed tilings of the even square torus under a half-turn · Fixed tilings of the odd square torus under a half-turn · Fixed tilings of the even square torus under the reflection \(r^2 f\) · Fixed tilings of the odd square torus under the reflection \(r^2 f\) · Fixed tilings of the even square torus under a three-quarter turn · Fixed tilings of the odd square torus under a three-quarter turn · Fixed tilings of the square torus under the anti-diagonal reflection · Fixed tilings of the square torus under the diagonal reflection

TheoremThe reflection f of grid cells is an involution#✓fully proved

For all natural numbers \(n\) and \(m\) and every cell \(c = (x, y) \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\), applying the cell map \((x, y) \mapsto (-1 - x, y)\) of the reflection \(f\) twice returns \(c\).

public theorem cellF_involutive (n m : ℕ) (c : ZMod n × ZMod m) :
    cellF n m (cellF n m c) = c

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Setting.

Uses 1

Statement usesCell map of the reflection f

TheoremFixed tilings of two cells under the identity#✓fully proved

Let the set of cells and the set of tile designs both be the two-element set \(\{0, 1\}\). The number of maps \(F : \{0, 1\} \to \{0, 1\}\) with \(F(\varphi(c)) = \sigma(F(c))\) for every cell \(c\), where \(\varphi\) is the identity map on cells and \(\sigma\) is the identity permutation of designs, equals \(4\); that is, all \(2^2\) tilings are fixed.

This is a sanity check of the definition of fixed tilings, not one of the paper's enumerative theorems.

public theorem fixedTilingCount_fin_two_identity :
    fixedTilingCount (α := Fin 2) (T := Fin 2) id 1 = 4

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Encoding check.

Uses 1

Statement usesNumber of fixed tilings

TheoremFixed tilings of the \(2 \times 1\) grid under reflection and a design swap#✓fully proved

On the grid \(\mathbb{Z}/2 \times \mathbb{Z}/1\) with two tile designs, exactly two tilings \(F\) satisfy \(F(f(c)) = \sigma(F(c))\) for every cell \(c\), where \(f : (x, y) \mapsto (-1 - x, y)\) is the reflection exchanging the two cells and \(\sigma\) swaps the two designs.

This is a check of the encoding, verified by computation.

public theorem fixedTilingCount_cellF_two_one_swap :
    fixedTilingCount (cellF 2 1) (Equiv.swap (0 : Fin 2) 1) = 2

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Encoding check.

Uses 2

Statement usesCell map of the reflection f · Number of fixed tilings

TheoremFixed tilings as a product over orbits#●ready to prove

Let \(\alpha\) be a finite set of cells, \(T\) a finite set of tile designs, \(\varphi\) a permutation of \(\alpha\) and \(\sigma\) a permutation of \(T\). The number of tilings \(F : \alpha \to T\) with \(F(\varphi(c)) = \sigma(F(c))\) for every cell \(c\) equals \(\prod_{\theta} t(|\theta|)\), where \(\theta\) runs over the orbits of \(\varphi\) on \(\alpha\), fixed cells included as orbits of size one, and \(t(k)\) is the number of designs fixed by \(\sigma^k\).

No order hypothesis on \(\sigma\) is needed.

public theorem_wanted fixedTilingCount_eq_orbit_product {α T : Type*}
    [Fintype α] [DecidableEq α] [Fintype T] [DecidableEq T]
    (φ : Equiv.Perm α) (σ : Equiv.Perm T) :
    fixedTilingCount φ σ =
      ∏ θ ∈ permOrbits φ, tileFixedCount σ θ.card

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 20.

Uses 3

Statement usesNumber of fixed tilings · Orbits of a permutation · Tile designs fixed by a power of a permutation

TheoremRectangular-grid tilings fixed by the identity#●ready to prove

Let \(n\) and \(m\) be positive integers, let \(T\) be a finite set of tiles and let \(\sigma\) be a permutation of \(T\) with \(\sigma^1 = 1\), that is, the identity. Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(c) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{nm}\).

The Burnside conclusion of Theorem 22 is not part of this single-element fixed-point statement.

public theorem_wanted rectangularGrid_identity {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 1 = 1) :
    fixedTilingCount (id : ZMod n × ZMod m → ZMod n × ZMod m) σ =
      Fintype.card T ^ (n * m)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 1

Statement usesNumber of fixed tilings

TheoremRectangular-grid tilings fixed by the half-turn, \(nm\) even#●ready to prove

Let \(n\) and \(m\) be positive integers with \(nm\) even, let \(T\) be a finite set of tiles and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2\) be the half-turn of \(\mathbb{Z}/n \times \mathbb{Z}/m\) given by \(r^2(x, y) = (-1 - x, -1 - y)\). Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(r^2(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{nm/2}\).

public theorem_wanted rectangularGrid_r2_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (heven : Even (n * m)) :
    fixedTilingCount (cellR2 n m) σ = Fintype.card T ^ (n * m / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 2

Statement usesCell map of the half-turn r² · Number of fixed tilings

TheoremRectangular-grid tilings fixed by the half-turn, \(nm\) odd#●ready to prove

Let \(n\) and \(m\) be positive integers with \(nm\) odd, let \(T\) be a finite set of tiles, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and let \(t\) be the number of tiles \(d \in T\) with \(\sigma(d) = d\). Let \(r^2\) be the half-turn of \(\mathbb{Z}/n \times \mathbb{Z}/m\) given by \(r^2(x, y) = (-1 - x, -1 - y)\). Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(r^2(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{(nm-1)/2} \, t\).

public theorem_wanted rectangularGrid_r2_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hodd : Odd (n * m)) :
    fixedTilingCount (cellR2 n m) σ =
      Fintype.card T ^ ((n * m - 1) / 2) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 3

Statement usesCell map of the half-turn r² · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremRectangular-grid tilings fixed by the reflection \(f\), \(n\) even#●ready to prove

Let \(n\) and \(m\) be positive integers with \(n\) even, let \(T\) be a finite set of tiles and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(f\) be the reflection of \(\mathbb{Z}/n \times \mathbb{Z}/m\) given by \(f(x, y) = (-1 - x, y)\). Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(f(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{nm/2}\).

public theorem_wanted rectangularGrid_f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (heven : Even n) :
    fixedTilingCount (cellF n m) σ = Fintype.card T ^ (n * m / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 2

Statement usesCell map of the reflection f · Number of fixed tilings

TheoremRectangular-grid tilings fixed by the reflection \(f\), \(n\) odd#●ready to prove

Let \(n\) and \(m\) be positive integers with \(n\) odd, let \(T\) be a finite set of tiles, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and let \(t\) be the number of tiles \(d \in T\) with \(\sigma(d) = d\). Let \(f\) be the reflection of \(\mathbb{Z}/n \times \mathbb{Z}/m\) given by \(f(x, y) = (-1 - x, y)\). Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(f(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{m(n-1)/2} \, t^m\).

public theorem_wanted rectangularGrid_f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hodd : Odd n) :
    fixedTilingCount (cellF n m) σ =
      Fintype.card T ^ (m * (n - 1) / 2) * tileFixedCount σ 1 ^ m

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 3

Statement usesCell map of the reflection f · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremRectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) even#●ready to prove

Let \(n\) and \(m\) be positive integers with \(m\) even, let \(T\) be a finite set of tiles and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(g\) be the reflection \(r^2 f\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\), given by \(g(x, y) = (x, -1 - y)\). Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(g(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{nm/2}\).

public theorem_wanted rectangularGrid_r2f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (heven : Even m) :
    fixedTilingCount (cellR2F n m) σ = Fintype.card T ^ (n * m / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 2

Statement usesCell map of the reflection r²f · Number of fixed tilings

TheoremRectangular-grid tilings fixed by the reflection \(r^2 f\), \(m\) odd#●ready to prove

Let \(n\) and \(m\) be positive integers with \(m\) odd, let \(T\) be a finite set of tiles, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and let \(t\) be the number of tiles \(d \in T\) with \(\sigma(d) = d\). Let \(g\) be the reflection \(r^2 f\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\), given by \(g(x, y) = (x, -1 - y)\). Then the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(g(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{n(m-1)/2} \, t^n\).

public theorem_wanted rectangularGrid_r2f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hodd : Odd m) :
    fixedTilingCount (cellR2F n m) σ =
      Fintype.card T ^ (n * (m - 1) / 2) * tileFixedCount σ 1 ^ n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 22.

Uses 3

Statement usesCell map of the reflection r²f · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the identity#●ready to prove

Let \(n\) be a positive integer, let \(T\) be a finite set and let \(\sigma\) be a permutation of \(T\) with \(\sigma^1 = 1\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(c) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{n^2}\).

public theorem_wanted squareGrid_identity {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 1 = 1) :
    fixedTilingCount (id : ZMod n × ZMod n → ZMod n × ZMod n) σ =
      Fintype.card T ^ (n ^ 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 1

Statement usesNumber of fixed tilings

TheoremSquare-grid tilings fixed by the half-turn for even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2\) be the half-turn of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(r^2(x, y) = (-1 - x, -1 - y)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^2(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{n^2/2}\).

public theorem_wanted squareGrid_r2_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (heven : Even n) :
    fixedTilingCount (cellR2 n n) σ = Fintype.card T ^ (n ^ 2 / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 2

Statement usesCell map of the half-turn r² · Number of fixed tilings

TheoremSquare-grid tilings fixed by the half-turn for odd \(n\)#●ready to prove

Let \(n\) be an odd positive integer, let \(T\) be a finite set, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and write \(t_\sigma\) for the number of elements \(t \in T\) with \(\sigma(t) = t\). Let \(r^2\) be the half-turn of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(r^2(x, y) = (-1 - x, -1 - y)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^2(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{(n^2 - 1)/2} \cdot t_\sigma\).

public theorem_wanted squareGrid_r2_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hodd : Odd n) :
    fixedTilingCount (cellR2 n n) σ =
      Fintype.card T ^ ((n ^ 2 - 1) / 2) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the half-turn r² · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the reflection \(f\) for even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(f\) be the reflection of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(f(x, y) = (-1 - x, y)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(f(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{n^2/2}\).

public theorem_wanted squareGrid_f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (heven : Even n) :
    fixedTilingCount (cellF n n) σ = Fintype.card T ^ (n ^ 2 / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 2

Statement usesCell map of the reflection f · Number of fixed tilings

TheoremSquare-grid tilings fixed by the reflection \(f\) for odd \(n\)#●ready to prove

Let \(n\) be an odd positive integer, let \(T\) be a finite set, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and write \(t_\sigma\) for the number of elements \(t \in T\) with \(\sigma(t) = t\). Let \(f\) be the reflection of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(f(x, y) = (-1 - x, y)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(f(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{(n^2 - n)/2} \cdot t_\sigma^{\,n}\).

public theorem_wanted squareGrid_f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hodd : Odd n) :
    fixedTilingCount (cellF n n) σ =
      Fintype.card T ^ ((n ^ 2 - n) / 2) * tileFixedCount σ 1 ^ n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the reflection f · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the reflection \(r^2 f\) for even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2 f\) be the reflection of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \((r^2 f)(x, y) = (x, -1 - y)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F((r^2 f)(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{n^2/2}\).

public theorem_wanted squareGrid_r2f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (heven : Even n) :
    fixedTilingCount (cellR2F n n) σ = Fintype.card T ^ (n ^ 2 / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 2

Statement usesCell map of the reflection r²f · Number of fixed tilings

TheoremSquare-grid tilings fixed by the reflection \(r^2f\), odd \(n\)#●ready to prove

Let \(n\) be an odd positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2f\) be the cell map \((x, y) \mapsto (x, -1-y)\) of the \(n \times n\) grid \((\mathbb{Z}/n\mathbb{Z})^2\). Then the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^2f(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{(n^2-n)/2} \, t^n\), where \(t\) is the number of designs in \(T\) fixed by \(\sigma\).

public theorem_wanted squareGrid_r2f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hodd : Odd n) :
    fixedTilingCount (cellR2F n n) σ =
      Fintype.card T ^ ((n ^ 2 - n) / 2) * tileFixedCount σ 1 ^ n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the reflection r²f · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the quarter-turn for even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set and let \(\sigma\) be a permutation of \(T\) with \(\sigma^4 = 1\). Let \(r\) be the quarter-turn of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(r(x, y) = (-1 - y, x)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{n^2/4}\).

public theorem_wanted squareGrid_r_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (heven : Even n) :
    fixedTilingCount (cellR n) σ = Fintype.card T ^ (n ^ 2 / 4)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 2

Statement usesCell map of the quarter-turn r · Number of fixed tilings

TheoremSquare-grid tilings fixed by the quarter-turn for odd \(n\)#●ready to prove

Let \(n\) be an odd positive integer, let \(T\) be a finite set, let \(\sigma\) be a permutation of \(T\) with \(\sigma^4 = 1\), and write \(t_\sigma\) for the number of elements \(t \in T\) with \(\sigma(t) = t\). Let \(r\) be the quarter-turn of the grid \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(r(x, y) = (-1 - y, x)\). Then the number of maps \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r(c)) = \sigma(F(c))\) for every cell \(c\) is \(|T|^{(n^2 - 1)/4} \cdot t_\sigma\).

public theorem_wanted squareGrid_r_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (hodd : Odd n) :
    fixedTilingCount (cellR n) σ =
      Fintype.card T ^ ((n ^ 2 - 1) / 4) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the quarter-turn r · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the rotation \(r^3\), even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^4 = 1\). Let \(r^3\) be the cell map \((x, y) \mapsto (y, -1-x)\) of the \(n \times n\) grid \((\mathbb{Z}/n\mathbb{Z})^2\). Then the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^3(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{n^2/4}\).

public theorem_wanted squareGrid_r3_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (heven : Even n) :
    fixedTilingCount (cellR3 n) σ = Fintype.card T ^ (n ^ 2 / 4)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 2

Statement usesCell map of the three-quarter turn r³ · Number of fixed tilings

TheoremSquare-grid tilings fixed by the rotation \(r^3\), odd \(n\)#●ready to prove

Let \(n\) be an odd positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^4 = 1\). Let \(r^3\) be the cell map \((x, y) \mapsto (y, -1-x)\) of the \(n \times n\) grid \((\mathbb{Z}/n\mathbb{Z})^2\). Then the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^3(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{(n^2-1)/4} \, t\), where \(t\) is the number of designs in \(T\) fixed by \(\sigma\).

public theorem_wanted squareGrid_r3_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (hodd : Odd n) :
    fixedTilingCount (cellR3 n) σ =
      Fintype.card T ^ ((n ^ 2 - 1) / 4) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the three-quarter turn r³ · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the diagonal reflection \(rf\)#●ready to prove

Let \(n\) be a positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(rf\) be the cell map \((x, y) \mapsto (y, x)\) of the \(n \times n\) grid \((\mathbb{Z}/n\mathbb{Z})^2\). Then the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(rf(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{(n^2-n)/2} \, t^n\), where \(t\) is the number of designs in \(T\) fixed by \(\sigma\).

public theorem_wanted squareGrid_rf {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) :
    fixedTilingCount (cellRF n) σ =
      Fintype.card T ^ ((n ^ 2 - n) / 2) * tileFixedCount σ 1 ^ n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the diagonal reflection rf · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSquare-grid tilings fixed by the diagonal reflection \(r^3f\)#●ready to prove

Let \(n\) be a positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^3f\) be the cell map \((x, y) \mapsto (-1-y, -1-x)\) of the \(n \times n\) grid \((\mathbb{Z}/n\mathbb{Z})^2\). Then the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^3f(c)) = \sigma(F(c))\) for every cell \(c\) equals \(|T|^{(n^2-n)/2} \, t^n\), where \(t\) is the number of designs in \(T\) fixed by \(\sigma\).

public theorem_wanted squareGrid_r3f {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) :
    fixedTilingCount (cellR3F n) σ =
      Fintype.card T ^ ((n ^ 2 - n) / 2) * tileFixedCount σ 1 ^ n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 24.

Uses 3

Statement usesCell map of the antidiagonal reflection r³f · Number of fixed tilings · Tile designs fixed by a power of a permutation

TheoremSolution of \(x = -1-x-a\) modulo odd \(n\)#●ready to prove

Let \(n\) be a positive odd integer and \(a \in \mathbb{Z}/n\). Then the set of \(x \in \mathbb{Z}/n\) with \(x = -1-x-a\) is the singleton \(\{k(-1-a)\}\), where \(k\) is the residue mod \(n\) of the integer \((n+1)/2\).

public theorem_wanted reflection_shift_solutions_odd (n : ℕ) [NeZero n]
    (a : ZMod n) (hn : Odd n) :
    {x : ZMod n | x = -1 - x - a} =
      {(((n + 1) / 2 : ℕ) : ZMod n) * (-1 - a)}

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Lemma 25.

TheoremSolutions of \(x = -1-x-a\) modulo even \(n\) for odd \(a\)#●ready to prove

Let \(n\) be a positive even integer and \(a \in \mathbb{Z}/n\) whose representative \(\bar a \in \{0, \dots, n-1\}\) is odd. Then the set of \(x \in \mathbb{Z}/n\) with \(x = -1-x-a\) consists of the residues mod \(n\) of the integers \((-1-\bar a)/2\) and \((n-1-\bar a)/2\).

The divisions by \(2\) are exact divisions of integers, carried out before reducing mod \(n\).

public theorem_wanted reflection_shift_solutions_even_odd (n : ℕ) [NeZero n]
    (a : ZMod n) (hn : Even n) (ha : Odd a.val) :
    {x : ZMod n | x = -1 - x - a} =
      {((((-1 : ℤ) - a.val) / 2 : ℤ) : ZMod n),
        ((((n : ℤ) - 1 - a.val) / 2 : ℤ) : ZMod n)}

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Lemma 25.

TheoremNo solutions of \(x = -1-x-a\) modulo \(n\) when \(n\) and \(a\) are even#●ready to prove

Let \(n\) be a positive even integer and \(a \in \mathbb{Z}/n\) whose representative in \(\{0, \dots, n-1\}\) is even. Then no \(x \in \mathbb{Z}/n\) satisfies \(x = -1-x-a\).

public theorem_wanted reflection_shift_solutions_even_even (n : ℕ) [NeZero n]
    (a : ZMod n) (hn : Even n) (ha : Even a.val) :
    {x : ZMod n | x = -1 - x - a} = ∅

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Lemma 25.

TheoremCylinder fixed-tiling count for the identity#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\), and let \(\sigma\) be a permutation of \(T\) with \(\sigma^1 = 1\), that is, the identity. Then the cylinder shift sum of the identity map of \(\mathbb{Z}/n \times \mathbb{Z}/m\) and \(\sigma\) equals \(\sum_{d \mid n} \varphi(d)\, |T|^{nm/d}\), where \(d\) runs over the positive divisors of \(n\) and \(\varphi\) is Euler's totient function.

public theorem_wanted cylinder_identity {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 1 = 1) :
    cylinderShiftSum n m id σ =
      ∑ d ∈ n.divisors, Nat.totient d * Fintype.card T ^ (n * m / d)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 28.

Uses 1

Statement usesCylinder shift sum

TheoremCylinder fixed-tiling count for the half-turn when \(m\) is even#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\) with \(m\) even, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2\) be the cell map \((x, y) \mapsto (-1 - x, -1 - y)\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\). Then the cylinder shift sum of \(r^2\) and \(\sigma\) equals \(n \cdot |T|^{nm/2}\).

public theorem_wanted cylinder_r2_m_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Even m) :
    cylinderShiftSum n m (cellR2 n m) σ = n * Fintype.card T ^ (n * m / 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 29.

Uses 2

Statement usesCell map of the half-turn r² · Cylinder shift sum

TheoremCylinder fixed-tiling count for the half-turn when \(m\) is odd and \(n\) is even#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\) with \(m\) odd and \(n\) even, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2\) be the cell map \((x, y) \mapsto (-1 - x, -1 - y)\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\), and let \(t\) be the number of designs fixed by \(\sigma\). Then twice the cylinder shift sum of \(r^2\) and \(\sigma\) equals \(n \left(|T|^{nm/2} + |T|^{(nm - 2)/2}\, t^2\right)\).

The identity is stated after multiplying by \(2\), so that it involves no fractions.

public theorem_wanted cylinder_r2_m_odd_n_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Odd m) (hn : Even n) :
    2 * cylinderShiftSum n m (cellR2 n m) σ =
      n * (Fintype.card T ^ (n * m / 2) +
        Fintype.card T ^ ((n * m - 2) / 2) * tileFixedCount σ 1 ^ 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 29.

Uses 3

Statement usesCell map of the half-turn r² · Cylinder shift sum · Tile designs fixed by a power of a permutation

TheoremCylinder fixed-tiling count for the half-turn when \(m\) and \(n\) are odd#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\) both be odd, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2\) be the cell map \((x, y) \mapsto (-1 - x, -1 - y)\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\), and let \(t\) be the number of designs fixed by \(\sigma\). Then the cylinder shift sum of \(r^2\) and \(\sigma\) equals \(n \cdot |T|^{(nm - 1)/2} \cdot t\).

public theorem_wanted cylinder_r2_odd_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Odd m) (hn : Odd n) :
    cylinderShiftSum n m (cellR2 n m) σ =
      n * Fintype.card T ^ ((n * m - 1) / 2) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 29.

Uses 3

Statement usesCell map of the half-turn r² · Cylinder shift sum · Tile designs fixed by a power of a permutation

TheoremFixed cylinder tilings of the reflection f, n even#●ready to prove

Let \(T\) be a finite set of tile designs, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and let \(n, m \ge 1\) with \(n\) even. For \(a \in \mathbb{Z}/n\mathbb{Z}\) count the tilings \(F : \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z} \to T\) with \(F(-1 - x - a, y) = \sigma(F(x, y))\) for every cell \((x, y)\), and let \(N\) be the sum of these counts over all \(a \in \mathbb{Z}/n\mathbb{Z}\). If \(t_f\) is the number of designs \(d \in T\) with \(\sigma(d) = d\), then

\[2N = n\left(|T|^{nm/2} + |T|^{(nm - 2m)/2} t_f^{2m}\right).\]

public theorem_wanted cylinder_f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Even n) :
    2 * cylinderShiftSum n m (cellF n m) σ =
      n * (Fintype.card T ^ (n * m / 2) +
        Fintype.card T ^ ((n * m - 2 * m) / 2) * tileFixedCount σ 1 ^ (2 * m))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 30.

Uses 3

Statement usesCell map of the reflection f · Cylinder shift sum · Tile designs fixed by a power of a permutation

TheoremCylinder fixed-tiling count for the reflection \(f\) when \(n\) is odd#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\) with \(n\) odd, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(f\) be the cell map \((x, y) \mapsto (-1 - x, y)\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\), and let \(t\) be the number of designs fixed by \(\sigma\). Then the cylinder shift sum of \(f\) and \(\sigma\) equals \(n \cdot |T|^{(nm - m)/2} \cdot t^m\).

public theorem_wanted cylinder_f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Odd n) :
    cylinderShiftSum n m (cellF n m) σ =
      n * Fintype.card T ^ ((n * m - m) / 2) * tileFixedCount σ 1 ^ m

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 30.

Uses 3

Statement usesCell map of the reflection f · Cylinder shift sum · Tile designs fixed by a power of a permutation

TheoremCylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is even#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\) with \(m\) even, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2 f\) be the cell map \((x, y) \mapsto (x, -1 - y)\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\). Then the cylinder shift sum of \(r^2 f\) and \(\sigma\) equals \(\sum_{d \mid n} \varphi(d)\, |T|^{nm / \operatorname{lcm}(d, 2)}\), where \(d\) runs over the positive divisors of \(n\) and \(\varphi\) is Euler's totient function.

public theorem_wanted cylinder_r2f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Even m) :
    cylinderShiftSum n m (cellR2F n m) σ =
      ∑ d ∈ n.divisors,
        Nat.totient d * Fintype.card T ^ (n * m / Nat.lcm d 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 31.

Uses 2

Statement usesCell map of the reflection r²f · Cylinder shift sum

TheoremCylinder fixed-tiling count for the reflection \(r^2 f\) when \(m\) is odd#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\) with \(m\) odd, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). Let \(r^2 f\) be the cell map \((x, y) \mapsto (x, -1 - y)\) of \(\mathbb{Z}/n \times \mathbb{Z}/m\), and for \(k \ge 0\) let \(t_k\) be the number of designs fixed by \(\sigma^k\). Then the cylinder shift sum of \(r^2 f\) and \(\sigma\) equals \(\sum_{d \mid n} \varphi(d)\, |T|^{(nm - n) / \operatorname{lcm}(d, 2)}\, t_d^{\,n/d}\), where \(d\) runs over the positive divisors of \(n\) and \(\varphi\) is Euler's totient function.

public theorem_wanted cylinder_r2f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Odd m) :
    cylinderShiftSum n m (cellR2F n m) σ =
      ∑ d ∈ n.divisors,
        Nat.totient d * Fintype.card T ^ ((n * m - n) / Nat.lcm d 2) *
          tileFixedCount σ d ^ (n / d)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 31.

Uses 3

Statement usesCell map of the reflection r²f · Cylinder shift sum · Tile designs fixed by a power of a permutation

TheoremTorus fixed-tiling sum for the identity#●ready to prove

Let \(n\) and \(m\) be positive integers, let \(T\) be a finite set of tiles and let \(\sigma\) be a permutation of \(T\) with \(\sigma^1 = 1\), that is, the identity. For \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\) let \(N(a, b)\) be the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(x + a, y + b) = \sigma(F(x, y))\) for every cell \((x, y)\). Then, with \(\varphi\) Euler's totient function,

\[\sum_{a \in \mathbb{Z}/n} \sum_{b \in \mathbb{Z}/m} N(a, b) = \sum_{c \mid m} \sum_{d \mid n} \varphi(c) \, \varphi(d) \, |T|^{mn / \operatorname{lcm}(c, d)}.\]

public theorem_wanted rectangularTorus_identity {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 1 = 1) :
    torusShiftSum n m id σ =
      ∑ c ∈ m.divisors, ∑ d ∈ n.divisors,
        Nat.totient c * Nat.totient d *
          Fintype.card T ^ (m * n / Nat.lcm c d)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 34.

Uses 1

Statement usesTorus shift sum

TheoremHalf-turn fixed points on the rectangular torus, both sides even#●ready to prove

Let \(T\) be a finite set of tile designs, \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), and \(n, m\) positive even integers. For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the maps \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(-1-x-a, -1-y-b) = \sigma(F(x, y))\) for all cells \((x, y)\), and let \(\mathrm{fxpt}\) be the sum of these counts over all \(nm\) shifts (the torus fixed-point count of the half-turn \(r^2\)). Write \(t_{\mathrm{id}} = |T|\) and let \(t_{r^2}\) be the number of designs \(d \in T\) with \(\sigma(d) = d\). Then

\[4\,\mathrm{fxpt} = nm\left(3\,t_{\mathrm{id}}^{nm/2} + t_{\mathrm{id}}^{nm/2-2}\,t_{r^2}^4\right).\]

public theorem_wanted rectangularTorus_r2_even_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Even n) (hm : Even m) :
    4 * torusShiftSum n m (cellR2 n m) σ =
      n * m * (3 * Fintype.card T ^ (n * m / 2) +
        Fintype.card T ^ (n * m / 2 - 2) * tileFixedCount σ 1 ^ 4)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 35.

Uses 3

Statement usesCell map of the half-turn r² · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremHalf-turn fixed points on the rectangular torus, both sides odd#●ready to prove

Let \(T\) be a finite set of tile designs, \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), and \(n, m\) positive odd integers. For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the maps \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(-1-x-a, -1-y-b) = \sigma(F(x, y))\) for all cells \((x, y)\), and let \(\mathrm{fxpt}\) be the sum of these counts over all \(nm\) shifts (the torus fixed-point count of the half-turn \(r^2\)). Write \(t_{\mathrm{id}} = |T|\) and let \(t_{r^2}\) be the number of designs \(d \in T\) with \(\sigma(d) = d\). Then

\[\mathrm{fxpt} = nm\,t_{\mathrm{id}}^{(nm-1)/2}\,t_{r^2}.\]

public theorem_wanted rectangularTorus_r2_odd_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Odd n) (hm : Odd m) :
    torusShiftSum n m (cellR2 n m) σ =
      n * m * Fintype.card T ^ ((n * m - 1) / 2) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 35.

Uses 3

Statement usesCell map of the half-turn r² · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremHalf-turn fixed points on the rectangular torus, \(n\) even and \(m\) odd#●ready to prove

Let \(T\) be a finite set of tile designs, \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), \(n\) a positive even integer and \(m\) a positive odd integer. For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the maps \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(-1-x-a, -1-y-b) = \sigma(F(x, y))\) for all cells \((x, y)\), and let \(\mathrm{fxpt}\) be the sum of these counts over all \(nm\) shifts (the torus fixed-point count of the half-turn \(r^2\)). Write \(t_{\mathrm{id}} = |T|\) and let \(t_{r^2}\) be the number of designs \(d \in T\) with \(\sigma(d) = d\). Then

\[2\,\mathrm{fxpt} = nm\left(t_{\mathrm{id}}^{nm/2} + t_{\mathrm{id}}^{nm/2-1}\,t_{r^2}^2\right).\]

public theorem_wanted rectangularTorus_r2_even_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Even n) (hm : Odd m) :
    2 * torusShiftSum n m (cellR2 n m) σ =
      n * m * (Fintype.card T ^ (n * m / 2) +
        Fintype.card T ^ (n * m / 2 - 1) * tileFixedCount σ 1 ^ 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 35.

Uses 3

Statement usesCell map of the half-turn r² · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremHalf-turn fixed points on the rectangular torus, \(n\) odd and \(m\) even#●ready to prove

Let \(T\) be a finite set of tile designs, \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), \(n\) a positive odd integer and \(m\) a positive even integer. For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the maps \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(-1-x-a, -1-y-b) = \sigma(F(x, y))\) for all cells \((x, y)\), and let \(\mathrm{fxpt}\) be the sum of these counts over all \(nm\) shifts (the torus fixed-point count of the half-turn \(r^2\)). Write \(t_{\mathrm{id}} = |T|\) and let \(t_{r^2}\) be the number of designs \(d \in T\) with \(\sigma(d) = d\). Then

\[2\,\mathrm{fxpt} = nm\left(t_{\mathrm{id}}^{nm/2} + t_{\mathrm{id}}^{nm/2-1}\,t_{r^2}^2\right).\]

public theorem_wanted rectangularTorus_r2_odd_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Odd n) (hm : Even m) :
    2 * torusShiftSum n m (cellR2 n m) σ =
      n * m * (Fintype.card T ^ (n * m / 2) +
        Fintype.card T ^ (n * m / 2 - 1) * tileFixedCount σ 1 ^ 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 35.

Uses 3

Statement usesCell map of the half-turn r² · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremTorus fixed-tiling sum for the reflection \(f\), \(n\) even#●ready to prove

Let \(n\) and \(m\) be positive integers with \(n\) even, let \(T\) be a finite set of tiles, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and for \(k \ge 0\) let \(t_k\) be the number of tiles \(d \in T\) with \(\sigma^k(d) = d\). Let \(f(x, y) = (-1 - x, y)\) on \(\mathbb{Z}/n \times \mathbb{Z}/m\), and for \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\) let \(N(a, b)\) be the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(f(x + a, y + b)) = \sigma(F(x, y))\) for every cell \((x, y)\). Then, with \(\varphi\) Euler's totient function,

\[2 \sum_{a \in \mathbb{Z}/n} \sum_{b \in \mathbb{Z}/m} N(a, b) = n \sum_{c \mid m} \varphi(c) \left(|T|^{nm / \operatorname{lcm}(2, c)} + t_c^{2m/c} \, |T|^{(n-2)m / \operatorname{lcm}(2, c)}\right).\]

public theorem_wanted rectangularTorus_f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Even n) :
    2 * torusShiftSum n m (cellF n m) σ =
      n * ∑ c ∈ m.divisors, Nat.totient c *
        (Fintype.card T ^ (n * m / Nat.lcm 2 c) +
          Fintype.card T ^ ((n - 2) * m / Nat.lcm 2 c) *
            tileFixedCount σ c ^ (2 * m / c))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 36.

Uses 3

Statement usesCell map of the reflection f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremTorus fixed-tiling sum for the reflection \(f\), \(n\) odd#●ready to prove

Let \(n\) and \(m\) be positive integers with \(n\) odd, let \(T\) be a finite set of tiles, let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\), and for \(k \ge 0\) let \(t_k\) be the number of tiles \(d \in T\) with \(\sigma^k(d) = d\). Let \(f(x, y) = (-1 - x, y)\) on \(\mathbb{Z}/n \times \mathbb{Z}/m\), and for \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\) let \(N(a, b)\) be the number of tilings \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(f(x + a, y + b)) = \sigma(F(x, y))\) for every cell \((x, y)\). Then, with \(\varphi\) Euler's totient function,

\[\sum_{a \in \mathbb{Z}/n} \sum_{b \in \mathbb{Z}/m} N(a, b) = n \sum_{c \mid m} \varphi(c) \, |T|^{(n-1)m / \operatorname{lcm}(2, c)} \, t_c^{m/c}.\]

public theorem_wanted rectangularTorus_f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hn : Odd n) :
    torusShiftSum n m (cellF n m) σ =
      n * ∑ c ∈ m.divisors, Nat.totient c *
        Fintype.card T ^ ((n - 1) * m / Nat.lcm 2 c) *
          tileFixedCount σ c ^ (m / c)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 36.

Uses 3

Statement usesCell map of the reflection f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed points of \(r^2 f\) on the rectangular torus, \(m\) even#●ready to prove

Let \(T\) be a finite set of tile designs, \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), \(n\) a positive integer and \(m\) a positive even integer. For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the maps \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(x+a, -1-y-b) = \sigma(F(x, y))\) for all cells \((x, y)\), and let \(\mathrm{fxpt}\) be the sum of these counts over all \(nm\) shifts (the torus fixed-point count of the reflection \(r^2 f\)). Write \(t_{\mathrm{id}} = |T|\), let \(t_{(r^2f)^d}\) be the number of designs \(e \in T\) with \(\sigma^d(e) = e\), and let \(\varphi\) be Euler's totient function. Then, with \(d\) running over the positive divisors of \(n\),

\[2\,\mathrm{fxpt} = m \sum_{d \mid n} \varphi(d)\left( t_{\mathrm{id}}^{nm/\operatorname{lcm}(d,2)} + t_{\mathrm{id}}^{n(m-2)/\operatorname{lcm}(d,2)}\,t_{(r^2f)^d}^{2n/d}\right).\]

public theorem_wanted rectangularTorus_r2f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Even m) :
    2 * torusShiftSum n m (cellR2F n m) σ =
      m * ∑ d ∈ n.divisors, Nat.totient d *
        (Fintype.card T ^ (n * m / Nat.lcm d 2) +
          Fintype.card T ^ (n * (m - 2) / Nat.lcm d 2) *
            tileFixedCount σ d ^ (2 * n / d))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 36.

Uses 3

Statement usesCell map of the reflection r²f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed points of \(r^2 f\) on the rectangular torus, \(m\) odd#●ready to prove

Let \(T\) be a finite set of tile designs, \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), \(n\) a positive integer and \(m\) a positive odd integer. For a shift \((a, b) \in \mathbb{Z}/n \times \mathbb{Z}/m\), count the maps \(F : \mathbb{Z}/n \times \mathbb{Z}/m \to T\) with \(F(x+a, -1-y-b) = \sigma(F(x, y))\) for all cells \((x, y)\), and let \(\mathrm{fxpt}\) be the sum of these counts over all \(nm\) shifts (the torus fixed-point count of the reflection \(r^2 f\)). Write \(t_{\mathrm{id}} = |T|\), let \(t_{(r^2f)^d}\) be the number of designs \(e \in T\) with \(\sigma^d(e) = e\), and let \(\varphi\) be Euler's totient function. Then, with \(d\) running over the positive divisors of \(n\),

\[\mathrm{fxpt} = m \sum_{d \mid n} \varphi(d)\, t_{\mathrm{id}}^{n(m-1)/\operatorname{lcm}(d,2)}\,t_{(r^2f)^d}^{n/d}.\]

public theorem_wanted rectangularTorus_r2f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1)
    (hm : Odd m) :
    torusShiftSum n m (cellR2F n m) σ =
      m * ∑ d ∈ n.divisors, Nat.totient d *
        Fintype.card T ^ (n * (m - 1) / Nat.lcm d 2) *
          tileFixedCount σ d ^ (n / d)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 36.

Uses 3

Statement usesCell map of the reflection r²f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremSquare-torus fixed points of the identity#●ready to prove

Let \(n\) be a positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be the identity permutation of \(T\). Let \(S\) be the sum, over all shifts \(v \in (\mathbb{Z}/n\mathbb{Z})^2\), of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(c + v) = \sigma(F(c))\) for every cell \(c\). Then \(S = \sum_{d_1 \mid n} \sum_{d_2 \mid n} \varphi(d_1) \, \varphi(d_2) \, |T|^{n^2/\operatorname{lcm}(d_1, d_2)}\), where \(d_1\) and \(d_2\) run over the positive divisors of \(n\) and \(\varphi\) is Euler's totient function.

public theorem_wanted squareTorus_identity {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 1 = 1) :
    torusShiftSum n n id σ =
      ∑ d₁ ∈ n.divisors, ∑ d₂ ∈ n.divisors,
        Nat.totient d₁ * Nat.totient d₂ *
          Fintype.card T ^ (n ^ 2 / Nat.lcm d₁ d₂)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 1

Statement usesTorus shift sum

TheoremFixed tilings of the odd square torus under a half-turn#●ready to prove

Let \(n\) be an odd positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), and write \(t_1\) for the number of designs \(d \in T\) with \(\sigma(d) = d\). Let \(S\) be the torus shift sum of the half-turn cell map \(r^2(x, y) = (-1-x, -1-y)\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^2(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(S = n^2 \, |T|^{(n^2-1)/2} \, t_1\).

public theorem_wanted squareTorus_r2_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hn : Odd n) :
    torusShiftSum n n (cellR2 n n) σ =
      n ^ 2 * Fintype.card T ^ ((n ^ 2 - 1) / 2) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 3

Statement usesCell map of the half-turn r² · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the even square torus under a half-turn#●ready to prove

Let \(n\) be an even positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\), and write \(t_1\) for the number of designs \(d \in T\) with \(\sigma(d) = d\). Let \(S\) be the torus shift sum of the half-turn cell map \(r^2(x, y) = (-1-x, -1-y)\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^2(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(4S = n^2 \left(3 \, |T|^{n^2/2} + |T|^{n^2/2 - 2} \, t_1^4\right)\).

Multiplying by four replaces the paper's coefficients \(3/4\) and \(1/4\) by integers.

public theorem_wanted squareTorus_r2_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hn : Even n) :
    4 * torusShiftSum n n (cellR2 n n) σ =
      n ^ 2 * (3 * Fintype.card T ^ (n ^ 2 / 2) +
        Fintype.card T ^ (n ^ 2 / 2 - 2) * tileFixedCount σ 1 ^ 4)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 3

Statement usesCell map of the half-turn r² · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremSquare-torus fixed points of the reflection \(f\), even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). For \(k \ge 1\) let \(t_k\) be the number of designs in \(T\) fixed by \(\sigma^k\). Let \(f\) be the cell map \((x, y) \mapsto (-1-x, y)\) of \((\mathbb{Z}/n\mathbb{Z})^2\), and let \(S\) be the sum, over all shifts \(v \in (\mathbb{Z}/n\mathbb{Z})^2\), of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(f(c + v)) = \sigma(F(c))\) for every cell \(c\). Then \(2S = n \sum_{d \mid n} \varphi(d) \, (a_d + b_d)\), where \(d\) runs over the positive divisors of \(n\), \(\varphi\) is Euler's totient function, \(\ell_d = \operatorname{lcm}(2, d)\), \(a_d = |T|^{n^2/\ell_d}\) and \(b_d = |T|^{(n^2-2n)/\ell_d} \, t_d^{2n/d}\).

public theorem_wanted squareTorus_f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hn : Even n) :
    2 * torusShiftSum n n (cellF n n) σ =
      n * ∑ d ∈ n.divisors, Nat.totient d *
        (Fintype.card T ^ (n ^ 2 / Nat.lcm 2 d) +
          Fintype.card T ^ ((n ^ 2 - 2 * n) / Nat.lcm 2 d) *
            tileFixedCount σ d ^ (2 * n / d))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 3

Statement usesCell map of the reflection f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremSquare-torus fixed points of the reflection \(f\), odd \(n\)#●ready to prove

Let \(n\) be an odd positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^2 = 1\). For \(k \ge 1\) let \(t_k\) be the number of designs in \(T\) fixed by \(\sigma^k\). Let \(f\) be the cell map \((x, y) \mapsto (-1-x, y)\) of \((\mathbb{Z}/n\mathbb{Z})^2\), and let \(S\) be the sum, over all shifts \(v \in (\mathbb{Z}/n\mathbb{Z})^2\), of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(f(c + v)) = \sigma(F(c))\) for every cell \(c\). Writing \(\varphi\) for Euler's totient function,

\[S = n \sum_{d \mid n} \varphi(d) \, |T|^{(n^2-n)/\operatorname{lcm}(2, d)} \, t_d^{n/d},\]

where \(d\) runs over the positive divisors of \(n\).

public theorem_wanted squareTorus_f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hn : Odd n) :
    torusShiftSum n n (cellF n n) σ =
      n * ∑ d ∈ n.divisors, Nat.totient d *
        Fintype.card T ^ ((n ^ 2 - n) / Nat.lcm 2 d) *
          tileFixedCount σ d ^ (n / d)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 3

Statement usesCell map of the reflection f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the even square torus under the reflection \(r^2 f\)#●ready to prove

Let \(n\) be an even positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\); for \(k \in \mathbb{N}\) write \(t_k\) for the number of designs \(d \in T\) with \(\sigma^k(d) = d\), and let \(\varphi\) be Euler's totient function. Let \(S\) be the torus shift sum of the cell map \(g(x, y) = (x, -1-y)\) of \(r^2 f\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(g(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(2S = n \sum_{d \mid n} \varphi(d) \left(|T|^{n^2/\operatorname{lcm}(2, d)} + |T|^{(n^2-2n)/ \operatorname{lcm}(2, d)} \, t_d^{2n/d}\right)\).

public theorem_wanted squareTorus_r2f_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hn : Even n) :
    2 * torusShiftSum n n (cellR2F n n) σ =
      n * ∑ d ∈ n.divisors, Nat.totient d *
        (Fintype.card T ^ (n ^ 2 / Nat.lcm 2 d) +
          Fintype.card T ^ ((n ^ 2 - 2 * n) / Nat.lcm 2 d) *
            tileFixedCount σ d ^ (2 * n / d))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 3

Statement usesCell map of the reflection r²f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the odd square torus under the reflection \(r^2 f\)#●ready to prove

Let \(n\) be an odd positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\); for \(k \in \mathbb{N}\) write \(t_k\) for the number of designs \(d \in T\) with \(\sigma^k(d) = d\), and let \(\varphi\) be Euler's totient function. Let \(S\) be the torus shift sum of the cell map \(g(x, y) = (x, -1-y)\) of \(r^2 f\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(g(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(S = n \sum_{d \mid n} \varphi(d) \, |T|^{(n^2-n)/\operatorname{lcm}(2, d)} \, t_d^{n/d}\).

public theorem_wanted squareTorus_r2f_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) (hn : Odd n) :
    torusShiftSum n n (cellR2F n n) σ =
      n * ∑ d ∈ n.divisors, Nat.totient d *
        Fintype.card T ^ ((n ^ 2 - n) / Nat.lcm 2 d) *
          tileFixedCount σ d ^ (n / d)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 38.

Uses 3

Statement usesCell map of the reflection r²f · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the odd square torus under a quarter-turn#●ready to prove

Let \(n\) be an odd positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^4 = 1\), and write \(t_1\) for the number of designs \(d \in T\) with \(\sigma(d) = d\). Let \(S\) be the torus shift sum of the quarter-turn cell map \(r(x, y) = (-1-y, x)\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(S = n^2 \, |T|^{(n^2-1)/4} \, t_1\).

public theorem_wanted squareTorus_r_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (hn : Odd n) :
    torusShiftSum n n (cellR n) σ =
      n ^ 2 * Fintype.card T ^ ((n ^ 2 - 1) / 4) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 39.

Uses 3

Statement usesCell map of the quarter-turn r · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremSquare-torus fixed points of the rotation \(r\), even \(n\)#●ready to prove

Let \(n\) be an even positive integer, let \(T\) be a finite set of tile designs, and let \(\sigma\) be a permutation of \(T\) with \(\sigma^4 = 1\). For \(k \ge 1\) let \(t_k\) be the number of designs in \(T\) fixed by \(\sigma^k\). Let \(r\) be the cell map \((x, y) \mapsto (-1-y, x)\) of \((\mathbb{Z}/n\mathbb{Z})^2\), and let \(S\) be the sum, over all shifts \(v \in (\mathbb{Z}/n\mathbb{Z})^2\), of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r(c + v)) = \sigma(F(c))\) for every cell \(c\). Then

\[2S = n^2 \left( |T|^{n^2/4} + |T|^{(n^2-4)/4} \, t_1^2 \, t_2 \right).\]

public theorem_wanted squareTorus_r_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (hn : Even n) :
    2 * torusShiftSum n n (cellR n) σ =
      n ^ 2 * (Fintype.card T ^ (n ^ 2 / 4) +
        Fintype.card T ^ ((n ^ 2 - 4) / 4) *
          tileFixedCount σ 1 ^ 2 * tileFixedCount σ 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 39.

Uses 3

Statement usesCell map of the quarter-turn r · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the odd square torus under a three-quarter turn#●ready to prove

Let \(n\) be an odd positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^4 = 1\), and write \(t_1\) for the number of designs \(d \in T\) with \(\sigma(d) = d\). Let \(S\) be the torus shift sum of the three-quarter-turn cell map \(r^3(x, y) = (y, -1-x)\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^3(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(S = n^2 \, |T|^{(n^2-1)/4} \, t_1\).

public theorem_wanted squareTorus_r3_odd {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (hn : Odd n) :
    torusShiftSum n n (cellR3 n) σ =
      n ^ 2 * Fintype.card T ^ ((n ^ 2 - 1) / 4) * tileFixedCount σ 1

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 39.

Uses 3

Statement usesCell map of the three-quarter turn r³ · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the even square torus under a three-quarter turn#●ready to prove

Let \(n\) be an even positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^4 = 1\), and for \(k = 1, 2\) write \(t_k\) for the number of designs \(d \in T\) with \(\sigma^k(d) = d\). Let \(S\) be the torus shift sum of the three-quarter-turn cell map \(r^3(x, y) = (y, -1-x)\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(r^3(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(2S = n^2 \left(|T|^{n^2/4} + |T|^{(n^2-4)/4} \, t_1^2 \, t_2\right)\).

public theorem_wanted squareTorus_r3_even {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 4 = 1) (hn : Even n) :
    2 * torusShiftSum n n (cellR3 n) σ =
      n ^ 2 * (Fintype.card T ^ (n ^ 2 / 4) +
        Fintype.card T ^ ((n ^ 2 - 4) / 4) *
          tileFixedCount σ 1 ^ 2 * tileFixedCount σ 2)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 39.

Uses 3

Statement usesCell map of the three-quarter turn r³ · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the square torus under the diagonal reflection#●ready to prove

Let \(n\) be a positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\); write \(t_1\) for the number of designs \(d \in T\) with \(\sigma(d) = d\), and let \(\varphi\) be Euler's totient function. Let \(S\) be the torus shift sum of the cell map \(g(x, y) = (y, x)\) of \(rf\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(g(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(S = n \left(\sum_{d \mid n,\ d \text{ odd}} \varphi(d) \, |T|^{(n^2-n)/(2d)} \, t_1^{n/d} + \sum_{d \mid n,\ d \text{ even}} \varphi(d) \, |T|^{n^2/(2d)}\right)\).

The paper writes this as a single divisor sum with a summand depending on the parity of \(d\).

public theorem_wanted squareTorus_rf {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) :
    torusShiftSum n n (cellRF n) σ = n *
      ((∑ d ∈ n.divisors.filter Odd,
          Nat.totient d * Fintype.card T ^ ((n ^ 2 - n) / (2 * d)) *
            tileFixedCount σ 1 ^ (n / d)) +
        ∑ d ∈ n.divisors.filter Even,
          Nat.totient d * Fintype.card T ^ (n ^ 2 / (2 * d)))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 40.

Uses 3

Statement usesCell map of the diagonal reflection rf · Tile designs fixed by a power of a permutation · Torus shift sum

TheoremFixed tilings of the square torus under the anti-diagonal reflection#●ready to prove

Let \(n\) be a positive integer, \(T\) a finite set of tile designs and \(\sigma\) a permutation of \(T\) with \(\sigma^2 = 1\); write \(t_1\) for the number of designs \(d \in T\) with \(\sigma(d) = d\), and let \(\varphi\) be Euler's totient function. Let \(S\) be the torus shift sum of the cell map \(g(x, y) = (-1-y, -1-x)\) of \(r^3 f\) on \((\mathbb{Z}/n\mathbb{Z})^2\), that is, the sum over all shifts \((a, b) \in (\mathbb{Z}/n\mathbb{Z})^2\) of the number of tilings \(F : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) with \(F(g(c + (a, b))) = \sigma(F(c))\) for every cell \(c\). Then \(S = n \left(\sum_{d \mid n,\ d \text{ odd}} \varphi(d) \, |T|^{(n^2-n)/(2d)} \, t_1^{n/d} + \sum_{d \mid n,\ d \text{ even}} \varphi(d) \, |T|^{n^2/(2d)}\right)\).

public theorem_wanted squareTorus_r3f {T : Type*} [Fintype T] [DecidableEq T]
    (n : ℕ) [NeZero n] (σ : Equiv.Perm T) (hσ : σ ^ 2 = 1) :
    torusShiftSum n n (cellR3F n) σ = n *
      ((∑ d ∈ n.divisors.filter Odd,
          Nat.totient d * Fintype.card T ^ ((n ^ 2 - n) / (2 * d)) *
            tileFixedCount σ 1 ^ (n / d)) +
        ∑ d ∈ n.divisors.filter Even,
          Nat.totient d * Fintype.card T ^ (n ^ 2 / (2 * d)))

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 40.

Uses 3

Statement usesCell map of the antidiagonal reflection r³f · Tile designs fixed by a power of a permutation · Torus shift sum

DefinitionAction of the rectangle group on grid cells#✓fully proved

Let \(n, m \in \mathbb{N}\) and view the cells of the \(n \times m\) grid as \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\). Write the elements of the dihedral group of order \(8\) as rotations \(r_i\) and reflections \(sr_i\) for \(i \in \mathbb{Z}/4\mathbb{Z}\). Each element acts on cells as follows: \(r_0\) by the identity, \(r_i\) with \(i \ne 0\) by the half-turn \((x, y) \mapsto (-1 - x, -1 - y)\), \(sr_0\) by the reflection \((x, y) \mapsto (-1 - x, y)\), and \(sr_i\) with \(i \ne 0\) by the reflection \((x, y) \mapsto (x, -1 - y)\).

The paper's rectangle group \(D_4 = \langle r^2, f \rangle\) is the subgroup \(\{r_0, r_2, sr_0, sr_2\}\), with \(f = sr_0\), \(r^2 = r_2\) and \(r^2 f = sr_2\). On this subgroup the assignment of cell maps is a homomorphism into maps under composition; the values at \(r_1\), \(r_3\), \(sr_1\) and \(sr_3\) are never used.

public def rectCellAction (n m : ℕ) : DihedralGroup 4 → ZMod n × ZMod m → ZMod n × ZMod m
  | .r i => if i = 0 then id else cellR2 n m
  | .sr i => if i = 0 then cellF n m else cellR2F n m

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definitions 1.4.1 and 1.4.2 (the dihedral action on cells).

Uses 3 · Used by 6

Statement usesCell map of the reflection f · Cell map of the half-turn r² · Cell map of the reflection r²f

Used byBurnside count of cylinder tilings under rectangle symmetries · Rectangle-group cell action of the half-turn · Rectangle-group cell action of the identity · Rectangle-group cell action of the reflection r²f · Rectangle-group cell action of the reflection f · Burnside count of torus tilings under the rectangle group

TheoremRectangle-group cell action of the identity#✓fully proved

Let \(n, m \in \mathbb{N}\), and let \(r_i\) (\(i \in \mathbb{Z}/4\mathbb{Z}\)) denote the rotations of the dihedral group of order \(8\). Under the rectangle-group action on the cells \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid, the identity element \(r_0\) acts as the identity map.

public theorem rectCellAction_r_zero (n m : ℕ) : rectCellAction n m (.r 0) = id

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.1.

Uses 1

Statement usesAction of the rectangle group on grid cells

TheoremRectangle-group cell action of the half-turn#✓fully proved

Let \(n, m \in \mathbb{N}\), and let \(r_i\) (\(i \in \mathbb{Z}/4\mathbb{Z}\)) denote the rotations of the dihedral group of order \(8\). Under the rectangle-group action on the cells \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid, \(r_2\) acts as the half-turn \((x, y) \mapsto (-1 - x, -1 - y)\).

public theorem rectCellAction_r_two (n m : ℕ) : rectCellAction n m (.r 2) = cellR2 n m

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.1.

Uses 2

Statement usesCell map of the half-turn r² · Action of the rectangle group on grid cells

TheoremRectangle-group cell action of the reflection f#✓fully proved

Let \(n, m \in \mathbb{N}\), and let \(sr_i\) (\(i \in \mathbb{Z}/4\mathbb{Z}\)) denote the reflections of the dihedral group of order \(8\). Under the rectangle-group action on the cells \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid, \(sr_0\) (the paper's \(f\)) acts as the reflection \((x, y) \mapsto (-1 - x, y)\).

public theorem rectCellAction_sr_zero (n m : ℕ) : rectCellAction n m (.sr 0) = cellF n m

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.1.

Uses 2

Statement usesCell map of the reflection f · Action of the rectangle group on grid cells

TheoremRectangle-group cell action of the reflection r²f#✓fully proved

Let \(n, m \in \mathbb{N}\), and let \(sr_i\) (\(i \in \mathbb{Z}/4\mathbb{Z}\)) denote the reflections of the dihedral group of order \(8\). Under the rectangle-group action on the cells \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) of the \(n \times m\) grid, \(sr_2\) (the paper's \(r^2 f\)) acts as the reflection \((x, y) \mapsto (x, -1 - y)\).

public theorem rectCellAction_sr_two (n m : ℕ) : rectCellAction n m (.sr 2) = cellR2F n m

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.1.

Uses 3

Statement usesCell map of the reflection r²f · Action of the rectangle group on grid cells

Proof usesCell map of the reflection f

DefinitionThe dihedral action on the cells of the square grid#✓fully proved

For a natural number \(n\), let \(r\) and \(f\) be the maps of \((\mathbb{Z}/n\mathbb{Z})^2\) given by \(r(x, y) = (-1 - y, x)\) (the quarter-turn) and \(f(x, y) = (-1 - x, y)\) (the reflection). The dihedral group of order \(8\) has the rotations \(r_i\) and the reflections \(sr_i\) for \(i \in \mathbb{Z}/4\mathbb{Z}\). The action sends \(r_i\) to the \(i\)-fold iterate \(r^i\) and \(sr_i\) to \(f \circ r^i\), where \(i\) is read as an integer in \(\{0, 1, 2, 3\}\).

Since \(f \circ r \circ f = r^{-1}\) on cells, this assignment turns the multiplication of the dihedral group into composition of maps.

public def squareCellAction (n : ℕ) : DihedralGroup 4 → ZMod n × ZMod n → ZMod n × ZMod n
  | .r i => (cellR n)^[i.val]
  | .sr i => cellF n n ∘ (cellR n)^[i.val]

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.2 (the dihedral action on cells).

Uses 2 · Used by 3

Statement usesCell map of the reflection f · Cell map of the quarter-turn r

Used byThe rotation \(r\) acts on the square grid as the quarter-turn · The reflection \(sr_0\) acts on the square grid as \(f\) · Burnside count of tilings of the square torus

TheoremThe rotation \(r\) acts on the square grid as the quarter-turn#✓fully proved

For every natural number \(n\), the square cell action of the dihedral group of order \(8\) on \(\mathbb{Z}/n \times \mathbb{Z}/n\) sends the rotation \(r\) to the quarter-turn \((x, y) \mapsto (-1-y, x)\).

public theorem squareCellAction_r_one (n : ℕ) : squareCellAction n (.r 1) = cellR n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.2.

Uses 2

Statement usesCell map of the quarter-turn r · The dihedral action on the cells of the square grid

TheoremThe reflection \(sr_0\) acts on the square grid as \(f\)#✓fully proved

Let \(r_i\) and \(sr_i\) (\(i \in \mathbb{Z}/4\mathbb{Z}\)) denote the rotations and the reflections of the dihedral group of order \(8\). For every natural number \(n\), the dihedral action on the cells \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\) of the \(n \times n\) grid sends the reflection \(sr_0\) to the reflection \(f\), \((x, y) \mapsto (-1 - x, y)\).

public theorem squareCellAction_sr_zero (n : ℕ) : squareCellAction n (.sr 0) = cellF n n

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Definition 1.4.2.

Uses 2

Statement usesCell map of the reflection f · The dihedral action on the cells of the square grid

TheoremBurnside count of cylinder tilings under rectangle symmetries#●ready to prove

Let \(T\) be a finite set of tile designs, let \(n, m \ge 1\), and let \(R\) be a subgroup of the dihedral group \(\langle r, f \rangle\) of order \(8\) that is contained in the rectangle group \(\lbrace 1, r^2, f, r^2 f \rbrace\) and acts on \(T\). For \(g \in R\) let \(\phi_g\) be its cell map on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\): \(\phi_1(x, y) = (x, y)\), \(\phi_{r^2}(x, y) = (-1 - x, -1 - y)\), \(\phi_f(x, y) = (-1 - x, y)\) and \(\phi_{r^2 f}(x, y) = (x, -1 - y)\). Consider the equivalence relation on tilings \(F : \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z} \to T\) generated by relating \(F\) to \(F'\) whenever there are \(a \in \mathbb{Z}/n\mathbb{Z}\) and \(g \in R\) with \(F'(x, y) = g^{-1} \cdot F(\phi_g(x + a, y))\) for every cell \((x, y)\). For \(g \in R\) let \(N_g\) be the sum over \(a \in \mathbb{Z}/n\mathbb{Z}\) of the number of tilings \(F\) with \(F(\phi_g(x + a, y)) = g \cdot F(x, y)\) for every cell \((x, y)\). Then the number of equivalence classes is \(\frac{1}{n|R|} \sum_{g \in R} N_g\).

As in the paper, the tile designs form an \(R\)-set: only the subgroup \(R\) acts on \(T\).

public theorem_wanted cylinder_distinctTilings_burnside {T : Type*} [Fintype T] [DecidableEq T]
    (n m : ℕ) [NeZero n] [NeZero m]
    (R : Subgroup (DihedralGroup 4)) [DecidablePred (· ∈ R)] [MulAction R T]
    (hR : ∀ g ∈ R, g = .r 0 ∨ g = .r 2 ∨ g = .sr 0 ∨ g = .sr 2) :
    (Nat.card (Quot fun F F' : ZMod n × ZMod m → T =>
        ∃ a : ZMod n, ∃ g : R, ∀ c, F' c = g⁻¹ • F (rectCellAction n m g (c.1 + a, c.2))) : ℚ) =
      1 / (n * Nat.card R) * ∑ g : R,
        (cylinderShiftSum n m (rectCellAction n m g) (MulAction.toPerm g : Equiv.Perm T) : ℚ)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 32 (jis-2024-24.6.1-thm-32).

Uses 2

Statement usesCylinder shift sum · Action of the rectangle group on grid cells

TheoremBurnside count of torus tilings under the rectangle group#●ready to prove

Let \(T\) be a finite set of tile designs and let \(n, m \ge 1\). Let \(R\) be a subgroup of the dihedral group of order \(8\), whose elements are the rotations \(r_i\) and reflections \(sr_i\) for \(i \in \mathbb{Z}/4\mathbb{Z}\), such that every element of \(R\) is one of \(r_0\), \(r_2\), \(sr_0\), \(sr_2\), and let \(R\) act on \(T\). Tilings of the \(n \times m\) torus are maps \(F : \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z} \to T\). Identify tilings under the equivalence relation generated by \(F \sim \bigl(c \mapsto g^{-1} \cdot F(g \cdot (c + v))\bigr)\) for \(v \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) and \(g \in R\), where \(g\) acts on cells by the rectangle-group cell action. Then the number of equivalence classes is

\[\frac{1}{n m \lvert R \rvert} \sum_{g \in R} \mathrm{fix}_g,\]

where \(\mathrm{fix}_g\) is the torus shift sum of the cell map of \(g\) and the permutation \(t \mapsto g \cdot t\) of \(T\), that is, the number of pairs \((v, F)\) of a shift \(v \in \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/m\mathbb{Z}\) and a tiling \(F\) with \(F(g \cdot (c + v)) = g \cdot F(c)\) for every cell \(c\).

public theorem_wanted rectTorus_distinctTilings_burnside {T : Type*} [Fintype T]
    [DecidableEq T] (n m : ℕ) [NeZero n] [NeZero m]
    (R : Subgroup (DihedralGroup 4)) [DecidablePred (· ∈ R)] [MulAction R T]
    (hR : ∀ g ∈ R, g = .r 0 ∨ g = .r 2 ∨ g = .sr 0 ∨ g = .sr 2) :
    (Nat.card (Quot fun F F' : ZMod n × ZMod m → T =>
        ∃ v : ZMod n × ZMod m, ∃ g : R, ∀ c, F' c = g⁻¹ • F (rectCellAction n m g (c + v))) : ℚ) =
      1 / (n * m * Nat.card R) * ∑ g : R,
        (torusShiftSum n m (rectCellAction n m g) (MulAction.toPerm g : Equiv.Perm T) : ℚ)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 37 (jis-2024-24.6.1-thm-37).

Uses 2

Statement usesAction of the rectangle group on grid cells · Torus shift sum

TheoremBurnside count of tilings of the square torus#●ready to prove

Let \(n\) be a positive integer and let \(T\) be a finite set of tile designs. Let \(\rho(x, y) = (-1-y, x)\) and \(\phi(x, y) = (-1-x, y)\) on the cells \((\mathbb{Z}/n\mathbb{Z})^2\) of the \(n \times n\) torus, and let the dihedral group \(D_8 = \langle r, f \rangle\) of the square act on cells by \(r^i \cdot c = \rho^i(c)\) and \(fr^i \cdot c = \phi(\rho^i(c))\) for \(i \in \mathbb{Z}/4\mathbb{Z}\). Let \(R\) be a subgroup of \(D_8\) that acts on \(T\), and write \(g \cdot d\) for the action of \(g \in R\) on a design \(d \in T\). Call two tilings \(F, F' : (\mathbb{Z}/n\mathbb{Z})^2 \to T\) equivalent when they are related by the equivalence relation generated by: \(F'(c) = g^{-1} \cdot F(g \cdot (c + v))\) for every cell \(c\), for some \(v \in (\mathbb{Z}/n\mathbb{Z})^2\) and \(g \in R\). Then the number of equivalence classes is

\[\frac{1}{n^2 |R|} \sum_{g \in R} \sum_{v \in (\mathbb{Z}/n\mathbb{Z})^2} N(g, v),\]

where \(N(g, v)\) is the number of tilings \(F\) with \(F(g \cdot (c + v)) = g \cdot F(c)\) for every cell \(c\); the inner sum is the torus shift sum of \(g\).

public theorem_wanted squareTorus_distinctTilings_burnside {T : Type*} [Fintype T]
    [DecidableEq T] (n : ℕ) [NeZero n]
    (R : Subgroup (DihedralGroup 4)) [DecidablePred (· ∈ R)] [MulAction R T] :
    (Nat.card (Quot fun F F' : ZMod n × ZMod n → T =>
        ∃ v : ZMod n × ZMod n, ∃ g : R, ∀ c, F' c = g⁻¹ • F (squareCellAction n g (c + v))) : ℚ) =
      1 / (n ^ 2 * Nat.card R) * ∑ g : R,
        (torusShiftSum n n (squareCellAction n g) (MulAction.toPerm g : Equiv.Perm T) : ℚ)

Sources

• Peter Kagey, William Keehn, Counting Tilings of the n × m Grid, Cylinder, and Torus, Journal of Integer Sequences 27 (2024), Article 24.6.1, Theorem 41 (jis-2024-24.6.1-thm-41).

Uses 2

Statement usesThe dihedral action on the cells of the square grid · Torus shift sum

24 fully proved57 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.