def UniformSet.cubeOf {d : ℕ} (N m j : ℕ) (p : Fin d → ℕ) : Fin d → ℕ

cubeOf N m j p returns the coordinates of the dyadic cube at scale Δ^j = N^{-j} (working in the grid {0, …, N^m - 1}^d) that contains the lattice point p. Each coordinate is obtained by dividing p i by N^(m - j), i.e. by truncating the last m - j base-N digits.

noncomputable def UniformSet.subcubeCovering (N m j d : ℕ) (X : Finset (Fin d → ℕ)) (Q : Fin d → ℕ) : ℕ

The branching count |Q ∩ X|^*_{Δ^{j+1}}: the number of distinct sub-cubes at scale Δ^{j+1} that are needed to cover the points of X lying inside the scale-Δ^j cube Q. Formally, it counts the image of X ∩ Q under the next finer cube map cubeOf N m (j + 1).

def UniformSet.IsUniform (N m d : ℕ) (X : Finset (Fin d → ℕ)) : Prop

IsUniform N m d X says that the set X ⊂ {0, …, N^m - 1}^d is (Δ, m)-uniform with Δ = 1/N: for every scale j < m, there is a single "branching factor" R_j such that every non-empty scale-Δ^j cube Q of X is split into exactly R_j non-empty scale-Δ^{j+1} sub-cubes (|Q ∩ X|^*_{Δ^{j+1}} = R_j).