True-life biomedical images, such as the synapses of neurons, are too large and onerous to process. How should the data structures of huge digital images be reliably condensed without losing their homological properties? Poza et al. propose a specialized reduction scheme for homological image processing. The unaccustomed reader of topology is encouraged to browse the imaginative algorithms used to enlighten computational topology in *Computational topology* [1], prior to exploring the formal mathematical validations of the algorithms for image reduction and processing in this paper.

The reputable basic perturbation lemma (BPL) is used to verify the correctness of algorithms for preserving the homological properties of digital images split into segments of small data structures. The authors present a considerably shortened formalization of the BPL. They (1) define chain complexes as families of structure-preserving maps (module morphisms) of images, (2) provide an algorithm for building the admissible discrete vector fields from the matrices of finite-type chain complexes, (3) present a vector field reduction theorem based on the BPL for computing the homology groups of much smaller finite-type chain complexes, (4) prove a generalized theorem for making use of reductions to construct the decompositions of chain complexes, and (5) show how the BPL is used to reduce the chain complexes of a digital image with the library of matrices in the SSReflect language for proving theorems in the Coq system.

The authors provide theoretical insights into proving the congruency between the homology of the chain complex of an image and the homology of its reduced chain complex. They offer insights into the creative use of the Haskell programming language for rapid prototyping of time-consuming automatic program verifications. The authors compellingly advocate the need to develop new algorithms, more effective data structures, and faster executing proof assistants for reduction in homological processing of biomedical images.