{"id":"palomar/PALOMAR-2026-10-20-000017","url":"https://github.com/dglasscockUML/NSF_LEAPS/tree/a3cf7072e465276748dd8522b1af92802c9f21b5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000017-v1.json","repo":"https://github.com/dglasscockUML/NSF_LEAPS","tags":["math.DS","msc:37B05","msc:37B20","topological-dynamics","semigroup-actions","regionally-proximal-relation","lean-formalization"],"score":0,"title":"The regionally proximal relation for commutative semigroup actions","trust":"high","domain":"math.DS","source":"palomar","authors":["Angelina Blahodatna","Lauren Detmold","Daniel Glasscock","Anh N. Le"],"reviews":0,"subject":"math.DS","summary":"The regionally proximal relation and the equicontinuous structure relation are fundamental relations in topological dynamics that capture equicontinuous behaviour in a topological dynamical system and its factors. For minimal actions of abelian groups they are known to be equivalence relations and to coincide. This development formalizes in Lean 4 the results of the paper \"The regionally proximal relation for commutative semigroup actions\", which generalizes these facts from group actions to semigroup actions. Throughout, a system is an action of a discrete semigroup S on a compact Hausdorff…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"The regionally proximal relation for commutative semigroup actions","identifier":"arXiv:2610.10397","relationship":"formalizes"}]}