Fixed polycubes

DefinitionLattice cells#✓fully proved

For a natural number \(d\), a lattice cell in dimension \(d\) is a point of \(\mathbb{Z}^d\), that is, a function assigning an integer to each of the \(d\) coordinate axes.

def latticeCell (d : ℕ) : Type := Fin d → ℤ
Sources
  • Sebastian Luther and Stephan Mertens, The Perimeter of Proper Polycubes, Journal of Integer Sequences 20 (2017), Article 17.9.5, https://cs.uwaterloo.ca/journals/JIS/VOL20/Mertens/mert4.tex: a d-dimensional polycube is a set of face-connected cells in ℤ^d, lines 115–117 (also arXiv:1705.03688v1).
Used by 7
Used byFace adjacency of lattice cells · Fixed polycubes · Canonical position of a cell set · Polycube · Lunnon's dimension decomposition for fixed polycubes · Proper dimension · Proper fixed polycubes

DefinitionFace adjacency of lattice cells#✓fully proved

Two lattice cells \(x, y \in \mathbb{Z}^d\) are face adjacent when there is an axis \(k\) such that \(x_j = y_j\) for every axis \(j \ne k\) and \(|x_k - y_k| = 1\).

def faceAdjacent (d : ℕ) (x y : latticeCell d) : Prop :=
  ∃ k : Fin d, (∀ j : Fin d, j ≠ k → x j = y j) ∧ (y k = x k + 1 ∨ x k = y k + 1)
Sources
  • Luther–Mertens, JIS 20 (2017), Article 17.9.5, lines 277–279: this is the "neighbors in the polycube" relation underlying the adjacency graph, in which two vertices are connected if the corresponding cells are neighbors.
Uses 1 · Used by 2
Statement usesLattice cells
Used byPolycube · Lunnon's dimension decomposition for fixed polycubes

DefinitionPolycube#✓fully proved

A finite set \(S\) of lattice cells in \(\mathbb{Z}^d\) is a polycube when it is nonempty and any two cells \(x, y \in S\) are joined by a finite sequence of cells of \(S\), starting at \(x\) and ending at \(y\), in which consecutive cells are face adjacent.

def isPolycubeCells (d : ℕ) (S : Finset (latticeCell d)) : Prop :=
  S.Nonempty ∧ ∀ x ∈ S, ∀ y ∈ S,
    Relation.ReflTransGen
      (fun a b : latticeCell d => faceAdjacent d a b ∧ a ∈ S ∧ b ∈ S) x y
Sources
  • Luther–Mertens, JIS 20 (2017), Article 17.9.5, lines 115–117: a d-dimensional polycube is a set of face-connected cells in ℤ^d. Connectivity is expressed by reflexive transitive closure of face adjacency restricted to the set S.
Uses 2 · Used by 3
Statement usesFace adjacency of lattice cells · Lattice cells
Used byFixed polycubes · Lunnon's dimension decomposition for fixed polycubes · Proper fixed polycubes

DefinitionCanonical position of a cell set#✓fully proved

A finite set \(S\) of lattice cells in \(\mathbb{Z}^d\) is in canonical position when, for every axis \(k\), every cell \(x \in S\) has \(x_k \ge 0\) and some cell \(x \in S\) has \(x_k = 0\); that is, the minimum of each coordinate over \(S\) is \(0\).

def isCanonicalCells (d : ℕ) (S : Finset (latticeCell d)) : Prop :=
  ∀ k : Fin d, (∃ x ∈ S, x k = 0) ∧ ∀ x ∈ S, 0 ≤ x k
Sources
  • Luther–Mertens, JIS 20 (2017), Article 17.9.5, lines 115–117: fixed polycubes are identified up to translation. Each class has a unique representative with minima at zero. Only translations are quotiented, so rotations and reflections stay distinct orientations.
Uses 1 · Used by 3
Statement usesLattice cells
Used byFixed polycubes · Lunnon's dimension decomposition for fixed polycubes · Proper fixed polycubes

DefinitionProper dimension#✓fully proved

The proper dimension of a finite set \(S\) of lattice cells in \(\mathbb{Z}^d\) is the number of axes \(k\) on which \(S\) varies, that is, for which there are cells \(x, y \in S\) with \(x_k \ne y_k\).

