The local dynamical structure of $Δ^*$ sets via a new Furstenberg family algebra
Angelina Blahodatna, Lauren Detmold, Daniel Glasscock, Anh N. Le
math.CO
Oct 7, 2026 · v1
math.DS
TL;DR
All results, including the main theorem on Δ* sets having local Bohr structure, are formally verified in Lean, with a GitHub repository and Palomar submission.
Abstract
In this paper, we strengthen the connection between the combinatorics of difference sets and the dynamics of group rotations. Our main result shows that sets which have non-empty intersection with all difference subsets of a commutative semigroup possess local Bohr structure. This generalizes results of Bergelson, Furstenberg, and Weiss and Host and Kra from the integers to arbitrary commutative semigroups. We accomplish this by A) utilizing a recent result showing that the regionally proximal relation is an equivalence relation for minimal actions of commutative semigroups and by B) describing a new, DeMorgan-type algebra on Furstenberg families that allows for efficient manipulation and computation. We formally verify all of the results in this paper in Lean. The main results are verified in a Palomar submission, and we link to a Github repository containing code for the complete verification.
Problem
Δ* sets meet every difference set. In the integers they are known to have local Bohr structure, by results of Bergelson–Furstenberg–Weiss and Host–Kra. The question is whether this structure extends to arbitrary commutative semigroups.
Approach
The authors use the recent result that the regionally proximal relation is an equivalence relation for minimal actions of commutative semigroups. They also introduce a new DeMorgan-type algebra of operations on Furstenberg families for manipulating combinatorial notions of largeness. The proof first reduces to uniformly recurrent sets arising from minimal dynamics. It then links sets of Bohr recurrence to Δ sets via the regionally proximal relation. All results are formally verified in Lean.
Results
Δ* subsets of commutative semigroups are shown to be very strongly piecewise Bohr_0, generalizing the integer results. The family algebra also gives a short proof that piecewise syndeticity is partition regular, plus new characterizations of C* sets. The Lean verification is available on GitHub, with the main results also in a Palomar submission.
