Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Linear-order completion and density

Statement

Let L be a linear order. A completion of L means a linear order M satisfying the following exact clauses:

  • (C1) L⊆M, with the same order on L;
  • (C2) every subset of M, including the empty set, has a least upper bound and a greatest lower bound in M;
  • (C3) every x∈M is the least upper bound in M of some subset of L; and
  • (C4) if a∈L is the least upper bound in L of A⊆L, then it remains the least upper bound of A in M.

Every linear order has such a completion, and any two completions are uniquely isomorphic over L. If L is dense, then it is order-dense in every completion. If in addition L has no endpoints, has no uncountable pairwise disjoint family of nonempty open intervals, and no nonempty open interval of L is separable in its order topology, then deleting the possible first and last elements of a completion produces a dense, no-endpoint, boundedly complete order with the same two latter properties.

Facts & Assumptions

Given: A linear order L; for the transfer clause, the additional hypotheses displayed in the statement.

[F1]

A linear order is a partial order in which every two elements are comparable; least upper bounds are unique by antisymmetry. Partial order and partially ordered set

[F2]

Open intervals are endpoint-excluding order-convex sets; we use the same displayed interval notation in an arbitrary linear order. Intervals of R: the nine order-convex forms, nondegeneracy, and length

[F3]
[F4]

Separability means the existence of an at most countable dense subset. Separability: the existence of an at most countable dense subset

[F5]

“Countable” means finite or countably infinite. Finite, countably infinite, countable, uncountable

[A1]

AC supplies simultaneous witnesses from families of nonempty intervals. The Axiom of Choice

Proof

1.1F1given

Let C(L) consist of the subsets X⊆L such that (i) b<a∈X implies b∈X, and (ii) whenever X has a least upper bound a in L, one has a∈X. Order C(L) by inclusion. These are the downward-closed cuts with every already-existing L-supremum closed in.

2.1F1step 1.1

The inclusion order on C(L) is linear. Indeed, if X,Y∈C(L) and a∈X∖Y, then every b∈Y satisfies b<a (otherwise downward closure would put a in Y), and hence b∈X; thus Y⊊X.

3.1F1step 1.1step 2.1

Every family X⊆C(L) has a supremum. Put U=⋃X. If U has no least upper bound in L, then U∈C(L) and is the union-supremum. If a=sup⁡LU exists, downward closure gives U∪{a}=(−∞,a], which lies in C(L) and is the least cut above every member of X. This includes X=∅. Infima then exist as suprema of sets of lower bounds, so C(L) is complete.

3.2F1step 1.1step 2.1

Send a∈L to j(a)=(−∞,a]. Each j(a) is a cut, and a<b holds exactly when j(a)⊊j(b), so j is an order embedding. Replacing L by its named copy j[L] if necessary gives literal inclusion as required by C1.

4.1F1step 1.1step 3.1step 3.2

Every cut X is sup⁡{j(a):a∈X}, including the empty cut. If a=sup⁡LA for A⊆L, then j(a) is an upper bound of j[A]; any cut Y above every j(x) for x∈A contains every b<a, and it contains a either because a∈A or because clause (ii) closes Y under the supremum a. Hence j(a)=sup⁡j[A]. Thus the constructed order satisfies C2-C4.

5.1F1step 1.1step 4.1

Let P be any completion satisfying C1-C4 and define τP(x)={a∈L:a≤Px}. This is a cut: downward closure is immediate, while if b=sup⁡LτP(x), C4 makes b its supremum in P, which also equals x by C3, so b=x∈τP(x). If x<y, C3 gives an a∈L with x<a≤y, so τP(x)⊊τP(y). Conversely the traces reflect order. For every cut X, if x=sup⁡PX, then τP(x)=X: an a<x in the trace cannot upper-bound X, and if a=x∈L, then a=sup⁡LX and cut closure puts a in X. Thus τP is an onto isomorphism from P to C(L) and fixes L. Applying this to two completions gives the unique isomorphism over L, since C3 forces any such isomorphism to send each sup⁡PA to sup⁡NA.

5.2F1step 4.1

Suppose now that L is dense and M is a completion. If x<y in M, C3 supplies b∈L with x<b≤y. If x∈L, density in L gives x<a<b for some a∈L. If x∉L and there were no a∈L with x<a<b, then b would be the least upper bound in L of the L-points below x; C4 would make that supremum equal both b and x, a contradiction. Hence in all cases some a∈L satisfies x<a<y, so L is order-dense in M.

6.1F2A1step 5.2

If (Iξ)ξ<ω1 were pairwise disjoint nonempty open intervals of M, order-density and A1 would choose aξ<bξ in L∩Iξ. The nonempty L-intervals (aξ,bξ) would remain pairwise disjoint, contradicting the corresponding hypothesis on L. Thus the interval ccc passes to M.

6.2F2F3F4F5A1step 5.2

Suppose a nonempty open interval I of M had a countable dense set D. Choose a<b in L∩I. The set D∩(a,b) is nonempty and countable; list it as (dn)n<ω, repeating entries in the finite case. For every pair di<dj, use order-density and A1 to choose eij∈L with di<eij<dj. The set E={eij:di<dj} is countable by diagonal enumeration of the pairs of natural indices. Given u<v in L∩(a,b), density of D first gives di∈(u,v) and then dj∈(di,v), so u<eij<v. Therefore E is dense in the nonempty L-interval (a,b), contradicting the hypothesis on L. No nonempty open interval of M is separable.

7.1A1step 5.2step 6.1step 6.2∎

Finally assume that L has no endpoints, and delete from M its first and last elements when they exist. Neither deleted point belongs to L. The remainder M∘ still contains the order-dense copy of L, is dense and has no endpoints, and retains the conclusions of steps 6.1-6.2. If a nonempty A⊆M∘ is bounded above there, then sup⁡MA lies above a member of A and below an upper bound in M∘, so it is neither deleted endpoint and belongs to M∘; hence M∘ is boundedly complete. This proves every assertion and records the precise use of AC.

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources