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.
Intervals of : the nine order-convex forms, nondegeneracy, and length
Definition
Throughout, is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) with its order (Order on the reals).
A subset is order-convex when
The intervals of are the sets of the following nine forms, where :
| bounded forms | one-sided and full forms | ||
|---|---|---|---|
An interval is open when both of its written endpoints are excluded, that is for the forms , , and ; it is closed when both written endpoints are included, that is for , , and . The forms and are half-open.
The symbols are notation and not elements of . They mark which side carries no endpoint condition at all; the five forms in the right column are defined by the displayed conditions on alone, and no arithmetic is ever performed with . This is the same refusal to extend silently that Conventions: , unbounded sets, and the extended reals records for suprema.
Every one of the nine forms is order-convex. Each is defined by a conjunction of at most two conditions, each of the shape , , or , and each such condition is inherited by an intermediate point: if and then , and if and then , by transitivity of the order (Ordered field). Applying this to whichever one or two conditions define the form in question gives whenever and .
Bounded intervals. An interval is bounded (Lower bound, bounded below, bounded set) exactly when it is of one of the four forms in the left column: for those, is a lower bound and an upper bound. The other five forms are unbounded, on the side or sides written with ; the verification is in the remarks below.
Nondegeneracy. An interval is degenerate when it has at most one element, and nondegenerate when it has at least two. For the four bounded forms with endpoints and :
- is nonempty exactly when , and it is nondegenerate exactly when . It is the singleton when .
- , and are nonempty exactly when , and then each is nondegenerate.
The only assertion here that is not immediate from the defining conditions is that makes nonempty with at least two points. It holds because , which follows from by adding , respectively , to both sides and halving (Ordered field); repeating the halving inside produces a second point.
Closed bounded intervals. These are the sets with , which is exactly the condition making them nonempty. They are the intervals the nested interval property is stated for, and the phrase closed bounded interval always carries the hypothesis in this library.
Length. The length of a bounded interval presented by its endpoints is
Length is attached to the presentation by endpoints and is not recovered from the set: , and are all empty when , and so is for any other , while each of these presentations has length , so nothing inconsistent arises; but the endpoints are named explicitly at every point where a length is used in this library, and never inferred from the set. Unbounded intervals are assigned no length.
Definition references
Remarks
-
Why the five unbounded forms really are unbounded. Take and suppose were an upper bound of it. The element satisfies , so , and , since (Basic properties of the absolute value) and (The multiplicative identity is positive). That contradicts . The same computation with replaced by any element of handles the open form, and reflecting through the origin handles and ; itself is unbounded on both sides for the same reason. Note that this uses no Archimedean property: it is the failure of a single bound, not the cofinality of the naturals.
-
The converse classification is not asserted here. It is true that every order-convex subset of is empty or one of the nine forms, and the proof runs through suprema and infima, but nothing in this library needs it and it is not proved anywhere here. What is used is only the direction proved above: each of the nine forms is order-convex.
-
Degenerate intervals are kept, not excluded. and are intervals under this definition. Excluding them would force a nonemptiness hypothesis into every statement that produces an interval, and the nested interval property is a good illustration: its conclusion is that the intersection is nonempty, and in the equality case the intersection is the degenerate interval , which is exactly the single point.