Paper: https://arxiv.org/abs/2606.30782
Lean 4 formalization of Dana Scott's 1972 Continuous Lattices (LNM 274):
injective T₀-spaces, Scott topology, way-below, function spaces, inverse limits.
Standalone package — no dependency on the 1980/1982 formalizations. Cross-presentation
equivalence theorems live in scott_models; this repo is registered
with Palomar on its own as
PALOMAR-2026-08-24-000003
(see PROVENANCE.md).
The pin is leanprover/lean4:v4.33.0 (same as qlambda).
| File | Role |
|---|---|
arxiv.md |
Formalization narrative and theorem inventory |
sources/ScottContinLatt1972.md |
OCR source text (Scott 1972 through Milner correction) |
Scott1972/ |
Sorry-free formalization of the paper |
Challenge.lean |
Palomar statement of record: Theorem 4.4 + definitions |
Solution.lean |
Palomar solution module: imports Scott1972/* proofs |
comparator.json |
Comparator config for the compared theorem and definitions |
formalization.yaml |
Palomar / formalization.yaml v0.4 metadata |
PROVENANCE.md |
Standalone Palomar submission; relation to scott_models |
lake exe cache get
lake buildlake build typechecks Scott1972, Challenge.lean, and Solution.lean. Before a
Palomar submission, run:
bash scripts/compare_challenge_solution_types.shChallenge.lean imports only Mathlib and states theorem_4_4 in the wording of
sources/ScottContinLatt1972.md (Theorem 4.4) with a deliberate sorry. The
explicit Homeomorph uses the product/subspace topology on the inverse limit
and Definition 3.1's pointwise Pi topology on its function space. The proof is
in FunctionSpaceTower.lean, imported by Solution.lean. Proposition 4.1
follows Scott's Proposition 3.8 + Lemma 3.9 + injectivity + Theorem 2.12 route;
Lemma 4.5 follows Scott's induction. The homeomorphism is built from Scott's
displayed formulas for i∞ and j∞.
The compared theorem uses propext, Classical.choice, and Quot.sound only.