Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 AA, −A-A is a cut and A+(−A)=0∗A + (-A) = 0^{*}

Statement

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

Facts & Assumptions

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

[A1]

Cut axioms (C1)–(C3), and the restatement that for a∈Aa \in A and b∉Ab \notin A one has a<ba < b; the contrapositive of (C2): if x∉Ax \notin A and y>xy > x then y∉Ay \notin A (Dedekind cut).

[A2]

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

[L1]

Q\mathbb{Q} is Archimedean: for every rational xx there is a natural number nn with x<nx < n (The rationals are Archimedean).

[L2]

Q\mathbb{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 AA and −A-A are cuts then A+(−A)A + (-A) is a cut (Cut addition: A+BA+B is a cut, commutative and associative, with identity 0∗0^{*}).

Proof

technique · direct
1.1

(C1, nonempty) A≠QA \neq \mathbb{Q}, so pick s∉As \notin A; then p0:=−s−1p_{0} := -s - 1 satisfies −p0−1=s∉A-p_{0} - 1 = s \notin A with witness r=1>0r = 1 > 0, so p0∈−Ap_{0} \in -A and −A≠∅-A \neq \varnothing.

A1choose
1.2

(C1, proper) A≠∅A \neq \varnothing, so pick a∈Aa \in A; then −a∉−A-a \notin -A, for if −a∈−A-a \in -A there were r>0r > 0 with a−r=−(−a)−r∉Aa - r = -(-a) - r \notin A, yet a−r<a∈Aa - r < a \in A forces a−r∈Aa - r \in A by (C2), a contradiction. Hence −A≠Q-A \neq \mathbb{Q}.

A1L2
1.3

(C2, downward closed) If p∈−Ap \in -A with witness r>0r > 0 (so −p−r∉A-p - r \notin A) and q<pq < p, then −q−r>−p−r-q - r > -p - r, so −q−r∉A-q - r \notin A by the contrapositive of (C2); thus q∈−Aq \in -A with the same rr.

A1L2
1.4

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

A1L2
1.5

(A+(−A)⊆0∗A + (-A) \subseteq 0^{*}) For a∈Aa \in A and p∈−Ap \in -A with witness r>0r > 0: since −p−r∉A-p - r \notin A while a∈Aa \in A, the restatement gives a<−p−ra < -p - r, so a+p<−r<0a + p < -r < 0; hence a+p∈0∗a + p \in 0^{*}.

A1L2
1.6

(setup) Fix v∈0∗v \in 0^{*} and put w:=−v/2w := -v/2, so w>0w > 0 since v<0v < 0; by (C1) choose a0∈Aa_{0} \in A (as A≠∅A \neq \varnothing) and b0∉Ab_{0} \notin A (as A≠QA \neq \mathbb{Q}).

A1L2choose
2.1

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

step 1.1step 1.2step 1.3step 1.4A1
2.2

(bounded above) Apply [L1] to the rational b0/wb_{0}/w: there is a natural MM with b0/w<Mb_{0}/w < M, so b0<Mwb_{0} < Mw since w>0w > 0; because b0∉Ab_{0} \notin A and Mw>b0Mw > b_{0}, the contrapositive of (C2) gives Mw∉AMw \notin A, whence any k∈Zk \in \mathbb{Z} with kw∈Akw \in A satisfies k<Mk < M (else k≥Mk \ge M gives kw≥Mwkw \ge Mw, so kw∉Akw \notin A by the contrapositive of (C2)), so K:={ k∈Z:kw∈A }K := \{\, k \in \mathbb{Z} : kw \in A \,\} is bounded above by MM.

step 1.6L1L2A1
2.3

(nonempty) Apply [L1] to the rational −a0/w-a_{0}/w: there is a natural NN with −a0/w<N-a_{0}/w < N, so −Nw<a0-Nw < a_{0} since w>0w > 0; because a0∈Aa_{0} \in A and −Nw<a0-Nw < a_{0}, (C2) gives −Nw∈A-Nw \in A, so −N∈K-N \in K and K≠∅K \neq \varnothing.

step 1.6L1L2A1
3.1

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

step 2.2step 2.3A2
4.1

(0∗⊆A+(−A)0^{*} \subseteq A + (-A)) With nn from step 3.1, set p:=−(n+2)wp := -(n+2)w; the witness r=w>0r = w > 0 gives −p−w=(n+1)w∉A-p - w = (n+1)w \notin A, so p∈−Ap \in -A, while nw∈Anw \in A, and nw+p=nw−(n+2)w=−2w=vnw + p = nw - (n+2)w = -2w = v. Hence v=nw+p∈A+(−A)v = nw + p \in A + (-A); as v∈0∗v \in 0^{*} was arbitrary, 0∗⊆A+(−A)0^{*} \subseteq A + (-A).

step 3.1A1L2
5.1

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

step 1.5step 4.1step 2.1L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 46 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources