Papers With

← All papers
First page of Chain Continuity and Scott-Closed Interpolation

Chain Continuity and Scott-Closed Interpolation

Yuxu Chen

math.GN Oct 13, 2026 · v1 math.LO
formalization topology logic
Read PDF arXiv abstract Code
TL;DR
The order-theoretic results on chain-continuous dcpos and Scott-closed interpolation are formalized in Lean 4, with code in a public GitHub repository.
Abstract
We prove that every chain-continuous dcpo is continuous and that its way-below relation is the relational square of its chain-below relation, answering a question of Erné. A subalgebra lattice obtained from a locally finite Jónsson algebra shows that the chain-below relation itself need not interpolate. For approximation by Scott-closed sets, we give a finite-upper-bound characterization on lower-set lattices and characterize interpolation by an extension property for directed lower sets. This yields a countably based, completely distributive algebraic lattice on which chain and directed approximation coincide, whereas Scott-closed approximation fails to interpolate, answering questions of Erné and of Ho and Zhao.
Problem

Erné asked whether every chain-continuous dcpo is continuous, and whether certain generalized continuity notions entail interpolation. Ho and Zhao raised related questions about approximation by Scott-closed sets.

Approach

A cofinality analysis of chain-generated ideals shows that a non-interpolable chain-below pair must satisfy a cofinality condition, so two interpolation failures cannot occur consecutively. A locally finite Jónsson algebra yields a subalgebra lattice that serves as a counterexample to chain-below interpolation. Scott-closed approximation on lower-set lattices is characterized by finite upper bounds, and its interpolation by an extension property for directed lower sets. A Lean 4 formalization accompanies the work.

Results

Every chain-continuous dcpo is continuous, and its way-below relation is the relational square of the chain-below relation, which itself need not interpolate. A countably based, completely distributive algebraic lattice is constructed on which Scott-closed approximation fails to interpolate, answering questions of Erné and of Ho and Zhao.