2026/07/20 by Patrick Barlatier, Richard Dapoigny
Mathematics · #math.LO #math.AT
Tarski's geometry of solids reconstructs point-like objects from concentric families of spherical regions rather than taking points as primitive entities. We formalize this reconstruction in Coq within a nominal mereological framework inspired by Lesniewski. The main question is how a regional, point-free geometry can support a Kuratowski closure operator on the objects obtained from such reconstructed points. We distinguish the regional topology of Tarski-Lesniewski solids from a point-class topology built on ball representatives. Point-like objects are treated as concentric point-classes, namely equivalence classes of ball representatives under equality of concentric families. Regional objects provide the source of basic neighbourhoods, but closure acts on point-class plurals rather than on solids themselves. We define point-open plurals and introduce a neighbourhood-based closure operator on them. The central Coq theorem proves that this operator satisfies the four Kuratowski closure axioms. We further define point-closed plurals as fixed points of this closure and derive a topological boundary remainder. The formalization separates regional openness, representative equivalence, and topological adherence, while avoiding the reification of reconstructed points as mereological individuals.