Alphabeta Math
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.

✓ 28 results · all verified · 17 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 11 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Construction of the Real Numbers via Dedekind Cuts

1 · Prerequisites

2 · Summary

Objective. This page constructs the real number field R via Dedekind cuts and proves that R is a totally ordered field with the least-upper-bound property. The natural numbers N, with their arithmetic and order, are the assumed starting point.

Foundations (N to Q). The construction of the integers and the rationals is shared verbatim with the Cauchy-sequence construction, so we take it as given: Z is built from N as a totally ordered commutative ring (The integers form a totally ordered ring), and Q from Z as a totally ordered, Archimedean field (The rationals form a totally ordered field, The rationals are Archimedean). Only the final passage from Q to R differs between the two constructions, and it is the subject of this page.

The gap in Q. Order-completeness fails in Q: the set {q:q2<2} is bounded above yet has no rational least upper bound. A Dedekind cut fills exactly such a gap, naming the missing bound by the rationals that lie below it.

Cuts and the reals. A Dedekind cut is a subset A⊆Q that is nonempty and proper, downward closed, and without a greatest element (Dedekind cut): the set of all rationals lying strictly below a point of the line. The reals are defined to be the set of all cuts (The real numbers R as Dedekind cuts), ordered simply by inclusion (Order on the Dedekind reals), which is a total order (Inclusion totally orders the Dedekind reals).

Arithmetic. Addition is the sumset A+B, with a subtle additive inverse −A chosen so that A+(−A)=0∗ (Addition, negation, and subtraction of Dedekind cuts, For a cut A, −A is a cut and A+(−A)=0∗). Multiplication is defined first on the nonnegative cuts and then extended by signs (Multiplication and reciprocals of Dedekind cuts, For a positive cut A, the reciprocal A−1 satisfies A⋅A−1=1∗). These operations make R a field (The Dedekind reals form a field) into which Q embeds densely, preserving sums, products, 0, 1 and the order (The rational cuts embed densely in R, preserving sums, products, 0, 1 and the order).

Order. Inclusion makes this field totally ordered (The Dedekind reals form a totally ordered field) and Archimedean (The Dedekind reals are Archimedean), so the rational cuts stay cofinal in R.

Destination. R is order-complete: every nonempty set of cuts bounded above has a least upper bound, obtained as nothing more than the union of the cuts (Dedekind completeness: the least-upper-bound property). This least-upper-bound property is the payoff of the construction, the order-theoretic counterpart of the Cauchy completeness delivered by the sequence construction (The reals are complete). It is also what a cut was designed to supply: each cut simply is the supremum of the rationals beneath it, so the holes in Q are filled once and for all.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The integers as equivalence classes of pairs of naturals

Definition

On the set N×N of pairs of natural numbers, define

(a,b)∼(c,d)  ⟺  a+d=b+c.

This is an equivalence relation (The integer-defining relation is an equivalence relation ↗). The integers are the quotient

Z:=(N×N)/∼,

and we write [(a,b)] for the equivalence class of (a,b).

Remarks

  • The pair (a,b) encodes the formal difference a−b; the defining relation a+d=b+c is the equation "a−b=c−d" restated using only addition, which is all N has.
  • N and its arithmetic (commutativity, associativity, distributivity, cancellation of addition, the order) are taken as given background throughout this construction.
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The integer-defining relation is an equivalence relation

Statement

The relation (a,b)∼(c,d)  ⟺  a+d=b+c on N×N (The integers as equivalence classes of pairs of naturals) is an equivalence relation.

Facts & Assumptions

Given: The relation (a,b)∼(c,d)  ⟺  a+d=b+c on N×N.

[A1]

Addition on N is commutative and associative.

[A2]

Cancellation in N: if x+z=y+z then x=y.

Proof

technique · direct
1.1

Reflexivity: for any (a,b) we have a+b=b+a, so (a,b)∼(a,b).

A1
1.2

Symmetry: suppose (a,b)∼(c,d), i.e. a+d=b+c. Then c+b=d+a, which is the defining equation for (c,d)∼(a,b).

A1
1.3

Suppose (a,b)∼(c,d) and (c,d)∼(e,f), i.e. a+d=b+c and c+f=d+e.

given
2.1

Adding the two equations: (a+d)+(c+f)=(b+c)+(d+e).

step 1.3algebra
3.1

Regrouping both sides: (a+f)+(c+d)=(b+e)+(c+d).

step 2.1A1
4.1

Cancelling (c+d): a+f=b+e, so (a,b)∼(e,f); the relation is transitive.

step 3.1A2
5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Arithmetic on the integers

Definition

On Z (The integers as equivalence classes of pairs of naturals) define, on representatives,

[(a,b)]+[(c,d)]:=[(a+c,  b+d)], [(a,b)]⋅[(c,d)]:=[(ac+bd,  ad+bc)], −[(a,b)]:=[(b,a)],0:=[(0,0)],1:=[(1,0)].

These do not depend on the chosen representatives (Integer addition and negation are well defined ↗, Integer multiplication is well defined ↗).

Remarks

  • The product formula is forced by the intended meaning: if (a,b) stands for a−b and (c,d) for c−d, then (a−b)(c−d)=(ac+bd)−(ad+bc).
  • Negation swaps the components: −(a−b)=b−a.
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Integer addition and negation are well defined

Statement

The operations [(a,b)]+[(c,d)]=[(a+c,b+d)] and −[(a,b)]=[(b,a)] on Z (Arithmetic on the integers) are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)∼(a′,b′) and (c,d)∼(c′,d′) in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N is commutative and associative.

Proof

technique · direct
1.1

By hypothesis a+b′=b+a′.

given
1.2

By hypothesis c+d′=d+c′.

given
2.1

Adding the two equations: (a+b′)+(c+d′)=(b+a′)+(d+c′).

step 1.1step 1.2algebra
2.2

Commuting the equation of step 1.1: b+a′=a+b′, which is the defining equation for (b,a)∼(b′,a′); negation is well defined.

step 1.1A1
3.1

Regrouping both sides: (a+c)+(b′+d′)=(b+d)+(a′+c′), which is the defining equation for (a+c, b+d)∼(a′+c′, b′+d′); addition is well defined.

step 2.1A1
4.1

Both operations are independent of representatives.

step 3.1step 2.2∎
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Integer multiplication is well defined

Statement

The operation [(a,b)]⋅[(c,d)]=[(ac+bd, ad+bc)] on Z (Arithmetic on the integers) is independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)∼(a′,b′) and (c,d)∼(c′,d′) in the sense of The integers as equivalence classes of pairs of naturals.

[A1]

Addition on N is commutative and associative.

[A2]

Multiplication on N is commutative.

[A3]

Distributivity in N: x(y+z)=xy+xz.

Proof

technique · direct
1.1

By hypothesis a+b′=b+a′; write s for this common value.

given
1.2

Regrouping and factoring: (ac+bd)+(a′d+b′c)=c(a+b′)+d(b+a′).

A1A2A3
1.3

Regrouping and factoring: (ad+bc)+(a′c+b′d)=d(a+b′)+c(b+a′).

A1A2A3
2.1

By step 1.1 both right-hand sides equal cs+ds, so (ac+bd)+(a′d+b′c)=(ad+bc)+(a′c+b′d).

step 1.1step 1.2step 1.3
3.1

That equation is precisely the defining relation (ac+bd, ad+bc)∼(a′c+b′d, a′d+b′c): the product class is unchanged when the first factor's representative changes.

step 2.1
4.1

The product formula is symmetric in its two arguments: swapping (a,b)↔(c,d) sends (ac+bd, ad+bc) to (ca+db, cb+da), the same pair. Hence, by the argument of steps 1.1–3.1 applied to the second factor, the product class is also unchanged when (c,d) is replaced by (c′,d′).

step 3.1A1A2
5.1

Replacing first (a,b) by (a′,b′) and then (c,d) by (c′,d′): [(a,b)]⋅[(c,d)]=[(a′,b′)]⋅[(c,d)]=[(a′,b′)]⋅[(c′,d′)]; multiplication is well defined.

step 3.1step 4.1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The integers form a commutative ring

Statement

