Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25
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.

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∎

Depends on

Used by

Dependency tree · two levels

9 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