PROVED (LEAN), the site's label; its suffix is a catalog label explained under Formalization. The status-defining source is Theorem 1.2 of Moreira, Richter and Robertson (Ann. of Math. (2) 189 (2019), 605--652, refereed), which proves the statement for positive upper density along any Følner sequence; the site's statement is the case of the intervals $\{1,\ldots,N\}$. The claim page is Moreira, Richter and Robertson, accepted on the site curator's credit and the refereed publication; the 2026 Lean development that declares itself a formalization of their theorem is linked there and gives no formalized evidence, since this corpus has not built or audited it.