Formal squares over the unit square separate FS-domains from RB-domains

Abstract

Every RB-domain is an FS-domain. Whether the converse holds was a long-standing open problem. We prove that the domain of closed axis-parallel squares in the plane whose centres lie in the unit square $[0,1]^2$, with the whole plane adjoined and ordered by reverse inclusion, is an FS-domain but not an RB-domain. The proof is quantitative. A finite-grid argument first shows that, on every finite slab $[0,1]^2\times[0,m]$, for every approximate identity and every $\varepsilon>0$, one member of the approximate identity has radius excess (i.e., the output radius minus the input radius) uniformly at most $\varepsilon$. By contrast, for every deflation and every $m>0$, the radius excess is at least $m/(4m+1)$ at some point of the slab $[0,1]^2\times[0,m]$. This solution was obtained independently of the recent work of Chen, Kou, and Lyu and uses a different method.

Disclosure

“Acknowledgments The author used ChatGPT (OpenAI) as a research and writing assistant during the development of this manuscript. I had been developing the under- lying proof strategy for some time and, on 30 April 2026, asked ChatGPT to help work out the most technically demanding analytic parts. Through a back-and-forth discussion, the remaining gaps were filled and a complete proof emerged on the same date. The choice of the formal-square model for this problem, t”

PDF page 24

Classification

Substantial proof generation

Multiplier

10

Verified

2026-08-23T05:02:14.772126Z

Structural counts