{"id":"palomar/PALOMAR-2026-08-24-000003","url":"https://github.com/catskillsresearch/scott1972/tree/278ba1745b6fb023fc3e9ffe53b7106ce60222c1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-24-000003-v2.json","repo":"https://github.com/catskillsresearch/scott1972","tags":["math.LO","math.GN","msc:06B35","msc:54H99","msc:03B40","domain-theory","continuous-lattices","lean-formalization"],"score":0,"title":"catskillsresearch/scott1972","trust":"high","domain":"math.LO","source":"palomar","authors":["Lars Warren Ericson"],"reviews":0,"subject":"math.LO","summary":"A Lean 4 / mathlib formalization of Dana Scott's 1972 paper *Continuous Lattices* (LNM 274), through the Milner correction (pp. 135–136). The Palomar compared result is Theorem 4.4 as worded in sources/ScottContinLatt1972.md: the inverse limit D_∞ of the recursively defined sequence ⟨D_n, j_n⟩ of function spaces is not only a continuous lattice, but it is also homeomorphic to its own function space [D_∞ → D_∞]. The compared Homeomorph explicitly uses the product/subspace topology on the inverse limit and the pointwise Pi topology on the function space. The full paper development…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-24","reactions":{},"formalized":true,"formalizes":[{"title":"Continuous Lattices","identifier":"","relationship":"formalizes"}]}