Abstract
These theories formalize region quadtrees, which are traditionally used
to represent two-dimensional images of (black and white) pixels.
Building on these quadtrees, addition and multiplication of recursive block matrices are verified.
The generalization of region quadtrees to \(k\) dimensions is also formalized.