LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)

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.

For a cut $A$ , $- A$ is a cut and $A + (- A) = 0^{*}$

Statement

For every Dedekind cut $A$ , the set $- A = {p \in Q : \exists r \in Q, r > 0, - p - r \notin A}$ (Addition, negation, and subtraction of Dedekind cuts) is again a Dedekind cut, and $A + (- A) = 0^{*}$ , where $0^{*} = {q \in Q : q < 0}$ . Thus every cut has an additive inverse and $(R, +)$ is a group.

Facts & Assumptions

Given: A Dedekind cut $A$ ; $- A : = {p \in Q : \exists r > 0, - p - r \notin A}$ , $A + (- A) : = {a + p : a \in A, p \in - A}$ , and $0^{*} : = {q \in Q : q < 0}$ (Addition, negation, and subtraction of Dedekind cuts).

[A1]

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

[A2]

A nonempty set $K \subseteq Z$ with $k < M$ for every $k \in K$ , where $M \in Z$ , has a greatest element: ${M - k : k \in K}$ is then a nonempty set of positive integers, so it has a least element $M - n$ by "every nonempty subset $S \subseteq 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 \neq Q$ , so pick $s \notin A$ ; then $p_{0} : = - s - 1$ satisfies $- p_{0} - 1 = s \notin A$ with witness $r = 1 > 0$ , so $p_{0} \in - A$ and $- A \neq \emptyset$ .

A1choose

1.2

(C1, proper) $A \neq \emptyset$ , so pick $a \in A$ ; then $- a \notin - A$ , for if $- a \in - A$ there were $r > 0$ with $a - r = - (- a) - r \notin A$ , yet $a - r < a \in A$ forces $a - r \in A$ by (C2), a contradiction. Hence $- A \neq Q$ .

A1L2

1.3

(C2, downward closed) If $p \in - A$ with witness $r > 0$ (so $- p - r \notin A$ ) and $q < p$ , then $- q - r > - p - r$ , so $- q - r \notin A$ by the contrapositive of (C2); thus $q \in - A$ with the same $r$ .

A1L2

1.4

(C3, no greatest) If $p \in - A$ with witness $r > 0$ , set $t : = p + r / 2 > p$ ; then $- t - r / 2 = - p - r \notin A$ , so $t \in - A$ with witness $r / 2 > 0$ , and $t > p$ .

A1L2

1.5

( $A + (- A) \subseteq 0^{*}$ ) For $a \in A$ and $p \in - A$ with witness $r > 0$ : since $- p - r \notin A$ while $a \in A$ , the restatement gives $a < - p - r$ , so $a + p < - r < 0$ ; hence $a + p \in 0^{*}$ .

A1L2

1.6

(setup) Fix $v \in 0^{*}$ and put $w : = - v / 2$ , so $w > 0$ since $v < 0$ ; by (C1) choose $a_{0} \in A$ (as $A \neq \emptyset$ ) and $b_{0} \notin A$ (as $A \neq 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 $b_{0} / w$ : there is a natural $M$ with $b_{0} / w < M$ , so $b_{0} < M w$ since $w > 0$ ; because $b_{0} \notin A$ and $M w > b_{0}$ , the contrapositive of (C2) gives $M w \notin A$ , whence any $k \in Z$ with $k w \in A$ satisfies $k < M$ (else $k \geq M$ gives $k w \geq M w$ , so $k w \notin A$ by the contrapositive of (C2)), so $K : = {k \in Z : k w \in A}$ is bounded above by $M$ .

step 1.6L1L2A1

2.3

(nonempty) Apply [L1] to the rational $- a_{0} / w$ : there is a natural $N$ with $- a_{0} / w < N$ , so $- N w < a_{0}$ since $w > 0$ ; because $a_{0} \in A$ and $- N w < a_{0}$ , (C2) gives $- N w \in A$ , so $- N \in K$ and $K \neq \emptyset$ .

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 $n w \in A$ because $n \in K$ , while $n + 1 > n$ gives $n + 1 \notin K$ , i.e. $(n + 1) w \notin A$ .

step 2.2step 2.3A2

4.1

( $0^{*} \subseteq A + (- A)$ ) With $n$ from step 3.1, set $p : = - (n + 2) w$ ; the witness $r = w > 0$ gives $- p - w = (n + 1) w \notin A$ , so $p \in - A$ , while $n w \in A$ , and $n w + p = n w - (n + 2) w = - 2 w = v$ . Hence $v = n w + p \in A + (- A)$ ; as $v \in 0^{*}$ was arbitrary, $0^{*} \subseteq 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∎

Depends on

Used by

The Dedekind reals form a field Theorem

Dependency tree · two levels

22 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

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (Appendix: construction of ℝ) (standard reference, not scraped)
E. Landau, Foundations of Analysis (standard reference, not scraped)
M. Girotti, Addendum — Construction of $\mathbb{R}$ via Dedekind's method (MATH 317, Advanced Calculus of One Variable) (standard reference, not scraped)
Math 331 course handout: Dedekind Cuts and Real Numbers (Hobart and William Smith Colleges) (standard reference, not scraped)

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

Statement

Facts & Assumptions

Proof

Depends on

Used by

Dependency tree · two levels

Sources

For a cut $A$ , $- A$ is a cut and $A + (- A) = 0^{*}$