ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

$\sup {q \in Q : q > 0, q^{2} < 2} = \sqrt{2}$ in $R$ , and no supremum in $Q$

Example

Let $ι : Q \to R$ be the canonical embedding of the rationals as an ordered subfield of $R$ (The unique embedding of ℚ into an ordered field) and put $S = {q \in Q : q > 0 and q^{2} < 2} .$ Viewed inside $R$ , the set $S$ has a supremum, namely $\sup S = \sqrt{2}$ , the unique nonnegative real whose square is $2$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ). Viewed inside $Q$ , the same set has no supremum at all: it has upper bounds in $Q$ , but none of them is least.

This is the reason $R$ exists. The rationals form an ordered field in which a perfectly ordinary bounded set fails to have a least upper bound, because the number that ought to be that bound is irrational (FALSE: some rational number squares to 2). The least-upper-bound property (Complete ordered field (least-upper-bound property)) is precisely the repair, and the value it supplies here is $\sqrt{2}$ .

The order-theoretic defect exhibited below is the exact counterpart of the metric defect recorded in FALSE: the rationals are complete, where a Cauchy sequence of rationals fails to have a rational limit. The two are different statements about the same hole in $Q$ , and this library repairs it twice, once by Dedekind cuts and once by Cauchy sequences.

Facts & Assumptions

Given: The complete ordered field $R$ , the canonical embedding $ι : Q \to R$ , the abbreviation $2 : = 1 + 1$ in each of the two fields, and the set $S : = {q \in Q : q > 0 and q^{2} < 2}$ , regarded as a subset of $Q$ and, through $ι$ , as the subset $ι (S)$ of $R$ . "Upper bound of $S$ in $Q$ " means an element $u \in Q$ with $q \leq u$ for every $q \in S$ , and "supremum of $S$ in $Q$ " means such a $u$ that is $\leq$ every upper bound of $S$ in $Q$ .

[L1]

Square roots: every $a \geq 0$ in $R$ has a unique $s \geq 0$ with $s^{2} = a$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L2]

Squaring is strictly monotone on the nonnegatives: for $a, b \geq 0$ in $R$ one has $a < b$ if and only if $a^{2} < b^{2}$ (Squaring is monotone on the nonnegatives).

[L3]

The embedding: $ι$ is the unique field homomorphism $Q \to R$ ; it is injective and order preserving, so $ι (q + r) = ι (q) + ι (r)$ , $ι (q r) = ι (q) ι (r)$ , $ι (1) = 1$ and $q < r$ implies $ι (q) < ι (r)$ . It also reflects the order: if $ι (q) < ι (r)$ then $q < r$ , since $r \leq q$ would give $ι (r) \leq ι (q)$ by order preservation and injectivity, contradicting trichotomy (The unique embedding of ℚ into an ordered field, Ordered field).

[L4]

Density: $R$ is Archimedean, being a complete ordered field, and its rationals are dense in it, so for $x < y$ in $R$ there is $q \in Q$ with $x < ι (q) < y$ (Every complete ordered field is Archimedean, Archimedean ordered field, ℚ is dense in every Archimedean ordered field).

[L5]

The claim that there exists $x \in Q$ with $x^{2} = 2$ is false (FALSE: some rational number squares to 2).

[L6]

Epsilon characterisation of the supremum: for a nonempty $X \subseteq R$ bounded above and an upper bound $w$ of $X$ , one has $w = \sup X$ if and only if for every $ε > 0$ there is $x \in X$ with $w - ε < x$ (Epsilon characterisation of the supremum).

[L7]

Every set ${a, b}$ of two reals has a maximum, which is one of the two entries and dominates both (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L8]

Order and least upper bounds: $0 < 1$ , hence $2 = 1 + 1 > 1 > 0$ in both fields; trichotomy holds, so the negation of $a \leq b$ is $b < a$ ; the order is transitive; adding a constant preserves it; multiplication distributes over addition, so $2 \cdot 2 = 2 + 2$ ; $0 \cdot a = 0$ for every $a$ , so $0^{2} = 0$ (Multiplication by zero: $0 \cdot a = 0$ ); and a least upper bound is an upper bound that is $\leq$ every upper bound (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Complete ordered field (least-upper-bound property), Ordered field, Field).

Verification

technique · direct

1.1

In $R$ we have $2 = 1 + 1 > 0$ , so [L1] supplies a unique $r \geq 0$ with $r^{2} = 2$ ; and $r \neq 0$ because $r = 0$ would give $r^{2} = 0 \neq 2$ , so $r > 0$ . Write $r = : \sqrt{2}$ .

L1L8choose

1.2

$S$ is nonempty: the rational $1$ satisfies $1 > 0$ and $1^{2} = 1 < 2$ , so $1 \in S$ .

1.3

Let $u \in Q$ be an arbitrary upper bound of $S$ in $Q$ , that is, $q \leq u$ for every $q \in S$ .

assume-hyp

1.4

Let $ε > 0$ in $R$ be arbitrary.

assume-hyp

1.5

The rational $2$ is an upper bound of $S$ in $Q$ , so $S$ is bounded above there: for $q \in S$ order preservation gives $ι (q) > 0$ and $ι (q)^{2} = ι (q^{2}) < ι (2) = 2 < 2 + 2 = 2 \cdot 2 = ι (2)^{2}$ , whence $ι (q) < ι (2)$ by [L2] and $q < 2$ by order reflection.

