Open Research Index

catskillsresearch/scott1972

Lars Warren Ericson

Palomar Registrypalomar/PALOMAR-2026-08-24-000003Aug 24, 2026math.LOscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-24-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-24-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-24-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'