False statementConstruction: AI-adaptedVerification: 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.

FALSE: every Dedekind cut has a greatest element

Statement

False claim: every Dedekind cut (Dedekind cut) has a greatest element: some $m \in A$ with $q \leq m$ for all $q \in 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 \in 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 \in Q : q < 0}$ is nonempty ( $- 1 \in 0^{*}$ ) and proper ( $0 \notin 0^{*}$ ), and it is downward closed: $q < p < 0 \Rightarrow q < 0$ , so $q \in 0^{*}$ .

givenL1

1.2

(C3) For any $q \in 0^{*}$ , i.e. $q < 0$ , the rational $q / 2$ satisfies $q < q / 2 < 0$ , so $q / 2 \in 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∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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)
Math 331 course handout: Dedekind Cuts and Real Numbers (Hobart and William Smith Colleges) (standard reference, not scraped)
Dedekind cut (Wikipedia) (standard reference, not scraped)