From Regional Topology to Point-Class Topology in Tarski's Geometry of Solids

Patrick Barlatier, Richard Dapoigny

arXiv:2607.18502v2 Primary: math.LO Secondary: math.AT

Abstract

Tarski's geometry of solids reconstructs point-like entities from concentric families of spherical regions rather than taking points as primitive. We formalize this reconstruction in Coq within a nominal mereological framework inspired by Leśniewski, and study how the regional geometry of solids induces a topology on reconstructed point-classes without adding new point individuals. Three of Tarski's postulates concerning solids and interior points, P2--P4, are derived as theorems. We refine Tarski's interior-point notion and define a regional interior operator satisfying the four Kuratowski interior axioms, together with a boundary operation and an encoding of RCC8 relations. We then pass to the setoid of ball representatives modulo same_center. Each ball generates a stable basic point-plural GBasicPointSet(Q), and these plurals form a basis for a metatheoretic topology on reconstructed point-classes. This topology is Hausdorff under Tarski's separation axiom Three_points and non-discrete under the local richness hypothesis BallCenterBundle. Finally, geometric neighbourhoods yield a closure operator GClosurePoint satisfying the four Kuratowski closure axioms and respecting extensional point-set equality. The formalization thus verifies the passage from a regional topology of solids to a Hausdorff topology and neighbourhood closure on reconstructed point-classes.

Disclosure

“rk addresses a different but related problem: the construction of a verified neighbourhood and closure semantics for region-induced point-class plurals. These approaches 1 During the preparation of the formal development, Codex and ChatGPT Pro were used as exploratory aids for testing alternative formulations, exposing ambiguities, and suggesting possible proof patterns. All final definitions, theorem statements, Coq scripts, and mathematical interpretations were reviewed an”
PDF page 2

Classification: Proof ideas or individual proof-step assistance
Multiplier: 8
Verified: 2026-08-23T19:02:08.925874Z

Structural counts

Pages 26 pdf

Theorems 22 source

Lemmas 25 source

Propositions 0 source

Corollaries 0 source

Definitions 36 source

Displayed equations 46 source

Bibliography entries 46 source

Appendix pages 0 estimated

Count notes

Source counts use the expanded primary TeX file PB_RB_JSL26_arxiv_v12.tex.
Appendix pages include the first PDF page with an explicit Appendix heading through the final page.