Kurepa’s line/tree correspondence: downstream proof contract

In ZFC, a Suslin line exists if and only if a Suslin tree exists. The line convention is Suslin lines in order language and the tree convention is Aronszajn, Suslin and special trees. This result is recorded here without proof and has no role as a local prerequisite.

The proof belongs to the planned page suslin-trees-lines-algebras-and-independence. The tree-to-line direction requires a normal-tree reduction, a lexicographic order on maximal branches, and completion while preserving ccc and nonseparability. The reverse direction requires the nowhere-separable reduction before selecting nested intervals to form a countable-level tree. These are mathematical obligations, not consequences of the two definitions. In particular distinct nodes with identical predecessor sets at a limit level cannot be treated as already separated by a first successor disagreement. The later proof must account for that normalization and for preservation under completion.

The source gives the two directions as Monk Theorems 9.13 and 9.18, with the line reduction in Theorem 9.17. The present page supplies the terminology and the independent tree constructions, but does not certify those later arguments.