Topology on integer grids links connectivity to consecutive points
Construction and formal verification of a special topology on {\mathbb{Z}}^{n}: characterization of connected subsets
Symbolic ComputationLogic in Computer Science
Summary
The paper studies a way to look at whole-number grids (like points with integer coordinates) so that connected groups are exactly the ones next to each other without gaps. The authors show how to build such a structure in any number of dimensions, explaining how points connect through immediate neighbors. They also checked their methods carefully with computer proof tools to make sure everything is correct. This work helps understand the fundamental shape and connection of points on grids.
What this means in practice
- •For digital image processors: Use the topology characterization to identify connected pixel regions that correspond exactly to consecutive integer-indexed points for refined image segmentation.
- •For network routing engineers: Model connectivity in grid-based network layouts to optimize pathfinding algorithms based on integer-step accessibility.
A theory result. No direct application yet.
Authors
Ignacio Vega-Páez
Abstract
We examine whether the integers admit a topology whose connected subsets are precisely the sets of consecutive integers. The main result gives a construction for every integer lattice {\mathbb{Z}}^{n}, n>0; the answer for Z is then obtained as a corollary. We prove that the neighborhoods determined by the parity of the sum of the coordinates form a basis and that topological connectedness agrees exactly with accessibility by finite paths of unit lattice steps. We also present a deductive audit and the correspondence between this argument and a verification in Lean 4 and Mathlib, including the empty set and the independent formal characterization of integer intervals. The construction and mathematical result originate in Problem 5712, proposed by Dan Marcus and solved in 1970 by the Cleveland State University group; the present article contributes a detailed exposition and a report on formal verification.