发表机构
U. of Massachusetts Lowell; U. of Denver（马萨诸塞大学洛厄尔分校; 丹佛大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文通过引入新型 Furstenberg 族代数，证明与交换半群所有差子集相交的集合具有局部 Bohr 结构，推广了整数上的经典结果，并在 Lean 中完成形式化验证。
AI 中文摘要
本文加强了差集组合学与群旋转动力学之间的联系。我们的主要结果表明，与交换半群的所有差子集都有非空交集的集合具有局部 Bohr 结构。这推广了 Bergelson、Furstenberg 和 Weiss 以及 Host 和 Kra 的结果，从整数推广到任意交换半群。我们通过以下方式实现这一目标：A) 利用最近的一个结果，即对于交换半群的极小平作用，区域近邻关系是等价关系；B) 描述一种新的、DeMorgan 型的 Furstenberg 族代数，该代数允许高效的操作和计算。我们在 Lean 中正式验证了本文的所有结果。主要结果在 Palomar 提交中得到了验证，我们链接到一个包含完整验证代码的 Github 仓库。
英文摘要
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.
Comments41 pages; verification code at https://github.com/dglasscockUML/NSF_LEAPS