noncomputable def properDimension (d : ℕ) (S : Finset (latticeCell d)) : ℕ :=
  Nat.card { k : Fin d // ∃ x ∈ S, ∃ y ∈ S, x k ≠ y k }
Sources
  • Luther–Mertens, JIS 20 (2017), Article 17.9.5, lines 160–162: a polycube spanning i dimensions is proper in i dimensions. Asinowski–Barequet–Barequet–Rote, Proper n-Cell Polycubes in n−3 Dimensions, Journal of Integer Sequences 15 (2012), Article 12.8.4, lines 171–172: proper dimension is the dimension of the convex hull of cell centers, which for axis-aligned cells equals the count of varying axes.
Uses 1 · Used by 2
Statement usesLattice cells
Used byLunnon's dimension decomposition for fixed polycubes · Proper fixed polycubes

DefinitionFixed polycubes#✓fully proved

For natural numbers \(d\) and \(n\), the fixed \(n\)-cell polycubes in dimension \(d\) are represented by the finite sets \(S\) of lattice cells in \(\mathbb{Z}^d\) that are polycubes (nonempty and connected through face adjacency), have exactly \(n\) cells, and are in canonical position (the minimum of each coordinate over \(S\) is \(0\)).

def fixedPolycube (d n : ℕ) : Type :=
  { S : Finset (latticeCell d) // isPolycubeCells d S ∧ S.card = n ∧ isCanonicalCells d S }
Uses 3 · Used by 3
Statement usesCanonical position of a cell set · Polycube · Lattice cells
Used byNumber of fixed polycubes · Lunnon's dimension decomposition for fixed polycubes · Proper fixed polycubes

DefinitionNumber of fixed polycubes#✓fully proved

For natural numbers \(d\) and \(n\), \(A_d(n)\) is the number of fixed \(n\)-cell polycubes in dimension \(d\), that is, the number of \(n\)-cell polycubes in \(\mathbb{Z}^d\) that are in canonical position.

noncomputable def fixedPolycubeCount (d n : ℕ) : ℕ :=
  Nat.card (fixedPolycube d n)
Uses 1 · Used by 1
Statement usesFixed polycubes
Used byLunnon's dimension decomposition for fixed polycubes

DefinitionProper fixed polycubes#✓fully proved

For natural numbers \(n\) and \(i\), the fixed \(n\)-cell polycubes proper in dimension \(i\) are the fixed \(n\)-cell polycubes in dimension \(i\) whose proper dimension is \(i\), that is, which vary along each of the \(i\) axes.

def properFixedPolycube (n i : ℕ) : Type :=
  { P : fixedPolycube i n // properDimension i P.val = i }
Uses 5 · Used by 2
Statement usesFixed polycubes · Canonical position of a cell set · Polycube · Lattice cells · Proper dimension
Used byLunnon's dimension decomposition for fixed polycubes · Number of proper fixed polycubes

DefinitionNumber of proper fixed polycubes#✓fully proved

For natural numbers \(n\) and \(i\), \(\mathrm{DX}(n,i)\) is the number of fixed \(n\)-cell polycubes proper in dimension \(i\), that is, of fixed \(n\)-cell polycubes in dimension \(i\) whose proper dimension is \(i\).

noncomputable def properFixedPolycubeCount (n i : ℕ) : ℕ :=
  Nat.card (properFixedPolycube n i)
Sources
  • Asinowski et al., JIS 15 (2012), Article 12.8.4, line 978, state \(\mathrm{DX}(n,0) = 0\) for \(n > 1\).
Uses 1 · Used by 1
Statement usesProper fixed polycubes
Used byLunnon's dimension decomposition for fixed polycubes

TheoremLunnon's dimension decomposition for fixed polycubes#✓fully proved

Let \(d\) and \(n\) be natural numbers with \(n > 1\), let \(A_d(n)\) be the number of fixed \(n\)-cell polycubes in dimension \(d\), and for each \(i\) let \(\mathrm{DX}(n,i)\) be the number of fixed \(n\)-cell polycubes proper in dimension \(i\). Then

\[A_d(n) = \sum_{i=1}^{n-1} \binom{d}{i} \, \mathrm{DX}(n,i).\]

The hypothesis \(n > 1\) is needed: the printed formula omits its domain and fails at \(n = 1\), where the single cell is a polycube proper in dimension \(0\) and so is counted only by the \(i = 0\) term, which the sum excludes. For \(n > 1\) that term vanishes, since \(\mathrm{DX}(n,0) = 0\).

theorem lunnon_fixed_polycube_dimension_decomposition
    (d n : ℕ) (hn : 1 < n) :
    fixedPolycubeCount d n =
      Finset.sum (Finset.Ico 1 n) (fun i => Nat.choose d i * properFixedPolycubeCount n i)
Sources
  • Sebastian Luther and Stephan Mertens, The Perimeter of Proper Polycubes, Journal of Integer Sequences 20 (2017), Article 17.9.5, https://cs.uwaterloo.ca/journals/JIS/VOL20/Mertens/mert4.tex: Lunnon's classical formula eq:lunnon-a, lines 172–175, with sum i = 1, …, n-1 and factor C(d,i); DX notation and the at-most-n-1 dimensions bound, lines 163–166. Original: W. F. Lunnon, Counting multidimensional polyominoes, Comput. J. 18 (1975), 366–367. DX(n,0) = 0 for n > 1 from Asinowski–Barequet–Barequet–Rote, JIS 15 (2012), Article 12.8.4, line 978, https://cs.uwaterloo.ca/journals/JIS/VOL15/Barequet/barequet2.tex.
Uses 9
Statement usesNumber of fixed polycubes · Number of proper fixed polycubes
Proof usesFace adjacency of lattice cells · Fixed polycubes · Canonical position of a cell set · Polycube · Lattice cells · Proper dimension · Proper fixed polycubes
10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.