Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (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.

An unbounded set has no supremum: the naturals inside R\mathbb{R}

Statement refuted

Refuted claim: every subset of R\mathbb{R} has a supremum in R\mathbb{R} (FALSE: every subset of R\mathbb{R} has a supremum).

The witness here is the canonical copy of the natural numbers inside R\mathbb{R}, A={n1 : n1},A = \{\, n \cdot 1 \ : \ n \ge 1 \,\}, where n1n \cdot 1 denotes the canonical natural 1++1n\underbrace{1 + \cdots + 1}_{n} of the field (Canonical naturals are positive and strictly increasing). The set AA is nonempty, so the nonemptiness hypothesis of the least-upper-bound property (Complete ordered field (least-upper-bound property)) is satisfied; what fails is boundedness above, and it fails as badly as possible, since AA has no upper bound whatsoever. That is precisely the Archimedean property of R\mathbb{R} (Every complete ordered field is Archimedean), so this failure is a theorem about R\mathbb{R}, not an accident of the set chosen.

Facts & Assumptions

Given: The complete ordered field R\mathbb{R} and the set A:={n1:n1}A := \{\, n \cdot 1 : n \ge 1 \,\} of its canonical naturals.

[L1]

Canonical naturals: 11=11 \cdot 1 = 1 and n1>0n \cdot 1 > 0 for every n1n \ge 1 (Canonical naturals are positive and strictly increasing).

[L2]

Archimedean property: R\mathbb{R} is a complete ordered field, hence Archimedean, so for every xRx \in \mathbb{R} there is a natural n1n \ge 1 with x<n1x < n \cdot 1 (Every complete ordered field is Archimedean, Archimedean ordered field).

[L3]

Upper bound, bounded above, supremum: uu is an upper bound of XX when xux \le u for every xXx \in X; XX is bounded above when it has an upper bound; and a supremum of XX is an upper bound of XX that is \le every upper bound of XX, so in particular every supremum is an upper bound (Complete ordered field (least-upper-bound property), Lower bound, bounded below, bounded set).

[L4]

The refuted claim: every SRS \subseteq \mathbb{R} has a supremum in R\mathbb{R} (FALSE: every subset of R\mathbb{R} has a supremum).

[L5]

Order: trichotomy holds, so a<ba < b and bab \le a cannot both be true (Ordered field, Complete ordered field (least-upper-bound property)).

Counterexample

technique · direct
1.1

AA is a nonempty subset of R\mathbb{R}: taking n=1n = 1 gives 11=1A1 \cdot 1 = 1 \in A.

L1
1.2

Let xRx \in \mathbb{R} be arbitrary.

assume-hyp
2.1

xx is not an upper bound of AA: the Archimedean property supplies a natural n1n \ge 1 with x<n1x < n \cdot 1, and n1n \cdot 1 is an element of AA, so the requirement n1xn \cdot 1 \le x for an upper bound fails by trichotomy.

step 1.2L2L3L5
3.1

Since xx was an arbitrary real number, no real number is an upper bound of AA; hence AA is not bounded above.

step 2.1step 1.2L3
4.1

A supremum of AA would in particular be an upper bound of AA, and there is none, so AA has no supremum in R\mathbb{R} even though AA is nonempty; the claim that every subset of R\mathbb{R} has a supremum is refuted, and the boundedness hypothesis of the least-upper-bound property cannot be dropped.

step 3.1step 1.1L3L4

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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