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.
The dyadic rationals of , their finite levels , and their density in
Definition
Throughout, is the canonical natural of (The canonical natural of a field), and as is standard is abbreviated to once no ambiguity results (For every in a complete ordered field there is a natural with ). For , is the natural-number power of Exponentiation of natural numbers, , and its agreement with the integer power in , distinct from but agreeing with the real (integer) power of Integer powers by that item's clause (d): . Writing for as just agreed, this lets be read as a natural number or as the real interchangeably.
For put
the order on the naturals and being that of Order on the natural numbers. Each is a finite subset of (Intervals of : the nine order-convex forms, nondegeneracy, and length) with (the cases and ); it has at most elements, so is finite in the sense of Finite, countably infinite, countable, uncountable. The dyadic rationals of are
a countable union of finite sets. Each level is nested in the next: if then (multiplying the natural inequality by ), and in (clearing the common factor , licensed by Ordered field), so every element of is exhibited as an element of ; hence and is genuinely increasing, not merely a union.
The level decomposition, stated and discharged here because the recursion of Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into , and conversely such a space is normal consumes it. For ,
and the new points are pairwise distinct, none lies in , and each lies strictly between the -consecutive pair and . Strict betweenness: , and dividing by the positive preserves strict order (Ordered field), so . Distinctness: is injective. Disjointness from : with would give after clearing the positive factor and applying injectivity of ; but gives , and gives , so no such exists. The union is all of : given with , the set is nonempty (), so by The well-ordering principle it has a least element , and since ; writing (Every nonzero natural number is a successor) gives , so or . In the first case (with since ); in the second it is (with since forces ). Finally, any two elements of lie together in a common level: one lies in some and the other in some , and both then lie in by the nesting just proved.
is dense in : for every and every real there is with . First, a growth fact about natural-number powers, proved by induction on (The principle of mathematical induction): for every . At , . If , then , the middle inequality adding the inductive hypothesis to itself and the last holding since ; both steps use only that the order of is compatible with addition (Order on the natural numbers). Transporting the inequality into by the order-preserving (Canonical naturals are positive and strictly increasing) gives for every .
Now fix and a real . By For every in a complete ordered field there is a natural with fix a natural with . Put ; then , so by Inverses of positives are positive, and reciprocation reverses order . Consider . It is nonempty, since satisfies because ; so by The well-ordering principle has a least element , and because . If then , and since , so , within distance of itself. If then and, by minimality of , , that is ; combined with this gives , and since . Either way some satisfies .
Remarks
-
Every dyadic rational of other than and lies strictly between them, since exactly when .
-
The finite levels, not itself, are what the construction of Urysohn's lemma recurses on. is presented here as the increasing union precisely so that a family indexed by can be built one finite level at a time, each level adding only finitely many new indices to the one before.
Depends on
Intervals of : the nine order-convex forms, nondegeneracy, and length
Integer powers
The canonical natural of a field
Exponentiation of natural numbers, , and its agreement with the integer power in
For every in a complete ordered field there is a natural with
Ordered field
The natural numbers (von Neumann)
Order on the natural numbers
The principle of mathematical induction
The well-ordering principle
Canonical naturals are positive and strictly increasing
Inverses of positives are positive, and reciprocation reverses order
Finite, countably infinite, countable, uncountable
Every nonzero natural number is a successor