{"id":"palomar/PALOMAR-2026-10-18-000015","url":"https://github.com/dglasscockUML/NSF_LEAPS/tree/e275c4e2bb477c110f542e606dac0519963e964c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000015-v1.json","repo":"https://github.com/dglasscockUML/NSF_LEAPS","tags":["math.CO","math.DS","msc:05D10","msc:37B05","msc:37B20","msc:22A20","dynamics","difference-sets","lean"],"score":0,"title":"The local dynamical structure of Δ* sets via a new Furstenberg family algebra","trust":"high","domain":"math.CO","source":"palomar","authors":["Angelina Blahodatna","Lauren Detmold","Daniel Glasscock","Anh N. Le"],"reviews":0,"subject":"math.CO","summary":"This development formalizes in Lean 4 the results of the paper \"The local dynamical structure of Δ* sets via a new Furstenberg family algebra\", which strengthens the connection between the combinatorics of difference sets and the dynamics of group rotations. Let S be a discrete semigroup. A set A ⊆ S is syndetic if there is a finite F ⊆ S with S = ∪_{f ∈ F} f⁻¹A; a Δ set if there is a sequence s₁, s₂, … in S with s_j ∈ s_i A for all i < j; and a Bohr_0 set if it contains the preimage of an open neighborhood of the identity under a semigroup homomorphism from S to a finite-dimensional torus.…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"The local dynamical structure of Δ* sets via a new Furstenberg family algebra","identifier":"arXiv:2610.10416","relationship":"formalizes"}]}