L2L3L8

2.1

$r$ is an upper bound of $ι (S)$ in $R$ : for $q \in S$ order preservation gives $ι (q) > 0$ and $ι (q)^{2} = ι (q^{2}) < ι (2) = 2 = r^{2}$ , so $ι (q) < r$ by [L2], hence $ι (q) \leq r$ .

step 1.1L2L3L8

2.2

$r$ is not the image of any rational: if $r = ι (q)$ then $ι (q^{2}) = ι (q)^{2} = r^{2} = 2 = ι (2)$ , so $q^{2} = 2$ by injectivity of $ι$ , which [L5] forbids.

step 1.1L3L5

2.3

Put $a_{ε} : = \max {0, r - ε}$ , which exists by [L7]; then $0 \leq a_{ε}$ , and $a_{ε} < r$ because $a_{ε}$ is one of the two entries $0$ and $r - ε$ , of which the first is $< r$ by 1.1 and the second is $< r$ because $ε > 0$ .

step 1.1step 1.4L7L8choose

2.4

The image $ι (u)$ of the bound $u$ is an upper bound of $ι (S)$ in $R$ : for $q \in S$ the inequality $q \leq u$ in $Q$ gives $ι (q) \leq ι (u)$ by order preservation.

step 1.3L3

3.1

Density applied to $a_{ε} < r$ produces a rational $q_{ε}$ with $a_{ε} < ι (q_{ε}) < r$ ; then $ι (q_{ε}) > a_{ε} \geq 0$ forces $q_{ε} > 0$ by order reflection, and $0 \leq ι (q_{ε}) < r$ gives $ι (q_{ε}^{2}) = ι (q_{ε})^{2} < r^{2} = 2 = ι (2)$ by [L2], hence $q_{ε}^{2} < 2$ in $Q$ ; so $q_{ε} \in S$ and $r - ε \leq a_{ε} < ι (q_{ε})$ .

step 2.3step 1.1L4L2L3

4.1

The set $ι (S)$ is nonempty and bounded above in $R$ by $r$ , and for every $ε > 0$ its element $ι (q_{ε})$ satisfies $r - ε < ι (q_{ε})$ ; the epsilon characterisation therefore gives $\sup ι (S) = r = \sqrt{2}$ .

step 1.2step 2.1step 3.1L6

5.1

Since $r$ is the least upper bound of $ι (S)$ and $ι (u)$ is an upper bound of it, we get $r \leq ι (u)$ ; and $r \neq ι (u)$ by 2.2, so $r < ι (u)$ .

step 4.1step 2.4step 2.2L8

6.1

Density applied to $r < ι (u)$ produces a rational $v$ with $r < ι (v) < ι (u)$ ; every $q \in S$ satisfies $ι (q) \leq r < ι (v)$ , so $q < v$ by order reflection and $v$ is an upper bound of $S$ in $Q$ ; and $v < u$ , again by order reflection. Hence $u$ is not $\leq$ every upper bound of $S$ in $Q$ , so $u$ is not a supremum of $S$ in $Q$ .

step 5.1step 2.1L4L3L8

7.1

The upper bound $u$ was an arbitrary one, so no upper bound of $S$ in $Q$ is least: $S$ has a supremum in $R$ , equal to $\sqrt{2}$ , and has no supremum in $Q$ even though it is nonempty and bounded above there, for instance by $2$ .

step 6.1step 4.1step 1.5L8∎

Remarks

The set $S$ is bounded above in $Q$ , by $2$ , as step 1.5 checks. Both hypotheses of the least-upper-bound property are therefore satisfied inside $Q$ , and the conclusion still fails. The property is a genuine assumption about the field, not a consequence of the order axioms alone.
The proof of leastness uses density twice, once to find an element of $S$ close below $\sqrt{2}$ and once to squeeze a rational between $\sqrt{2}$ and a putative rational least upper bound. Both uses go through ℚ is dense in every Archimedean ordered field, which is itself a consequence of the Archimedean property (Every complete ordered field is Archimedean).
The same argument runs with $2$ replaced by any positive rational $c$ that is not the square of a rational, once its two numerical steps are readjusted: step 1.2 must exhibit a positive rational whose square lies below $c$ , and step 1.5 a positive rational whose square lies above it, neither of which is the constant $1$ or $2$ in general. Both exist for every positive rational $c$ , and uniformly, so nothing here depends on $c$ being convenient: take $p : = c / (1 + c)$ and $w : = 1 + c$ , both positive rationals. Then $p^{2} < c$ , since $p^{2} < c$ is equivalent to $c^{2} < c (1 + c)^{2}$ and hence, dividing by $c > 0$ , to $c < (1 + c)^{2} = 1 + 2 c + c^{2}$ , which holds because $1 + c + c^{2} > 0$ ; and $w^{2} = 1 + 2 c + c^{2} > c$ for the same reason. Everything after those two steps is unchanged, so the failure is pervasive rather than a curiosity attached to $\sqrt{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

Least-upper-bound property (Wikipedia) (standard reference, not scraped)
Square root of 2 (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed. (standard reference, not scraped)
MIT 18.100A, Complete Lecture Notes (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

sup⁡{q∈Q:q>0, q2<2}=2sup{q∈Q:q>0, q2<2}=2​ in RR, and no supremum in QQ