(Z,+,⋅,0,1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, in which every element has the additive inverse −[(a,b)]=[(b,a)].

Facts & Assumptions

Given: Z with the operations of Arithmetic on the integers.

[L1]

Addition on N is commutative and associative, with zero as a two-sided identity (Addition is commutative, Addition is associative, Left identity for addition).

[L2]

Multiplication on N is commutative and associative, distributes over addition, and has the usual zero and identity laws (Multiplication is commutative, Multiplication is associative, Distributivity and the successor law for multiplication, Zero and one under multiplication).

[L3]

The integer operations are independent of representatives (Integer addition and negation are well defined, Integer multiplication is well defined).

Proof

technique · direct
1.1

By [L3], each axiom may be verified on arbitrary fixed representatives (a,b),(c,d),(e,f).

L3suffices
1.2

Associativity of +: ((a,b)+(c,d))+(e,f) and (a,b)+((c,d)+(e,f)) both equal (a+c+e,  b+d+f).

L1
1.3

Commutativity of +: (a+c, b+d)=(c+a, d+b).

L1
1.4

Additive identity: (a,b)+(0,0)=(a+0, b+0)=(a,b).

L1
1.5

Additive inverses: (a,b)+(b,a)=(a+b, b+a)∼(0,0), since (a+b)+0=(b+a)+0.

L1
1.6

Commutativity of ⋅: swapping (a,b)↔(c,d) sends (ac+bd, ad+bc) to (ca+db, cb+da), the same pair.

L1L2
1.7

Multiplicative identity: (a,b)⋅(1,0)=(a⋅1+b⋅0,  a⋅0+b⋅1)=(a,b).

L1L2
1.8

Associativity of ⋅: expanding, both ((a,b)(c,d))(e,f) and (a,b)((c,d)(e,f)) equal (ace+adf+bcf+bde,  acf+ade+bce+bdf).

L1L2
1.9

Distributivity: (a,b)⋅((c,d)+(e,f))=(a(c+e)+b(d+f),  a(d+f)+b(c+e))=(ac+bd, ad+bc)+(ae+bf, af+be)=(a,b)(c,d)+(a,b)(e,f).

L1L2
2.1

Steps 1.2–1.9 verify all axioms: (Z,+,⋅,0,1) is a commutative ring with identity and additive inverses.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8step 1.9∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the integers

Definition

For integers x=[(a,b)] and y=[(c,d)] (The integers as equivalence classes of pairs of naturals) define

x≤y  ⟺  a+d≤b+cin N.

Write x<y when x≤y and x≠y. An integer x is positive when 0<x; on representatives, 0<[(a,b)] exactly when b<a.

Remarks

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The integers form a totally ordered ring

Statement

The relation of Order on the integers is well defined and is a total order on Z; it is compatible with addition (x≤y implies x+z≤y+z) and positives are closed under multiplication (0<x and 0<y imply 0<xy). Thus Z is a totally ordered commutative ring.

Facts & Assumptions

Given: Integers x=[(a,b)], y=[(c,d)], z=[(e,f)] with the operations of Arithmetic on the integers.

[L1]

Addition on N is commutative and associative (Addition is commutative, Addition is associative).

[L2]

The order on N is total, antisymmetric, and transitive (≤ is a linear order on N).

[L3]

Natural order is translation-invariant: x≤y  ⟺  x+z≤y+z (Order is compatible with addition).

[L4]

By the definition of natural order, x≤y exactly when y=x+k for some natural k; if x<y, such a gap is nonzero (Order on the natural numbers).

[L5]

Natural multiplication is commutative and associative, distributes over addition, and has the usual zero and identity laws; multiplication by a nonzero natural preserves strict order (Multiplication is commutative, Multiplication is associative, Distributivity and the successor law for multiplication, Zero and one under multiplication, Order is compatible with multiplication).

[L6]

The integer operations make Z a commutative ring with multiplicative identity (The integers form a commutative ring).

Proof

technique · direct
1.1

Suppose (a,b)∼(a′,b′) and (c,d)∼(c′,d′), i.e. a+b′=b+a′ and c+d′=d+c′.

given
1.2

Suppose a+d≤b+c.

given
1.3

Totality: in N either a+d≤b+c or b+c≤a+d, so x≤y or y≤x.

L2
1.4

Antisymmetry: x≤y and y≤x give a+d≤b+c and b+c≤a+d, hence a+d=b+c, which is x=y as classes.

L2
1.5

Transitivity: from a+d≤b+c and c+f≤d+e, adding gives (a+d)+(c+f)≤(b+c)+(d+e); regrouping, (a+f)+(c+d)≤(b+e)+(c+d); cancelling, a+f≤b+e, i.e. x≤z.

L1L2L3
1.6

Compatibility with addition: x+z≤y+z reads (a+e)+(d+f)≤(b+f)+(c+e), which regroups to (a+d)+(e+f)≤(b+c)+(e+f), equivalent to a+d≤b+c, i.e. x≤y.

L1L3
1.7

Suppose 0<x and 0<y, i.e. b<a and d<c.

given
2.1

Adding (a′+d′): (a+d)+(a′+d′)≤(b+c)+(a′+d′).

step 1.2L3
2.2

Regrouping with the equations of step 1.1: (b+c)+(a′+d′)=(b+a′)+(c+d′)=(a+b′)+(d+c′)=(a+d)+(b′+c′).

step 1.1L1
2.3

Write a=b+k and c=d+m with nonzero naturals k,m.

step 1.7L4
3.1

So (a+d)+(a′+d′)≤(a+d)+(b′+c′); cancelling (a+d) gives a′+d′≤b′+c′. Applying the same argument with primed and unprimed representatives exchanged proves the converse implication, so the relation is independent of representatives.

step 1.1step 2.1step 2.2L3
3.2

Expanding both components of xy=[(ac+bd, ad+bc)]: ac+bd=(b+k)(d+m)+bd=(bd+bm+kd+bd)+km and ad+bc=(b+k)d+b(d+m)=bd+kd+bd+bm, so ac+bd=(ad+bc)+km.

step 2.3L1L5
4.1

Since k,m are nonzero, 0<k and 0<m by [L4]. Hence [L5] gives 0=0⋅m<km, and step 3.2 yields ad+bc<ac+bd, which is 0<xy.

step 2.3step 3.2L2L4L5
5.1

The order is well defined, total, compatible with addition, and positives are closed under multiplication; together with [L6], this makes Z a totally ordered commutative ring.

step 3.1step 1.3step 1.4step 1.5step 1.6step 4.1L6∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The integers have no zero divisors; multiplicative cancellation

Statement

If x,y∈Z are nonzero then xy≠0. Consequently, if xz=yz and z≠0, then x=y.

Facts & Assumptions

Given: Nonzero integers x,y.

[L1]

Z is a totally ordered ring; in particular trichotomy holds (each integer is negative, zero, or positive) and positives are closed under multiplication (The integers form a totally ordered ring).

[L2]

Ring arithmetic in Z: (−u)v=−(uv), −(−u)=u, and distributivity (The integers form a commutative ring).

Proof

technique · cases
1.1

By trichotomy, each of x and y is positive or negative; split on the sign pattern.

L1cases-exhaustive
1.2

Case both positive: 0<xy by closure of positives, so xy≠0.

assume-case bothL1
1.3

Case exactly one negative, say y<0 (the other case is identical by commutativity): 0<−y, so 0<x(−y)=−(xy), hence xy<0 and xy≠0.

assume-case mixedL1L2
1.4

Case both negative: 0<−x and 0<−y, so 0<(−x)(−y)=xy, and xy≠0.

assume-case negnegL1L2
2.1

In every case xy≠0: the product of nonzero integers is nonzero.

step 1.2step 1.3step 1.4cases
3.1

Cancellation: if xz=yz with z≠0, then (x−y)z=xz−yz=0; were x−y≠0, the product would be nonzero, so x−y=0, i.e. x=y.

step 2.1L2∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The naturals embed in the integers

Statement

The map ι(n)=[(n,0)] is injective and preserves addition, multiplication, and order. Its image is exactly the set of nonnegative integers, so every x≥0 in Z is ι(k) for a unique natural k.

Facts & Assumptions

Given: The map ι:N→Z, ι(n)=[(n,0)].

[A1]

Arithmetic identities in N: x+0=x, 0+x=x, x⋅0=0, 0⋅x=0, x⋅1=x.

[A2]

The order on N, and: x≤y iff y=x+k for some k.

Proof

technique · direct
1.1

Injectivity: [(m,0)]=[(n,0)] means m+0=0+n, i.e. m=n.

A1
1.2

Addition: ι(m)+ι(n)=[(m+n, 0+0)]=ι(m+n).

A1
1.3

Multiplication: ι(m) ι(n)=[(mn+0⋅0,  m⋅0+0⋅n)]=ι(mn).

A1
1.4

Order: ι(m)≤ι(n) reads m+0≤0+n, i.e. m≤n.

A1A2
1.5

Image: if 0≤[(a,b)] then b≤a, so a=b+k and (a,b)∼(k,0), giving [(a,b)]=ι(k); conversely 0≤ι(k) for every k.

A2algebra
2.1

ι embeds N into Z, preserving arithmetic and order, with image the nonnegative integers.

step 1.1step 1.2step 1.3step 1.4step 1.5∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

The rationals as equivalence classes of pairs of integers

Definition

On the set of pairs (a,b) with a,b∈Z and b≠0, define

(a,b)∼(c,d)  ⟺  ad=cbin Z.

This is an equivalence relation (The rational-defining relation is an equivalence relation ↗). The rationals are the quotient Q, and [(a,b)] is written a/b.

Remarks

  • The pair (a,b) encodes the formal quotient a/b; the relation ad=cb is "a/b=c/d" cleared of denominators, using only the ring arithmetic of Z (The integers form a commutative ring).
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rational-defining relation is an equivalence relation

Statement

The relation (a,b)∼(c,d)  ⟺  ad=cb on pairs of integers with nonzero second component (The rationals as equivalence classes of pairs of integers) is an equivalence relation.

Facts & Assumptions

Given: Pairs (a,b),(c,d),(e,f) of integers with b,d,f≠0.

[L1]

Z is a commutative ring (The integers form a commutative ring).

[L2]

Multiplicative cancellation in Z: ud=vd with d≠0 implies u=v (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct
1.1

Reflexivity: ab=ba, so (a,b)∼(a,b).

L1
1.2

Symmetry: if ad=cb then cb=ad, which is the defining equation for (c,d)∼(a,b).

L1
1.3

Suppose (a,b)∼(c,d) and (c,d)∼(e,f), i.e. ad=cb and cf=ed.

given
2.1

Multiplying the first equation by f and the second by b: adf=cbf and cfb=edb.

step 1.3L1
3.1

Chaining: (af)d=adf=cbf=cfb=edb=(eb)d.

step 2.1L1
4.1

Cancelling the nonzero d: af=eb, so (a,b)∼(e,f); the relation is transitive.

step 3.1L2
5.1

The relation is reflexive, symmetric, and transitive, hence an equivalence relation.

step 1.1step 1.2step 4.1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-07-24Open item page →

Arithmetic on the rationals

Definition

On Q (The rationals as equivalence classes of pairs of integers) define, on representatives,

[(a,b)]+[(c,d)]:=[(ad+cb,  bd)],[(a,b)]⋅[(c,d)]:=[(ac,  bd)], −[(a,b)]:=[(−a,b)],0:=[(0,1)],1:=[(1,1)],

and, for [(a,b)]≠0 (equivalently a≠0), the inverse [(a,b)]−1:=[(b,a)].

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

Rational arithmetic is well defined

Statement

Sum, product, and negation of Arithmetic on the rationals are independent of the chosen representatives.

Facts & Assumptions

Given: Pairs with (a,b)∼(a′,b′) and (c,d)∼(c′,d′) (The rationals as equivalence classes of pairs of integers), all second components nonzero.

[L1]

Z is a commutative ring (The integers form a commutative ring).

Proof

technique · direct
1.1

By hypothesis ab′=a′b and cd′=c′d.

given
2.1

Product: (ac)(b′d′)=(ab′)(cd′)=(a′b)(c′d)=(a′c′)(bd), so (ac, bd)∼(a′c′, b′d′).

step 1.1L1
2.2

Sum: (ad+cb)(b′d′)=(ab′)(dd′)+(cd′)(bb′)=(a′b)(dd′)+(c′d)(bb′)=(a′d′+c′b′)(bd), so (ad+cb, bd)∼(a′d′+c′b′, b′d′).

step 1.1L1
2.3

Negation: from ab′=a′b, (−a)b′=(−a′)b, so (−a,b)∼(−a′,b′).

step 1.1L1
3.1

All three operations are independent of representatives.

step 2.1step 2.2step 2.3∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The reciprocal on the rationals is well-defined

Statement

On Q∖{0} the reciprocal [(a,b)]−1:=[(b,a)] (Arithmetic on the rationals) is independent of the chosen representative: if (a,b)∼(a′,b′) with a,a′,b,b′≠0, then (b,a)∼(b′,a′). Hence the reciprocal is a well-defined function on Q∖{0}.

Facts & Assumptions

Given: Nonzero rationals represented by integer pairs (a,b) and (a′,b′) with a,a′,b,b′≠0, where (x,y)∼(z,w)  ⟺  xw=zy in Z (The rationals as equivalence classes of pairs of integers).

[L1]

Multiplication in Z is commutative (The integers form a commutative ring).

Proof

technique · direct
1.1

By hypothesis (a,b)∼(a′,b′), that is ab′=a′b in Z.

given
2.1

Commuting each product by [L1], b′a=ba′, hence ba′=b′a.

step 1.1L1
3.1

The equation ba′=b′a is exactly the defining relation (b,a)∼(b′,a′), and since a,a′≠0 the pairs (b,a),(b′,a′) are legal rational representatives; therefore [(a,b)]−1=[(b,a)]=[(b′,a′)]=[(a′,b′)]−1, so the reciprocal is well-defined on Q∖{0}.

step 2.1given∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rationals form a field

Statement

(Q,+,⋅,0,1) with the operations of Arithmetic on the rationals is a field: a commutative ring with 1≠0 in which every nonzero element has a multiplicative inverse.

Facts & Assumptions

Given: Rationals with representatives (a,b),(c,d),(e,f), second components nonzero.

[L1]

The operations are independent of representatives (Rational arithmetic is well defined).

[L2]

Z is a commutative ring in which 1≠0 (The integers form a commutative ring; 1≠0 because 1≠0 in N).

[L3]

Z has no zero divisors and admits cancellation (The integers have no zero divisors; multiplicative cancellation).

Proof

technique · direct
1.1

By [L1], each axiom may be verified on fixed representatives.

L1suffices
1.2

Associativity of +: both ((a,b)+(c,d))+(e,f) and (a,b)+((c,d)+(e,f)) have representative (adf+cbf+ebd,  bdf).

L2
1.3

Commutativity of +: (ad+cb, bd) and (cb+ad, db) are equal pairs.

L2
1.4

Additive identity: (a,b)+(0,1)=(a⋅1+0⋅b,  b⋅1)=(a,b).

L2
1.5

Additive inverses: (a,b)+(−a,b)=(ab−ab,  b2)=(0,b2)∼(0,1).

L2
1.6

Associativity and commutativity of ⋅: ((ac)e, (bd)f)=(a(ce), b(df)) and (ac, bd)=(ca, db).

L2
1.7

Multiplicative identity: (a,b)(1,1)=(a,b); and 1≠0 since 1⋅1≠0⋅1.

L2
1.8

Distributivity: (a,b)((c,d)+(e,f)) has representative (a(cf+ed),  b(df)), while (a,b)(c,d)+(a,b)(e,f) has representative (acbf+aebd,  b2df)=(b(acf+aed),  b(bdf)); cancelling the common nonzero factor b these are equivalent.

L2L3
1.9

Inverses: [(a,b)]=0 iff a⋅1=0⋅b iff a=0; for a≠0, (a,b)(b,a)=(ab, ba)∼(1,1).

L2
2.1

All field axioms hold: Q is a field.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6step 1.7step 1.8step 1.9∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-24Open item page →

Order on the rationals

Definition

Every rational has a representative with positive denominator (if b<0 then (a,b)∼(−a,−b) with −b>0, Every rational has a positive-denominator representative ↗). For representatives with b>0 and d>0 define

[(a,b)]≤[(c,d)]  ⟺  ad≤cbin Z.

A rational x is positive when 0<x; on such representatives, 0<[(a,b)] exactly when 0<a.

Remarks

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Every rational has a positive-denominator representative

Statement

Every rational has a representative (a,b) with b>0: for a class [(a,b)] (where b≠0), if b>0 take (a,b) itself, and if b<0 then (a,b)∼(−a,−b) with −b>0. Consequently the order on Q (Order on the rationals), which is stated on positive-denominator representatives, is defined on all of Q.

Facts & Assumptions

Given: A rational represented by (a,b) with a,b∈Z, b≠0, and the relation (x,y)∼(z,w)  ⟺  xw=zy (The rationals as equivalence classes of pairs of integers).

[L1]

Trichotomy in Z: each nonzero integer is either >0 or <0, and b<0 iff −b>0 (The integers form a totally ordered ring).

[L2]

In the commutative ring Z, a(−b)=−(ab)=(−a)b (both products are the additive inverse of ab, by distributivity) (The integers form a commutative ring).

Proof

technique · direct
1.1

Since b≠0, by trichotomy [L1] either b>0 or b<0.

givenL1
2.1

If b>0, the representative (a,b) already has positive denominator.

step 1.1
2.2

If b<0, then −b>0 by [L1], and a(−b)=(−a)b by [L2] is exactly the defining relation (a,b)∼(−a,−b); so (−a,−b) represents the same class and has positive denominator −b.

step 1.1L1L2
3.1

In either case the class has a representative with positive denominator; hence the order Order on the rationals, stated on such representatives, is defined for every rational.

step 2.1step 2.2∎
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The rationals form a totally ordered field

Statement

The relation of Order on the rationals is well defined and makes the field Q (The rationals form a field) a totally ordered field: the order is total, x≤y implies x+z≤y+z, and 0<x, 0<y imply 0<xy.

Facts & Assumptions

Given: Rationals x=[(a,b)], y=[(c,d)], z=[(e,f)] with b,d,f>0.

[L1]

Z is a totally ordered commutative ring; positives are closed under products (The integers form a totally ordered ring).

Proof

technique · direct
1.1

Order-scaling in Z: for p>0, if u<v then 0<(v−u)p, so up<vp; conversely if up≤vp and v<u then vp<up, impossible; hence u≤v iff up≤vp.

L1algebra
1.2

Suppose (a,b)∼(a′,b′) and (c,d)∼(c′,d′) with b′,d′>0, i.e. ab′=a′b and cd′=c′d; suppose also ad≤cb.

given
1.3

Totality: ad≤cb or cb≤ad in Z, so x≤y or y≤x.

L1
1.4

Antisymmetry: ad≤cb and cb≤ad give ad=cb, i.e. x=y as classes.

L1
1.5

Positive products: if 0<x and 0<y then 0<a and 0<c, so xy=[(ac, bd)] has ac>0 and bd>0, hence 0<xy.

L1
1.6

For transitivity, let z=[(e,f)] with f>0 and suppose additionally y≤z, i.e. cf≤ed.

given
2.1

Scaling the hypothesis ad≤cb by b′d′>0: (ad)(b′d′)≤(cb)(b′d′).

step 1.1step 1.2L1
2.2

Rearranging both sides with ab′=a′b and cd′=c′d: (ad)(b′d′)=(ab′)(dd′)=(a′b)(dd′)=(a′d′)(bd) and (cb)(b′d′)=(cd′)(bb′)=(c′d)(bb′)=(c′b′)(bd).

step 1.2L1
2.3

Transitivity: from ad≤cb and cf≤ed, scaling by f>0 and b>0 gives (af)d=(ad)f≤(cb)f=(cf)b≤(ed)b=(eb)d; cancelling d>0 via order-scaling, af≤eb, i.e. x≤z.

step 1.1step 1.2step 1.6L1
2.4

Compatibility with addition: x+z≤y+z reads (af+eb)(df)≤(cf+ed)(bf), which expands to (ad)f2+(eb)(df)≤(cb)f2+(ed)(bf); the second terms are equal, so this is (ad)f2≤(cb)f2, equivalent by order-scaling with f2>0 to ad≤cb, i.e. x≤y.

step 1.1L1
3.1

Combining: (a′d′)(bd)≤(c′b′)(bd) with bd>0, so a′d′≤c′b′ by order-scaling: the order is independent of representatives.

step 2.1step 2.2step 1.1L1
4.1

The order is well defined, total, compatible with addition, and positives are closed under multiplication: Q is a totally ordered field.

step 3.1step 1.3step 1.4step 2.3step 2.4step 1.5∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The integers embed in the rationals

Statement

The map j(k)=[(k,1)] is injective and preserves addition, multiplication, and order. Composing with The naturals embed in the integers embeds N in Q; we write k for j(k) throughout.

Facts & Assumptions

Given: The map j:Z→Q, j(k)=[(k,1)].

[L1]

Ring arithmetic in Z (The integers form a commutative ring).

[L2]

The order on Q (Order on the rationals), whose defining inequality is read in the order on Z (Order on the integers).

[L3]

Equality in Q: [(a,b)]=[(c,d)] iff ad=cb (The rationals as equivalence classes of pairs of integers).

Proof

technique · direct
1.1

Injectivity: (k,1)∼(m,1) means k⋅1=m⋅1, i.e. k=m.

L3L1
1.2

Addition: j(k)+j(m)=[(k⋅1+m⋅1,  1)]=j(k+m).

L1
1.3

Multiplication: j(k) j(m)=[(km, 1)]=j(km).

L1
1.4

Order: denominators are 1>0, so j(k)≤j(m) reads k⋅1≤m⋅1, i.e. k≤m.

L1L2
2.1

j embeds Z into Q, preserving arithmetic and order.

step 1.1step 1.2step 1.3step 1.4∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

The rationals are Archimedean

Statement

For every rational x there is a natural number n with x<n. Consequently, for every rational ε>0 there is a natural n≥1 with 1/n<ε.

Facts & Assumptions

Given: A rational x=[(a,b)] with b>0.

[L1]

The order and arithmetic of Q (The rationals form a totally ordered field).

[L2]

Integer facts: positive integers are exactly ι(m) with m≥1 natural; nonnegative integers are the image of N; the embeddings preserve arithmetic and order (The naturals embed in the integers, The integers embed in the rationals, The integers form a totally ordered ring).

Proof

technique · direct
1.1

Since b>0, b lies in the image of N and b≥1.

L2
1.2

If a≤0 set k=0; otherwise a is a positive integer, so a=ι(k) for some natural k≥1. In both cases a≤k (as integers).

L2
2.1

Then a<k+1 and, since b≥1 and k+1>0, also k+1≤(k+1)b.

step 1.1step 1.2L2
3.1

Hence a<(k+1)b, and dividing by b>0 (order-scaling in the definition of the rational order), x=[(a,b)]<[((k+1)b, b)]=k+1=:n.

step 2.1L1
4.1

For rational ε>0: apply the above to x=1/ε to get n with 1/ε<n, hence 1/n<ε.

step 3.1L1∎
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Dedekind cut

Definition

Work over the totally ordered field Q of rationals (The rationals as equivalence classes of pairs of integers, The rationals form a totally ordered field). A subset A⊆Q is a Dedekind cut iff it satisfies all three of:

  • (C1) A≠∅ and A≠Q (proper and nonempty);
  • (C2) downward closed: if p∈A and q<p, then q∈A;
  • (C3) no greatest element: if p∈A, then there exists r∈A with p<r.

Remarks

This is the lower-set convention (Rudin's): a cut is the set of rationals lying strictly below a real point, so it "opens downward" and never closes off at a maximum. Under the opposite (upper-set) convention the inequalities are reversed; we fix the lower-set form throughout.

An equivalent phrasing of (C2) by contraposition: if q∉A and q<p, then p∉A; the complement Q∖A is upward closed. Consequently every a∈A and b∉A satisfy a<b: were b≤a, downward closure (C2) would place b∈A. Thus a cut splits Q into a lower piece A and an upper piece Q∖A with every element of the former below every element of the latter, the lower piece having no largest member.

The set of all Dedekind cuts is the carrier of the real numbers (The real numbers R as Dedekind cuts); each cut is a real number, identified with the downward gap of rationals it names.

DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-08-02 (claude-opus-5)Open item page →

The real numbers R as Dedekind cuts

Definition

The real numbers are defined to be the set of all Dedekind cuts of Q (Dedekind cut): R:={ A⊆Q:A is a Dedekind cut }. Elements of R are written A,B,C,…; each is a subset of Q satisfying (C1)–(C3).

The rationals embed into R by the rational embedding: for q∈Q set q∗:={ r∈Q:r<q }, the cut of all rationals strictly below q. Each q∗ is a Dedekind cut (Each rational cut q∗ is a Dedekind cut ↗), and q↦q∗ sends Q into R. The images of 0 and 1 are written 0∗ and 1∗; being cuts they lie in R and serve as its additive and multiplicative identities.

Remarks

A cut A is exactly the set of rationals lying below a putative real point; R is thus built by naming each point through the downward gap of rationals it determines. Where Q has a genuine rational point q, the cut q∗ recovers it, but the construction also admits cuts A with no largest excluded rational and no rational boundary at all, such as { q:q<0 or q2<2 }. These are precisely the missing limits of Q: the cut convention manufactures a real number wherever Q leaves a hole, which is why R is complete while Q is not.

The order on R is set inclusion, A≤B:⇔A⊆B (Order on the Dedekind reals). That q↦q∗ is an order-preserving ring embedding, and that its image is dense, is recorded in The rational cuts embed densely in R, preserving sums, products, 0, 1 and the order; the arithmetic and order structure making R a complete ordered field is developed in The Dedekind reals form a totally ordered field and Dedekind completeness: the least-upper-bound property.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Each rational cut q∗ is a Dedekind cut

Statement

For every q∈Q the set q∗={ r∈Q:r<q } (The real numbers R as Dedekind cuts) is a Dedekind cut (Dedekind cut). In particular 0∗ and 1∗ are Dedekind cuts, hence elements of R, so they are legitimate as the additive and multiplicative identities of R.

Facts & Assumptions

Given: A rational q and the set q∗={ r∈Q:r<q }, with the Dedekind-cut axioms (C1) proper and nonempty, (C2) downward closed, (C3) no greatest element (Dedekind cut).

[L1]

Q is a totally ordered field: < is transitive and total, q−1<q<q+1, and whenever p<q the midpoint p+q2 satisfies p<p+q2<q (The rationals form a totally ordered field).

Proof

technique · direct
1.1

(C1) q∗ is nonempty and proper: q−1<q gives q−1∈q∗, while q≮q gives q∉q∗, so q∗≠∅ and q∗≠Q.

givenL1
1.2

(C2) q∗ is downward closed: if p∈q∗, so p<q, and r<p, then r<q by transitivity, hence r∈q∗.

givenL1
1.3

(C3) q∗ has no greatest element: if p∈q∗ then p<q, so the midpoint m=p+q2 satisfies p<m<q, giving m∈q∗ with m>p.

givenL1
2.1

Satisfying (C1), (C2), (C3), q∗ is a Dedekind cut; applied at q=0 and q=1 this shows 0∗ and 1∗ are Dedekind cuts and hence elements of R.

step 1.1step 1.2step 1.3∎
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Order on the Dedekind reals

Definition

For Dedekind cuts A,B∈R (Dedekind cut, The real numbers R as Dedekind cuts), the order is set inclusion:

A≤B  ⟺  A⊆B,A<B  ⟺  A⊊B.

That is, A<B means A⊆B and A≠B.

A cut A is called positive iff 0∗<A, and nonnegative iff 0∗≤A, where 0∗={ r∈Q:r<0 } is the cut of 0. Negative and nonpositive cuts are defined symmetrically: A<0∗ and A≤0∗.

Remarks

Positivity has a convenient rational restatement: 0∗≤A iff every rational r<0 lies in A, and 0∗<A iff moreover 0∈A. Indeed if 0∈A then downward closure (C2) forces every r<0 into A, so 0∗⊆A and the inclusion is proper; conversely 0∗⊊A supplies some q∈A with q≥0, whence 0∈A by (C2). Thus a cut is positive exactly when it contains 0.

Inclusion is manifestly reflexive, antisymmetric, and transitive; what is not immediate is that it is total (any two cuts are comparable), which is Inclusion totally orders the Dedekind reals. Compatibility of this order with the field operations (translation invariance of ≤ and closure of nonnegatives under products), making R a totally ordered field, is The Dedekind reals form a totally ordered field.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

Inclusion totally orders the Dedekind reals

Statement

Set inclusion totally orders the Dedekind reals (Order on the Dedekind reals): the relation A≤B:⇔A⊆B on cuts (Dedekind cut) is reflexive, antisymmetric (with antisymmetry delivering set equality A=B), and transitive, and it is moreover total: for any two cuts A,B, either A⊆B or B⊆A.

Facts & Assumptions

Given: Dedekind cuts A,B∈R, ordered by inclusion (Order on the Dedekind reals).

[A1]

Set inclusion ⊆ is a partial order on any family of sets: reflexive (A⊆A), antisymmetric (mutual inclusion A⊆B, B⊆A gives A=B), and transitive.

[A2]

The order on Q is total (The rationals form a totally ordered field): for rationals x,y exactly one of x<y, x=y, y<x holds.

[L1]

Downward closure (C2): if p∈A and q<p then q∈A, and likewise for B (Dedekind cut).

Proof

technique · direct
1.1

The relation ≤ is set inclusion, and ⊆ is reflexive, antisymmetric (mutual inclusion A⊆B and B⊆A forces the set equality A=B), and transitive; hence ≤ is a partial order on R.

A1
1.2

It remains to establish totality. Fix cuts A,B; if A⊆B there is nothing to prove, so assume A⊈B. It suffices to show B⊆A.

suffices: B ⊆ A when A ⊄ B
2.1

Since A⊈B, choose a rational x with x∈A and x∉B.

step 1.2choose
3.1

Every y∈B satisfies y<x: otherwise x≤y by trichotomy, and then downward closure of B places x∈B (directly if x<y, or as x=y∈B), contradicting x∉B.

step 2.1L1A2
4.1

Fix any y∈B. From y<x together with x∈A, downward closure of A gives y∈A; as y∈B was arbitrary, B⊆A.

step 2.1step 3.1L1
5.1

Thus for all cuts A,B, A⊆B or B⊆A, so ≤ is total; combined with the partial-order properties, set inclusion is a total order on R.

step 1.1step 1.2step 4.1∎
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Addition, negation, and subtraction of Dedekind cuts

Definition

Let A,B∈R be Dedekind cuts of Q (Dedekind cut, The real numbers R as Dedekind cuts).

Sum. The sum is the Minkowski sumset in Q: A+B:={ a+b:a∈A, b∈B }.

Additive identity. 0∗:={ q∈Q:q<0 }, the cut of the rational 0 under the embedding q↦q∗={ r∈Q:r<q } (The real numbers R as Dedekind cuts).

Additive inverse. For a cut A, −A:={ p∈Q:∃ r∈Q, r>0, with −p−r∉A }. Equivalently, p∈−A iff there is a rational s∉A with s<−p (set s=−p−r; conversely r=−p−s>0). Intuitively −p is bounded away from A from below: some rational strictly beneath −p already fails to lie in A.

Subtraction. A−B:=A+(−B).

Remarks

The sum A+B is again a cut, and (R,+) is an abelian group with identity 0∗: closure, commutativity, associativity, and the identity law are Cut addition: A+B is a cut, commutative and associative, with identity 0∗, and existence of inverses is For a cut A, −A is a cut and A+(−A)=0∗.

The r>0 slack in the definition of −A is essential and is not cosmetic. Neither {−a:a∈A} nor {−a:a∉A} is a cut in general: the first need not be downward closed, and the second can acquire a greatest element. Excising the boundary rational (the "−p−r with r>0" clause) makes −A a genuine cut with no greatest element and forces the exact identity A+(−A)=0∗, not merely A+(−A)⊊0∗ (For a cut A, −A is a cut and A+(−A)=0∗).

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Cut addition: A+B is a cut, commutative and associative, with identity 0∗

Statement

For Dedekind cuts A,B, the sumset A+B={ a+b:a∈A, b∈B } (Addition, negation, and subtraction of Dedekind cuts) is again a Dedekind cut. Addition of cuts is commutative and associative, and 0∗={ q∈Q:q<0 } is a two-sided identity: A+0∗=A for every cut A.

Facts & Assumptions

Given: Dedekind cuts A,B,C; A+B:={ a+b:a∈A, b∈B } and 0∗:={ q∈Q:q<0 } (Addition, negation, and subtraction of Dedekind cuts).

[A1]

Cut axioms (C1)–(C3), and the restatement that for a∈A and b∉A one has a<b; the contrapositive of (C2): if x∉A and y>x then y∉A (Dedekind cut).

[L1]

Q is a commutative, associative, totally ordered field; in particular addition is commutative and associative and the order is translation-invariant (The rationals form a totally ordered field).

Proof

technique · direct
1.1

(C1) A+B is proper and nonempty: choosing a∈A, b∈B gives a+b∈A+B, so A+B≠∅; choosing a′∉A, b′∉B, every a∈A, b∈B satisfies a<a′ and b<b′, hence a+b<a′+b′, so a′+b′∉A+B and A+B≠Q.

A1L1
1.2

(C2) A+B is downward closed: if s=a+b∈A+B with a∈A, b∈B, and q<s, then q−a<b, so q−a∈B by (C2) for B; hence q=a+(q−a)∈A+B.

A1L1
1.3

(C3) A+B has no greatest element: given s=a+b∈A+B, (C3) for A yields a′∈A with a′>a, whence a′+b∈A+B and a′+b>a+b=s.

A1L1
1.4

Commutativity and associativity descend from Q: A+B={a+b}={b+a}=B+A, and (A+B)+C={(a+b)+c}={a+(b+c)}=A+(B+C).

L1
1.5

A+0∗⊆A: for a∈A and q∈0∗ (so q<0), a+q<a, hence a+q∈A by (C2).

A1L1
1.6

A⊆A+0∗: given a∈A, (C3) supplies r∈A with r>a; then a−r<0, so a−r∈0∗, and a=r+(a−r)∈A+0∗.

A1L1
2.1

A+B satisfies (C1)–(C3), so it is a Dedekind cut.

step 1.1step 1.2step 1.3A1
2.2

The two inclusions give the identity law A+0∗=A.

step 1.5step 1.6
3.1

Hence A+B is a cut, and cut addition is commutative and associative with two-sided identity 0∗.

step 2.1step 1.4step 2.2∎
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

For a cut A, −A is a cut and A+(−A)=0∗

Statement

For every Dedekind cut A, the set −A={ p∈Q:∃ r∈Q, r>0, −p−r∉A } (Addition, negation, and subtraction of Dedekind cuts) is again a Dedekind cut, and A+(−A)=0∗, where 0∗={ q∈Q:q<0 }. Thus every cut has an additive inverse and (R,+) is a group.

Facts & Assumptions

Given: A Dedekind cut A; −A:={ p∈Q:∃ r>0, −p−r∉A },  A+(−A):={ a+p:a∈A, p∈−A }, and 0∗:={ q∈Q:q<0 } (Addition, negation, and subtraction of Dedekind cuts).

[A1]

Cut axioms (C1)–(C3), and the restatement that for a∈A and b∉A one has a<b; the contrapositive of (C2): if x∉A and y>x then y∉A (Dedekind cut).

[A2]

A nonempty set K⊆Z with k<M for every k∈K, where M∈Z, has a greatest element: { M−k:k∈K } is then a nonempty set of positive integers, so it has a least element M−n by "every nonempty subset S⊆N has a least element" (The well-ordering principle), and that n is the greatest element of K.

[L1]

Q is Archimedean: for every rational x there is a natural number n with x<n (The rationals are Archimedean).

[L2]

Q is a totally ordered field; addition, negation, and scaling by positive rationals respect the order (The rationals form a totally ordered field).

[L3]

If A and −A are cuts then A+(−A) is a cut (Cut addition: A+B is a cut, commutative and associative, with identity 0∗).

Proof

technique · direct
1.1

(C1, nonempty) A≠Q, so pick s∉A; then p0:=−s−1 satisfies −p0−1=s∉A with witness r=1>0, so p0∈−A and −A≠∅.

A1choose
1.2

(C1, proper) A≠∅, so pick a∈A; then −a∉−A, for if −a∈−A there were r>0 with a−r=−(−a)−r∉A, yet a−r<a∈A forces a−r∈A by (C2), a contradiction. Hence −A≠Q.

A1L2
1.3

(C2, downward closed) If p∈−A with witness r>0 (so −p−r∉A) and q<p, then −q−r>−p−r, so −q−r∉A by the contrapositive of (C2); thus q∈−A with the same r.

A1L2
1.4

(C3, no greatest) If p∈−A with witness r>0, set t:=p+r/2>p; then −t−r/2=−p−r∉A, so t∈−A with witness r/2>0, and t>p.

A1L2
1.5

(A+(−A)⊆0∗) For a∈A and p∈−A with witness r>0: since −p−r∉A while a∈A, the restatement gives a<−p−r, so a+p<−r<0; hence a+p∈0∗.

A1L2
1.6

(setup) Fix v∈0∗ and put w:=−v/2, so w>0 since v<0; by (C1) choose a0∈A (as A≠∅) and b0∉A (as A≠Q).

A1L2choose
2.1

(−A is a cut) −A satisfies (C1)–(C3), so −A is a Dedekind cut.

step 1.1step 1.2step 1.3step 1.4A1
2.2

(bounded above) Apply [L1] to the rational b0/w: there is a natural M with b0/w<M, so b0<Mw since w>0; because b0∉A and Mw>b0, the contrapositive of (C2) gives Mw∉A, whence any k∈Z with kw∈A satisfies k<M (else k≥M gives kw≥Mw, so kw∉A by the contrapositive of (C2)), so K:={ k∈Z:kw∈A } is bounded above by M.

step 1.6L1L2A1
2.3

(nonempty) Apply [L1] to the rational −a0/w: there is a natural N with −a0/w<N, so −Nw<a0 since w>0; because a0∈A and −Nw<a0, (C2) gives −Nw∈A, so −N∈K and K≠∅.

step 1.6L1L2A1
3.1

(greatest element) K is a nonempty set of integers bounded above, so by [A2] it has a greatest element n; then nw∈A because n∈K, while n+1>n gives n+1∉K, i.e. (n+1)w∉A.

step 2.2step 2.3A2
4.1

(0∗⊆A+(−A)) With n from step 3.1, set p:=−(n+2)w; the witness r=w>0 gives −p−w=(n+1)w∉A, so p∈−A, while nw∈A, and nw+p=nw−(n+2)w=−2w=v. Hence v=nw+p∈A+(−A); as v∈0∗ was arbitrary, 0∗⊆A+(−A).

step 3.1A1L2
5.1

The inclusions of steps 1.5 and 4.1 give A+(−A)=0∗; with −A a cut (step 2.1) and A+(−A) therefore a cut [L3], A has additive inverse −A.

step 1.5step 4.1step 2.1L3∎
DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-02 (claude-opus-5)Open item page →

Multiplication and reciprocals of Dedekind cuts

Definition

Multiplication of Dedekind cuts (Dedekind cut, The real numbers R as Dedekind cuts) is defined first for nonnegative cuts, then extended to all cuts by their signs (Order on the Dedekind reals) via the absolute value.

Positive case. For cuts A,B>0∗ (strictly positive),

A⋅B:={ q∈Q:q≤0 }  ∪  { ab:a∈A, b∈B, a>0, b>0 }.

Absolute value. ∣A∣:=A if A≥0∗, and ∣A∣:=−A otherwise (Addition, negation, and subtraction of Dedekind cuts for −A); thus ∣A∣≥0∗ always, and ∣0∗∣=0∗.

Sign extension. For arbitrary cuts A,B,

  • A⋅B:=0∗ if A=0∗ or B=0∗;
  • A⋅B:=∣A∣⋅∣B∣ if A,B are both >0∗ or both <0∗;
  • A⋅B:=−(∣A∣⋅∣B∣) if A,B have opposite signs.

Identity. The multiplicative identity is 1∗={ r∈Q:r<1 }.

Reciprocal. For A>0∗,

A−1:={ p∈Q:p≤0 }  ∪  { p>0:∃ s∈Q, s>0, s∉A, p<1/s }.

Equivalently, a positive rational p lies in A−1 iff 1/p is an upper rational bound of A that is not the least one (Rudin's construction). For A<0∗, set A−1:=−((−A)−1). Division is A/B:=A⋅B−1 for B≠0∗.

Remarks

  • The product formula is stated only for strictly positive cuts A,B>0∗: then there exist positive a∈A, b∈B, so the positive products ab are nonempty and, because A,B have no greatest element (axiom (C3)), A⋅B has none either; together with downward closure this makes A⋅B a genuine cut, the clause {q≤0} being absorbed below those positive products. The formula is deliberately not applied at the boundary A=0∗ or B=0∗, where {q≤0} would leave 0 as a greatest element and so fail to be a cut; products with a zero factor are supplied instead by the first sign rule, A⋅B=0∗, so the operation is well posed on all cuts.
  • On the rational embedding q↦q∗ the operation agrees with Q: (pq)∗=p∗⋅q∗ (The rational cuts embed densely in R, preserving sums, products, 0, 1 and the order); with q∗⋅(1/q)∗=1∗ that gives (q∗)−1=(1/q)∗ for q>0, the reciprocal being the one supplied by For a positive cut A, the reciprocal A−1 satisfies A⋅A−1=1∗.
  • That these operations send cuts to cuts and satisfy the field axioms ( commutativity, associativity, distributivity over addition, identity 1∗, and A⋅A−1=1∗ for every A≠0∗) is The Dedekind reals form a field.
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

For a positive cut A, the reciprocal A−1 satisfies A⋅A−1=1∗

Statement

For A>0∗, the reciprocal A−1 (Multiplication and reciprocals of Dedekind cuts) is a Dedekind cut with A−1>0∗, and A⋅A−1=1∗.

Facts & Assumptions

Given: A cut A with A>0∗, and the multiplicative identity 1∗={r∈Q:r<1}.

[L1]

Nonnegative product: for A,B>0∗, A⋅B={q≤0}∪{ab:a∈A, b∈B, a>0, b>0} (Multiplication and reciprocals of Dedekind cuts).

[L2]

Reciprocal: for A>0∗, A−1={p≤0}∪{ p>0:∃ s∈Q, s>0, s∉A, p<1/s } (Multiplication and reciprocals of Dedekind cuts).

[L3]

A>0∗ means A contains a positive rational; and every cut is a proper, downward-closed set of rationals with no greatest element (Order on the Dedekind reals, Dedekind cut).

[L4]

Q is a field: rational addition and multiplication are commutative and associative, multiplication distributes over addition, and every nonzero rational is invertible (The rationals form a field); the order is total, x≤y implies x+z≤y+z, and 0<x, 0<y imply 0<xy (The rationals form a totally ordered field).

[L6]

Every nonempty subset S⊆N has a least element: there is ℓ∈S with ℓ≤s for all s∈S (The well-ordering principle).

[L5]

Rational power growth: for a rational y>1 one has yn≥1+n(y−1) for every natural n≥1, by induction from Q arithmetic — at n=1 both sides are y, and if yn≥1+n(y−1) then, multiplying by y>0 and writing y=1+(y−1), yn+1≥(1+(y−1))(1+n(y−1))=1+(n+1)(y−1)+n(y−1)2≥1+(n+1)(y−1) because n(y−1)2≥0; and by the Archimedean property every rational is exceeded by some such power; since a cut is proper it omits a rational upper bound, so for any a0>0 some a0yn∉A (The rationals are Archimedean, Dedekind cut).

Proof

technique · direct
1.1

A−1 is a cut with A−1>0∗: since A>0∗ contains 0 and hence, by downward closure, all rationals ≤0, every s∉A is positive; fix a0∈A with a0>0, so any positive p∈A−1 has p<1/s<1/a0 (its witness s∉A satisfies s>a0), making A−1 proper; it is nonempty (it contains 0) and downward closed: a q≤0 lies in the {p≤0} clause, and if 0<q<p with p∈A−1 carrying witness s (p<1/s) then q<p<1/s, so q∈A−1 with the same witness s; it contains a positive p (take any s∉A and 0<p<1/s), and has no greatest element: a p≤0 is exceeded by the positive element just exhibited, while any positive p∈A−1 carries a witness s>0, s∉A with p<1/s, and the rational p′=(p+1/s)/2 satisfies p<p′<1/s, so p′ lies in A−1 with the same witness s yet p′>p.

L2L3L4
1.2

Inclusion A⋅A−1⊆1∗: any q≤0 in A⋅A−1 lies in 1∗, and if a∈A, p∈A−1 with a,p>0, choose s∉A, s>0, p<1/s, so a<s (as a∈A, s∉A) and ap<s⋅(1/s)=1, giving ap∈1∗.

L1L2L3L4
1.3

For the reverse inclusion fix a target x with 0<x<1: pick a rational t with x<t<1 (betweenness in Q) and set y:=1/t, so y>1; choose a0∈A with a0>0 (as A>0∗); by rational power growth some power a0yn∉A, so { n≥1:a0yn∉A } is a nonempty set of naturals.

L3L4L5
2.1

Let n≥1 be the least natural with a0yn∉A (nonempty by step 1.3; n≥1 since a0y0=a0∈A); by minimality a:=a0yn−1∈A with a>0, while s:=a0yn=a⋅y∉A with s>0.

L4L6step 1.3choose
3.1

Set p:=x/a>0; since x<t=1/y gives 1/x>y, we get 1/p=a/x>a⋅y=s, so p<1/s with s>0, s∉A, whence p∈A−1 by the reciprocal's definition; then x=a⋅p with a∈A, p∈A−1, a,p>0, so x∈A⋅A−1, and with the {q≤0} clause this yields 1∗⊆A⋅A−1.

L1L2L4step 1.1step 1.3step 2.1algebra
4.1

Combining the two inclusions gives A⋅A−1=1∗, and by step 1.1 the reciprocal A−1 is a Dedekind cut with A−1>0∗.

step 1.1step 1.2step 3.1∎
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The Dedekind reals form a field

Statement

The set R of Dedekind cuts of Q (The real numbers R as Dedekind cuts), with cut addition and cut multiplication (Addition, negation, and subtraction of Dedekind cuts, Multiplication and reciprocals of Dedekind cuts), is a field.

Facts & Assumptions

Given: Cuts A,B,C∈R, the cut 0∗ (additive identity) and 1∗ (multiplicative identity).

[L1]

Nonnegative product: for A,B>0∗, A⋅B={q≤0}∪{ab:a∈A, b∈B, a>0, b>0} (Multiplication and reciprocals of Dedekind cuts).

[L2]

Sign rules and reciprocal: A⋅B=0∗ if A or B is 0∗; A⋅B=∣A∣∣B∣ for equal signs and −(∣A∣∣B∣) for opposite signs; and A−1=−((−A)−1) when A<0∗ (Multiplication and reciprocals of Dedekind cuts).

[L3]

Absolute value: ∣A∣=A if A≥0∗ and ∣A∣=−A otherwise, so ∣A∣≥0∗ (Multiplication and reciprocals of Dedekind cuts).

[L4]

Addition: A+B={a+b:a∈A, b∈B}, with inverse −A (Addition, negation, and subtraction of Dedekind cuts).

[L5]

(R,+) is an abelian group: + is well defined, commutative, associative, with identity 0∗ (Cut addition: A+B is a cut, commutative and associative, with identity 0∗) and inverses A+(−A)=0∗ (For a cut A, −A is a cut and A+(−A)=0∗).

[L6]

Inclusion totally orders R, so exactly one of A>0∗, A=0∗, A<0∗ holds (Inclusion totally orders the Dedekind reals).

[L7]

Q is a field: rational multiplication is commutative, associative, distributes over addition, and every nonzero rational is invertible (The rationals form a field); its order is total, x≤y implies x+z≤y+z, and 0<x, 0<y imply 0<xy (The rationals form a totally ordered field).

[L8]

The embedding q↦q∗ is an injective ring map with (pq)∗=p∗⋅q∗ and 1∗≠0∗ (The rational cuts embed densely in R, preserving sums, products, 0, 1 and the order).

[L9]

Multiplicative inverse of a positive cut: for A>0∗, the reciprocal A−1 is a cut with A−1>0∗ and A⋅A−1=1∗ (For a positive cut A, the reciprocal A−1 satisfies A⋅A−1=1∗).

[L10]

Negation is an additive homomorphism on (R,+): −(X+Y)=(−X)+(−Y), since ((−X)+(−Y))+(X+Y)=0∗ by commutativity, associativity, and the inverse law, so (−X)+(−Y) is the unique additive inverse of X+Y (Cut addition: A+B is a cut, commutative and associative, with identity 0∗, For a cut A, −A is a cut and A+(−A)=0∗).

[L11]

A cut A is positive iff 0∗<A, and 0∗<A holds exactly when 0∈A; in that case (C3) supplies a∈A with a>0 (Order on the Dedekind reals, Dedekind cut).

Proof

technique · direct
1.1

For A,B>0∗, A⋅B is a cut: it is nonempty and proper, downward closed because any 0<y<ab equals (y/b) b with 0<y/b<a in A (so the positive part of A⋅B is exactly {ab:a∈A,b∈B,a,b>0}), and it has no greatest element because A has none: given ab with a∈A, b∈B, a,b>0, choose a′∈A with a′>a, and then a′b∈A⋅B with a′b>ab since b>0; and 0∗⋅B=0∗ by the sign rule, so multiplication of nonnegatives lands in R.

L1L2L6L7L11
1.2

On nonnegatives multiplication is commutative: A⋅B and B⋅A are the same set, since {ab}={ba} by commutativity of rational multiplication.

L1L7
1.3

Identity on nonnegatives: A⋅1∗=A for A≥0∗. For x∈A with x>0 pick a∈A, a>x (no greatest element), so x=a⋅(x/a) with 0<x/a<1, giving A⊆A⋅1∗; conversely ar<a∈A for 0<r<1 forces ar∈A, so A⋅1∗⊆A; the 0∗ case is the sign rule.

L1L7
1.4

1∗≠0∗, as the embedding is injective and 1≠0 in Q.

L8
1.5

For the reverse inclusion of distributivity, dispose of degenerate cases: if A=0∗ then A⋅B=A⋅C=A⋅(B+C)=0∗, so A⋅B+A⋅C=0∗=A⋅(B+C); if B=0∗ then A⋅B=0∗ and B+C=0∗+C=C (additive identity), so A⋅B+A⋅C=0∗+A⋅C=A⋅C=A⋅(B+C), and symmetrically if C=0∗.

L2L4L5
1.6

Sign rule: for all cuts X,Y, (−X)⋅Y=−(X⋅Y) and X⋅(−Y)=−(X⋅Y); indeed ∣−X∣=∣X∣ so both sides keep magnitude ∣X∣∣Y∣, while negating one factor toggles the same-sign versus opposite-sign classification of the pair and hence flips the product's sign in the definition A⋅B=0∗ / ∣A∣∣B∣ / −(∣A∣∣B∣) (the 0∗ case being immediate), so in particular X⋅Y=−(∣X∣⋅Y) whenever X<0∗.

L2L3L6
2.1

On nonnegatives multiplication is associative: by step 1.1 the positive elements of A⋅B are exactly the products ab, so those of (A⋅B)⋅C are the (ab)c=abc, and likewise A⋅(B⋅C) has positive part the a(bc)=abc; both sides are thus {q≤0}∪{abc:a∈A,b∈B,c∈C, a,b,c>0}, by associativity of rational products.

step 1.1L1L7
2.2

Distributivity on nonnegatives, inclusion ⊆ for A,B,C≥0∗: a positive element of A⋅(B+C) is a⋅w with a∈A, w∈B+C, a,w>0, and w=b+c for some b∈B, c∈C; then a⋅w=ab+ac where ab∈A⋅B and ac∈A⋅C (each product lies in the positive part of its factor product when positive, otherwise in that product's {q≤0} clause), so a⋅w∈A⋅B+A⋅C; with the {q≤0} clause this gives A⋅(B+C)⊆A⋅B+A⋅C.

L1L4L7step 1.1
2.3

For the reverse inclusion assume A,B,C>0∗, the degenerate cases being step 1.5; then A⋅B and A⋅C each contain a positive rational and, being downward-closed cuts (step 1.1), contain positive rationals arbitrarily close to 0.

L1L11step 1.1step 1.5
2.4

Every A≠0∗ has a multiplicative inverse: for A>0∗ the reciprocal A−1 satisfies A⋅A−1=1∗; for A<0∗ we have −A>0∗ and A−1=−((−A)−1), so applying the sign rule to both factors gives A⋅A−1=(−A)⋅(−A)−1=1∗ by the reciprocal of the positive cut −A.

L2L3L9step 1.6
3.1

Take u∈A⋅B+A⋅C with u>0, say u=s+t with s∈A⋅B, t∈A⋅C: if t≤0, pick a positive t′∈A⋅C with t′<u (available by step 2.3) and set s′:=u−t′, so 0<s′≤s (since t≤0 gives s≥u>s′) and s′∈A⋅B by downward closure, then replace (s,t) by (s′,t′); symmetrically if s≤0; so we may assume s,t>0.

L4step 1.1step 2.3
3.2

The nonnegative laws now extend by signs: A⋅B and B⋅A share magnitude ∣A∣∣B∣=∣B∣∣A∣ and the same sign, hence are equal (step 1.2); (A⋅B)⋅C and A⋅(B⋅C) share magnitude ∣A∣∣B∣∣C∣ and the sign given by the product of the three factor signs, hence are equal (step 2.1); and A⋅1∗=A, since 1∗>0∗ leaves the sign of A unchanged and ∣A∣⋅1∗=∣A∣ (step 1.3).

L2L3step 1.2step 1.3step 2.1
4.1

With s,t>0 from step 3.1, step 1.1 gives s=a1b1 and t=a2c1 with a1,a2∈A, b1∈B, c1∈C all positive; set a:=max⁡(a1,a2), so a∈A and a>0.

L11step 1.1step 3.1
5.1

Put b:=s/a and c:=t/a: then 0<b=a1b1/a≤b1, so b∈B, and 0<c=a2c1/a≤c1, so c∈C, both by downward closure; hence u=s+t=ab+ac=a(b+c) with b+c∈B+C, b+c>0, a∈A, a>0, so u∈A⋅(B+C).

L1L4L7step 4.1
6.1

Hence for A,B,C>0∗ and u∈A⋅B+A⋅C: if u≤0 then u∈A⋅(B+C) by its {q≤0} clause, and if u>0 then u∈A⋅(B+C) by step 5.1, so A⋅B+A⋅C⊆A⋅(B+C); with step 2.2 this gives A⋅(B+C)=A⋅B+A⋅C, an equality that also holds in the degenerate cases of step 1.5, so distributivity holds for all A,B,C≥0∗.

L1step 1.5step 2.2step 5.1
7.1

Distributivity for A≥0∗ with B,C≤0∗: writing B=−∣B∣, C=−∣C∣ so that B+C=(−∣B∣)+(−∣C∣)=−(∣B∣+∣C∣) by [L10], the sign rule and nonnegative distributivity give A⋅(B+C)=−(A⋅(∣B∣+∣C∣))=−(A⋅∣B∣+A⋅∣C∣)=(−(A⋅∣B∣))+(−(A⋅∣C∣))=A⋅B+A⋅C, the last equality using that negation is an additive homomorphism.

L3L5L10step 6.1step 1.6
7.2

Distributivity for A≥0∗ with B≥0∗≥C and D:=B+C≥0∗: then B=D+∣C∣ with D,∣C∣≥0∗, so A⋅B=A⋅D+A⋅∣C∣ by nonnegative distributivity, whence A⋅D=A⋅B−A⋅∣C∣=A⋅B+A⋅C because A⋅C=−(A⋅∣C∣) by the sign rule; that is A⋅(B+C)=A⋅B+A⋅C.

L3L4L5step 6.1step 1.6
7.3

Distributivity for A≥0∗ with B≥0∗≥C and D:=B+C<0∗: then ∣C∣=B+∣D∣ with B,∣D∣≥0∗, so A⋅∣C∣=A⋅B+A⋅∣D∣ by nonnegative distributivity, giving A⋅C=−(A⋅∣C∣)=(−(A⋅B))+(−(A⋅∣D∣)) and A⋅D=−(A⋅∣D∣) by the sign rule, whence A⋅B+A⋅C=−(A⋅∣D∣)=A⋅D=A⋅(B+C).

L3L4L5step 6.1step 1.6
8.1

Distributivity for A≥0∗ and arbitrary B,C: if B,C≥0∗ this is step 6.1; if B,C≤0∗ it is step 7.1; otherwise one factor is ≥0∗ and the other ≤0∗, say B≥0∗≥C (else exchange B,C using commutativity of +), and then it is step 7.2 or step 7.3 according as B+C≥0∗ or B+C<0∗; by the sign trichotomy these cases are exhaustive, so A⋅(B+C)=A⋅B+A⋅C.

L5L6step 6.1step 7.1step 7.2step 7.3
9.1

Distributivity for A<0∗: the sign rule gives A⋅(B+C)=−(∣A∣⋅(B+C)) and A⋅B+A⋅C=(−(∣A∣⋅B))+(−(∣A∣⋅C))=−(∣A∣⋅B+∣A∣⋅C), while ∣A∣≥0∗ makes step 8.1 apply to give ∣A∣⋅(B+C)=∣A∣⋅B+∣A∣⋅C, so the two negated cuts coincide and A⋅(B+C)=A⋅B+A⋅C.

L3L5L10step 1.6step 8.1
10.1

By the sign trichotomy every cut A is either ≥0∗ (step 8.1) or <0∗ (step 9.1), so A⋅(B+C)=A⋅B+A⋅C holds for all cuts A,B,C.

L6step 8.1step 9.1
11.1

Thus (R,+) is an abelian group (L5), multiplication is commutative and associative with identity 1∗≠0∗ (step 3.2, step 1.4), distributes over addition (step 10.1), and every nonzero cut is invertible (step 2.4): R is a field.

L5step 1.4step 3.2step 10.1step 2.4∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The rational cuts embed densely in R, preserving sums, products, 0, 1 and the order

Statement

The rational embedding q↦q∗, where q∗={ r∈Q:r<q } (The real numbers R as Dedekind cuts), is injective and order-preserving-and-reflecting, p<q  ⟺  p∗⊊q∗, and a ring embedding: (p+q)∗=p∗+q∗, (pq)∗=p∗⋅q∗, 0↦0∗, 1↦1∗. Moreover its image is dense: for cuts A<B there is a rational q with A<q∗<B.

Facts & Assumptions

Given: Rationals p,q, the embedding q↦q∗={ r∈Q:r<q }, and cuts A,B (The real numbers R as Dedekind cuts).

[L1]

Cut structure: downward closure (p∈A, q<p⇒q∈A), the separation property (a∈A, b∉A⇒a<b), and the absence of a greatest element (Dedekind cut), holding of every element of R (The real numbers R as Dedekind cuts).

[L2]

Order is inclusion: A<B means A⊊B (Order on the Dedekind reals).

[L3]

Trichotomy, transitivity, and irreflexivity of the rational order (The rationals form a totally ordered field).

[L4]

Cut addition is the rational sumset A+B={ a+b:a∈A, b∈B }, the additive inverse is −A={ p∈Q:∃ r>0, −p−r∉A }, and 0∗={ q∈Q:q<0 } is the additive identity of the embedding (Addition, negation, and subtraction of Dedekind cuts).

[L5]

Cut multiplication: for A,B>0∗, A⋅B={ q≤0 }∪{ ab:a∈A, b∈B, a>0, b>0 }; the sign rules A⋅B=0∗ when A or B is 0∗, A⋅B=∣A∣ ∣B∣ for equal signs and A⋅B=−(∣A∣ ∣B∣) for opposite signs; and ∣A∣=A for A≥0∗ else ∣A∣=−A, with 1∗={ r<1 } the multiplicative identity (Multiplication and reciprocals of Dedekind cuts).

[L6]

Q is a field: rational addition and multiplication are commutative and associative, multiplication distributes over addition, and every nonzero rational is invertible (The rationals form a field); its order is total, x≤y implies x+z≤y+z, and 0<x, 0<y imply 0<xy (The rationals form a totally ordered field). Consequently multiplying a<b by a positive preserves the order, and every pair r<s has the strict midpoint r<(r+s)/2<s, since 2=1+1>0 is invertible and 2r<r+s<2s.

Proof

technique · direct
1.1

Order preservation: if p<q then p∗⊊q∗. For r∈p∗ we have r<p<q, so r∈q∗, giving p∗⊆q∗; and p∈q∗ while p∉p∗, so the inclusion is proper.

L3
1.2

Order reflection: if p∗⊊q∗ then p<q. Pick r∈q∗∖p∗; then r<q and ¬(r<p), so p≤r<q, whence p<q.

L3
1.3

Unit identities: 0↦0∗ and 1↦1∗ hold because 0∗={ r<0 } and 1∗={ r<1 } are exactly the cuts named by the embedding at 0 and 1 and fixed as the additive and multiplicative identities.

L4L5
1.4

Additive identity, inclusion p∗+q∗⊆(p+q)∗: a typical element is a+b with a<p and b<q, and order compatibility of rational addition gives a+b<p+q, so a+b∈(p+q)∗.

L4L6
1.5

Additive identity, inclusion (p+q)∗⊆p∗+q∗: given r<p+q set d=(p+q−r)/2>0, a=p−d, b=q−d; then a<p, b<q, and a+b=(p+q)−2d=r, so r=a+b∈p∗+q∗.

L4L6
1.6

Nonnegative product, inclusion p∗⋅q∗⊆(pq)∗ for p,q>0: an element is either ≤0, hence in (pq)∗ since pq>0, or ab with 0<a<p and 0<b<q, and then ab<pb<pq, so ab∈(pq)∗.

L5L6
1.7

Nonnegative product, inclusion (pq)∗⊆p∗⋅q∗ for p,q>0: take r<pq; if r≤0 it lies in the { q≤0 } clause, and if r>0 then r/q<p, so the strict midpoint a=(r/q+p)/2 satisfies r/q<a<p, and b=r/a gives 0<a<p and 0<b<q (as a>r/q>0 yields b=r/a<q), with ab=r∈p∗⋅q∗.

L5L6choose
1.8

Density setup: let A<B, i.e. A⊊B; choose x∈B∖A, and since B has no greatest element choose y∈B with y>x.

L1L2choose
1.9

Negation identity −(p∗)=(−p)∗: by the negation definition −(p∗)={ r:∃ t>0, −r−t∉p∗ }={ r:∃ t>0, −r−t≥p }={ r:∃ t>0, r≤−p−t }={ r:r<−p }=(−p)∗, where −r−t∉p∗ gives −r−t≥p by trichotomy and t=−p−r>0 witnesses the last equality.

L4L3L6
2.1

Additive identity: combining the two inclusions, (p+q)∗=p∗+q∗.

step 1.4step 1.5
2.2

Nonnegative multiplicative identity: for p,q>0 the two inclusions give (pq)∗=p∗⋅q∗, while if p=0 or q=0 then pq=0 and the sign rule 0∗⋅B=0∗ gives (pq)∗=0∗=p∗⋅q∗; hence (pq)∗=p∗⋅q∗ for all p,q≥0.

step 1.6step 1.7L5
2.3

Injectivity: if p∗=q∗ then neither p∗⊊q∗ nor q∗⊊p∗, so by reflection ¬(p<q) and ¬(q<p); trichotomy forces p=q.

step 1.2L3
2.4

Combining preservation and reflection, p<q  ⟺  p∗⊊q∗, that is p<q  ⟺  p∗<q∗: the embedding preserves and reflects order.

step 1.1step 1.2L2
2.5

A<y∗: for a∈A, separation gives a<x (as x∉A) and x<y, so a<y and a∈y∗, whence A⊆y∗; and x∈y∗ (since x<y) while x∉A, so the inclusion is proper, A⊊y∗.

step 1.8L1L2L3
2.6

y∗<B: for r∈y∗, r<y and y∈B, so downward closure gives r∈B, whence y∗⊆B; and y∈B while y∉y∗, so y∗⊊B.

step 1.8L1L2
2.7

Absolute value identity ∣p∗∣=∣p∣∗: since 0∗⊆p∗  ⟺   every r<0 satisfies r<p  ⟺  p≥0, we have p≥0  ⟺  p∗≥0∗; if p≥0 then ∣p∗∣=p∗=∣p∣∗, while if p<0 then p∗<0∗, so ∣p∗∣=−(p∗)=(−p)∗=∣p∣∗ using −(p∗)=(−p)∗ and ∣p∣=−p.

step 1.9L2L3L5
3.1

Multiplicative identity for all signs: the sign rules give p∗⋅q∗=±(∣p∗∣⋅∣q∗∣), and ∣p∗∣⋅∣q∗∣=∣p∣∗⋅∣q∣∗=(∣p∣ ∣q∣)∗ by the absolute-value identity and the nonnegative case; when p,q share a sign pq≥0 and ∣p∣ ∣q∣=pq, so p∗⋅q∗=(pq)∗, and when they have opposite signs pq<0, ∣p∣ ∣q∣=−pq, and −((−pq)∗)=(pq)∗ by the negation identity, so again p∗⋅q∗=(pq)∗ (the p=0 or q=0 case being step 2.2); hence (pq)∗=p∗⋅q∗ for all p,q.

step 2.2step 2.7step 1.9L5
4.1

Taking q=y yields A<q∗<B, so the image is dense; with injectivity, order preservation/reflection, and the ring identities (p+q)∗=p∗+q∗, (pq)∗=p∗⋅q∗, 0↦0∗, 1↦1∗, the map q↦q∗ is a dense, order-preserving ring embedding of Q into R. Closure of the image under reciprocals, which a subfield would also require, is not established here.

step 2.1step 3.1step 1.3step 2.3step 2.4step 2.5step 2.6∎
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

The Dedekind reals form a totally ordered field

Statement

The inclusion order A≤B:  ⟺  A⊆B (Order on the Dedekind reals) makes R, the field of Dedekind cuts (The Dedekind reals form a field), a totally ordered field: the order is total, translation-invariant (A≤B⇒A+C≤B+C), and closed under multiplication of nonnegatives (0∗≤A and 0∗≤B⇒0∗≤A⋅B).

Facts & Assumptions

Given: Cuts A,B,C ordered by inclusion (Order on the Dedekind reals).

[L1]

R (Dedekind cuts) is a field under + and ⋅ (The Dedekind reals form a field).

[L2]

Inclusion totally orders R: reflexive, antisymmetric, transitive, and total (Inclusion totally orders the Dedekind reals).

[L3]

Addition is the sumset A+B={ a+b:a∈A, b∈B }, with identity 0∗ (Addition, negation, and subtraction of Dedekind cuts).

[L4]

For strictly positive cuts A,B>0∗, A⋅B={ q∈Q:q≤0 }∪{ ab:a∈A, b∈B, a>0, b>0 }; and A⋅B=0∗ whenever A=0∗ or B=0∗ (the sign rule). Also 0∗={ r∈Q:r<0 } (Multiplication and reciprocals of Dedekind cuts, Order on the Dedekind reals).

Proof

technique · direct
1.1

By Inclusion totally orders the Dedekind reals the relation ⊆ is a reflexive, antisymmetric, transitive, and total order on R.

L2
1.2

Translation invariance: suppose A⊆B. Every element of A+C has the form a+c with a∈A, c∈C; since a∈A⊆B, also a+c∈B+C. Hence A+C⊆B+C, i.e. A≤B⇒A+C≤B+C.

L3
1.3

Positivity of products of nonnegatives: suppose 0∗≤A and 0∗≤B. If A=0∗ or B=0∗, then A⋅B=0∗ by the sign rule [L4], so 0∗⊆A⋅B. Otherwise A,B>0∗, and the positive-case formula [L4] gives A⋅B⊇{ q∈Q:q≤0 }⊇{ r∈Q:r<0 }=0∗, so 0∗⊆A⋅B. In either case 0∗≤A⋅B.

L4
2.1

Thus R is a field whose inclusion order is total, translation-invariant, and closed under multiplication of nonnegative cuts: a totally ordered field.

step 1.1step 1.2step 1.3L1∎
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The Dedekind reals are Archimedean

Statement

R (Dedekind cuts) is Archimedean: for every cut A there is a natural number n with A<n∗. Equivalently, the rational cuts (n∗)n∈N are cofinal in R: no single cut is an upper bound for all of them.

Facts & Assumptions

Given: A cut A.

[L1]

A cut is a proper subset of Q (A≠Q), and a∈A, b∉A⇒a<b (Dedekind cut); the elements of R are exactly these cuts (The real numbers R as Dedekind cuts).

[L2]

Rational Archimedean property: for every q∈Q there is a natural number n with n>q (The rationals are Archimedean).

[L3]

The embedding preserves order: p<q⇒p∗⊊q∗, i.e. p∗<q∗ (The rational cuts embed densely in R, preserving sums, products, 0, 1 and the order).

[L4]

Inclusion order, and transitivity of < in the totally ordered field (Order on the Dedekind reals, The Dedekind reals form a totally ordered field).

Proof

technique · direct
1.1

Since A≠Q, choose a rational q∉A.

L1choose
1.2

By the rational Archimedean property, choose a natural number n with n>q.

L2choose
2.1

A⊆q∗: for a∈A, the separation property gives a<q (as q∉A), so a∈q∗.

step 1.1L1
2.2

q∗<n∗: from q<n and order preservation, q∗⊊n∗.

step 1.2L3
3.1

Hence A⊆q∗⊊n∗, so A<n∗: the rational cuts are cofinal and R is Archimedean.

step 2.1step 2.2L4∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

Dedekind completeness: the least-upper-bound property

Statement

Least-upper-bound property. Every nonempty set S of Dedekind cuts that is bounded above (there is a cut B with A≤B for all A∈S) has a least upper bound sup⁡S, and it is given explicitly by the union C:=⋃A∈SA. Together with The Dedekind reals form a totally ordered field this shows R is a complete totally ordered field: the Dedekind construction is order-complete. This order-completeness is the Dedekind counterpart of the Cauchy-sequence completeness of R.

Facts & Assumptions

Given: A nonempty set S of Dedekind cuts bounded above by a cut B (A≤B for all A∈S), and C:=⋃A∈SA (The real numbers R as Dedekind cuts).

[L1]

Cut axioms: (C1) proper and nonempty, (C2) downward closed, (C3) no greatest element (Dedekind cut).

[L2]

Order is inclusion: A≤D  ⟺  A⊆D (Order on the Dedekind reals).

[L3]

Inclusion is a partial (indeed total) order, so upper and least-upper bounds are taken with respect to ⊆ (Inclusion totally orders the Dedekind reals).

[L4]

R is a totally ordered field; the least-upper-bound property below is the order-completeness that complements it (The Dedekind reals form a totally ordered field).

Proof

technique · direct
1.1

(C1) C is nonempty and proper: S has a member A0 with A0≠∅ and A0⊆C, so C≠∅; and every A∈S satisfies A⊆B, so C=⋃A∈SA⊆B with B≠Q, hence C≠Q.

givenL1L2
1.2

(C2) C is downward closed: if p∈C then p∈A for some A∈S; for q<p, downward closure of A gives q∈A⊆C.

givenL1
1.3

(C3) C has no greatest element: if p∈C then p∈A for some A∈S; as A has no greatest element there is r∈A with r>p, and r∈C.

givenL1
1.4

C is an upper bound for S: every A∈S satisfies A⊆⋃A′∈SA′=C, i.e. A≤C.

givenL2
1.5

C is below every upper bound: if a cut D satisfies A≤D for all A∈S, then A⊆D for all A, so C=⋃A∈SA⊆D, i.e. C≤D.

givenL2L3
2.1

C is a Dedekind cut.

step 1.1step 1.2step 1.3L1
3.1

Therefore sup⁡S exists and equals C=⋃A∈SA: R has the least-upper-bound property. With The Dedekind reals form a totally ordered field, R is a complete totally ordered field, the order-completeness of the Dedekind construction, the exact counterpart of Cauchy-sequence completeness.

step 2.1step 1.4step 1.5L4∎

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

The cut S={q:q<0 or q2<2} is an irrational real number

Example

The set S:={q∈Q:q<0 or q2<2} is a Dedekind cut (Dedekind cut), hence a real number (The real numbers R as Dedekind cuts), yet no rational lies "at its boundary": it is the cut that names 2, the real number Q lacks. It is the canonical witness that cuts capture limits missing from Q, and the standard test case for the completeness of R.

Facts & Assumptions

Given: The set S:={q∈Q:q<0 or q2<2}, the cut axioms (C1)–(C3) (Dedekind cut), and R as the set of all cuts with rational embedding q↦q∗={r∈Q:r<q} (The real numbers R as Dedekind cuts).

[L1]

Q is a totally ordered field; in particular squaring is order-preserving on nonnegatives (0≤a<b⇒a2<b2) and the usual rational arithmetic holds (The rationals form a totally ordered field).

[L2]

No rational number squares to 2 (FALSE: some rational number squares to 2).

Verification

technique · direct
1.1

(C1) 0∈S since 02=0<2, so S≠∅; and 2∉S since 2>0 and 22=4>2, so S≠Q.

givenL1
1.2

(C2) Let p∈S and q<p. If q<0 then q∈S by definition. Otherwise 0≤q<p, so p>0; then p∈S forces p2<2, and 0≤q<p gives q2<p2<2, whence q∈S.

givenL1
1.3

(C3, case q≤0) Given q∈S with q≤0, take r=1: then 1∈S (as 12=1<2) and r=1>0≥q, so r>q.

givenL1
1.4

(C3, case q>0) Given q∈S with q>0, we have q2<2; set r=2q+2q+2. Then r−q=2−q2q+2>0, so r>q>0, while r2−2=2 (q2−2)(q+2)2<0, so r2<2; hence r∈S with r>q.

givenL1algebra
2.1

(C3) Combining the two cases, every q∈S admits r∈S with r>q: S has no greatest element.

step 1.3step 1.4
3.1

By steps 1.1, 1.2 and 2.1, S satisfies (C1)–(C3); it is a Dedekind cut (Dedekind cut), i.e. a real number (The real numbers R as Dedekind cuts).

step 1.1step 1.2step 2.1
4.1

Finally S≠p∗ for every p∈Q: were S=p∗={r:r<p}, then p∉S would give p>0 and p2≥2, while p2=2 is impossible by [L2], so p2>2; as p>0 we have p+2>0, and then s:=2p+2p+2 satisfies 0<s<p and s2>2, so s∉S, yet s<p puts s∈p∗=S, a contradiction. Thus S is a cut represented by no rational: it is the cut that names 2, the real number absent from Q.

step 3.1L2algebra∎
False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-24Open item page →

FALSE: some rational number squares to 2

Statement

False claim: there exists x∈Q with x2=2.

Facts & Assumptions

Given: The rationals as quotients of integer pairs (The rationals as equivalence classes of pairs of integers).

[A1]

Every rational can be written a/b in lowest terms, with a,b not both even (cancel common factors of 2; the process terminates by well-ordering of N).

[A2]

Parity in Z: if k2 is even then k is even (an odd k=2j+1 has odd square 4j2+4j+1).

Refutation

technique · contradiction
1.1

Assume, for contradiction, that some x∈Q has x2=2; write x=a/b in lowest terms, a,b not both even.

assume-contraA1
2.1

Clearing denominators: a2=2b2.

step 1.1algebra
3.1

a2 is even, hence a is even: a=2c.

step 2.1A2
4.1

Substituting: 4c2=2b2, so b2=2c2 is even, hence b is even.

step 3.1A2algebra
5.1

Both a and b are even, contradicting the lowest-terms choice of step 1.1; the assumption fails: no rational squares to 2.

step 4.1step 1.1discharge-contradiction∎
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25Open item page →

FALSE: every Dedekind cut has a greatest element

Statement

False claim: every Dedekind cut (Dedekind cut) has a greatest element: some m∈A with q≤m for all q∈A.

Facts & Assumptions

Given: The cut axioms (C1)–(C3) (Dedekind cut), R as the set of all cuts (The real numbers R as Dedekind cuts), and the rational cut 0∗:={q∈Q:q<0}.

[L1]

Q is a totally ordered field; in particular for q<0 the rational q/2 satisfies q<q/2<0 (The rationals form a totally ordered field).

Refutation

technique · direct
1.1

(C1, C2) 0∗={q∈Q:q<0} is nonempty (−1∈0∗) and proper (0∉0∗), and it is downward closed: q<p<0⇒q<0, so q∈0∗.

givenL1
1.2

(C3) For any q∈0∗, i.e. q<0, the rational q/2 satisfies q<q/2<0, so q/2∈0∗ and q/2>q; hence no element of 0∗ is greatest.

givenL1
2.1

By steps 1.1 and 1.2, 0∗ satisfies (C1)–(C3): it is a Dedekind cut (Dedekind cut), i.e. a real number (The real numbers R as Dedekind cuts), with no greatest element.

step 1.1step 1.2
3.1

Thus 0∗ is a Dedekind cut having no greatest element, directly contradicting the claim; more strongly, "no greatest element" is precisely axiom (C3), which every cut must satisfy, so the claim fails for all cuts and is false.

step 2.1given∎

Sources