Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

The Dedekind reals form a totally ordered field

Statement

The inclusion order A≤B:  ⟺  A⊆BA \le B :\iff A \subseteq B (Order on the Dedekind reals) makes R\mathbb{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+CA \le B \Rightarrow A + C \le B + C), and closed under multiplication of nonnegatives (0∗≤A0^{*} \le A and 0∗≤B⇒0∗≤A⋅B0^{*} \le B \Rightarrow 0^{*} \le A \cdot B).

Facts & Assumptions

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

[L1]

R\mathbb{R} (Dedekind cuts) is a field under ++ and ⋅\cdot (The Dedekind reals form a field).

[L2]

Inclusion totally orders R\mathbb{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 }A + B = \{\, a + b : a \in A,\ b \in B \,\}, with identity 0∗0^{*} (Addition, negation, and subtraction of Dedekind cuts).

[L4]

For strictly positive cuts A,B>0∗A, B > 0^{*}, A⋅B={ q∈Q:q≤0 }∪{ ab:a∈A, b∈B, a>0, b>0 }A \cdot B = \{\, q \in \mathbb{Q} : q \le 0 \,\} \cup \{\, a b : a \in A,\ b \in B,\ a > 0,\ b > 0 \,\}; and A⋅B=0∗A \cdot B = 0^{*} whenever A=0∗A = 0^{*} or B=0∗B = 0^{*} (the sign rule). Also 0∗={ r∈Q:r<0 }0^{*} = \{\, r \in \mathbb{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 ⊆\subseteq is a reflexive, antisymmetric, transitive, and total order on R\mathbb{R}.

L2
1.2

Translation invariance: suppose A⊆BA \subseteq B. Every element of A+CA + C has the form a+ca + c with a∈Aa \in A, c∈Cc \in C; since a∈A⊆Ba \in A \subseteq B, also a+c∈B+Ca + c \in B + C. Hence A+C⊆B+CA + C \subseteq B + C, i.e. A≤B⇒A+C≤B+CA \le B \Rightarrow A + C \le B + C.

L3
1.3

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

L4
2.1

Thus R\mathbb{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∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 22 results over 13 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